My understanding from the linked paper in another thread, is not to do it the way Spivak does. That is, the article says Lamport "walked us through a proof of a corollary to the mean value theorem from that textbook, pointing out statements that he felt were not precise or rigorous enough and rewriting the proof using his technique."

My reading of that is that Lamport found faults in Spivak's approach. Did I missread that?

I will say that this really looks like a way to write proofs for computers to read, moreso than a way to write them for other people. Probably has great value, but not too surprising that it isn't widespread.

Hear, hear. Spivak motivated me to emphasize the humanistic features of mathematics.

Thankfully, his view underpins elite mathematics programs, e.g.

http://www.hcssim.org

http://en.wikipedia.org/wiki/Math_55