The Coq mailing list

[Ramana Kumar <ramana.kumar AT gmail.com>]

On Sun, Dec 4, 2011 at 7:14 PM, Marco Servetto 
<marco.servetto AT gmail.com>
 wrote:
>>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.
>

I would suggest that making use of the statements is a better way to
understand them and make sure they are right than stepping through
their proof. For example, if you prove a lemma and that enables you to
prove your main theorem, then it's likely the lemma statement was
correct. If you make a definition and you can subsequently prove lots
of unsurprising "sanity test" results about it, then it's likely the
definition was correct.