The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

>Interesting perspective.  I've never heard someone previously say that it's 
>important to be able to
>"check Coq proofs by hand."
One good reason to check proofs, or at least, to understand what is
going on with proofs is
that is useful for debugging your statements: We know that the
statements we have proved are right.
But are we really understanding our statements? is like "requirements
bug" in software programming.
See the proof in "action" may help ourselves to understand our statements.