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.
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.