I agree with the concerns on the false dichotomy between theoretical computer science and mathematics, but from the mathematician's perspective I think there's another issue not being discussed due to the typical CS obsession over automated proof systems.
Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of course the point is also to be correct, but somehow communicating insight takes priority. Relying on large bodies of latent knowledge, and omitting details, is an effective way to do that. Allowing for occasional mistakes is okay, because mathematics as a whole is fault tolerant (or at least, history gives evidence to that claim).
Lamport's field is a bit different, because there they study distributed protocols with the intent of creating value in the real world. So when they prove a theorem, they're not just proving a theorem to gain understanding about something, they're proving a theorem so they can improve the security or fault-tolerance (or whatever else) of some real system. Writing down a 200+ page TLA proof is measurably worth the investment because the users of their work (applied computer scientists and engineers) want error-free theorems and a clean CS literature much more than they want insight.
For mathematicians communicating to other mathematicians, a two-paragraph argument that is convincing and omits the details (that one can verify on their own) is much more valuable. I'm not trying to make a value judgement either way, just trying to explain the culture of math proofs and why I think something like TLA+ will never catch on among mainstream mathematicians. You might say it's mathematicians defending their job security, but it's also simply that mathematicians like exploring and inventing and hearing creative proofs and perspectives. Deferring things to computers removes the a-ha moment.
[Edit] And the idea that somehow high school students and undergraduates will magically start reading and understanding proofs because we write them using TLA+ is a joke.
What do you think of the idea of writing proofs in the hierarchical style in Lamport's section 3, but not using TLA? To me, the hierarchical proofs seemed very clear and easy to understand, but the TLA (although I only skimmed it) seemed to introduce too much formalism and thereby hurt readability.
Also, it would be easy to put paragraphs of text in between hierarchical proof statements, which would preserve the ability to give intuition and proof sketches. Here I'm thinking of things like analysis, where (at least in my experience) what you really want to do is see the picture of the proof in your head and understand it that way, and the written proof is always just a way of checking it.
I think people already do write things in a hierarchical way. They have one main theorem which is supported by multiple propositions and lemmas and corollaries. At least, this is how all good papers I read are organized.
I think Lamport's vision is that the hierarchy extends down to the very last detail. This is what I'm skeptical of, because no mathematician has time to do this. To paraphrase Newton, you need to stand on the shoulders of giants to make progress.
Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of course the point is also to be correct, but somehow communicating insight takes priority. Relying on large bodies of latent knowledge, and omitting details, is an effective way to do that. Allowing for occasional mistakes is okay, because mathematics as a whole is fault tolerant (or at least, history gives evidence to that claim).
Lamport's field is a bit different, because there they study distributed protocols with the intent of creating value in the real world. So when they prove a theorem, they're not just proving a theorem to gain understanding about something, they're proving a theorem so they can improve the security or fault-tolerance (or whatever else) of some real system. Writing down a 200+ page TLA proof is measurably worth the investment because the users of their work (applied computer scientists and engineers) want error-free theorems and a clean CS literature much more than they want insight.
For mathematicians communicating to other mathematicians, a two-paragraph argument that is convincing and omits the details (that one can verify on their own) is much more valuable. I'm not trying to make a value judgement either way, just trying to explain the culture of math proofs and why I think something like TLA+ will never catch on among mainstream mathematicians. You might say it's mathematicians defending their job security, but it's also simply that mathematicians like exploring and inventing and hearing creative proofs and perspectives. Deferring things to computers removes the a-ha moment.
[Edit] And the idea that somehow high school students and undergraduates will magically start reading and understanding proofs because we write them using TLA+ is a joke.