Community experiences writing Lamport's structured proofs About two years ago, I came across this paper by Lamport
http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf
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?
 A: From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.) 
I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction. 
When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:
$$
\frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}}
     {\Gamma \vdash [e]_R \in A/R}
$$
That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.
But using this fact is rather painful: 
$$
\frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B}
$$
This rule says that if you know that 


*

*$e$ is an element of $A/R$, and 

*$t$ is some element of $B$  with a free variable $x$ in set $A$, and

*if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)


Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.) 
What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof). 
I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.
