Structured proofs

I know, I know, I'm never going to be a mathematician, but here is an article about a talk by Leslie Lamport about how 21st century proofs should be written. And here is Lamport's own paper on the topic. I'm totally with him on the structure - I think a hierarchical proof structure is a great idea, and a much more careful and explicit structure is also much more understandable. But when he goes to defining a formal language TLA+ for expressing proofs, I have to say that the sheer ugliness of the format is an instant dealbreaker for me. No way. That is not the elegant way to express proofs.

Further thought is necessary. But I'll bet I can come up with a prettier language.