About two years ago, I came across this paper by Lamport
on writing proofs hierarchically. It changed how I wrote all of my proofs for about six months and identified the gaps in my understanding and knowledge extremely well. These days, I won't use it for simpler proofs, but I find it indispensable when I want to thoroughly understand long and complex ones.
I think this is potentially a wonderful pedagogical tool, in that all steps and assumptions are organized and easily referred to, and is also useful for self-checking. Some discussion on the blog evaluating Deolalikar's claimed proof of $P\neq NP$, to give one example, Professor Tao's apposite remarks on the need for precision, (August 15, 2010, 3:05 PM - I hope he doesn't mind my quoting him)
One thing this illustrates is the importance of setting out precise definitions. I feel that if Deolalikar had written down a precise definition of what it meant for a solution space to be polylog parameterisable, the difficulties would have been found a lot sooner, and in particular probably by Deolalikar himself, well before he finished the preprint to share with others.
reminded me of Lamport's essay. Lamport comments on something similar from his own experience:
The style was first applied to proofs of ordinary theorems in a paper I wrote with Martín Abadi. He had already written conventional proofs—proofs that were good enough to convince us and, presumably, the referees. Rewriting the proofs in a structured style, we discovered that almost every one had serious mistakes, though the theorems were correct. Any hope that incorrect proofs might not lead to incorrect theorems was destroyed in our next collaboration. Time and again, we would make a conjecture and write a proof sketch on the blackboard—a sketch that could easily have been turned into a convincing conventional proof—only to discover, by trying to write a structured proof, that the conjecture was false. Since then, I have never believed a result without a careful, structured proof. My skepticism has helped avoid numerous errors.
Has anyone had experience with this style of writing proofs?