Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] survey on Coq interfaces

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] survey on Coq interfaces


chronological Thread 
  • From: Marco Servetto <marco.servetto AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] survey on Coq interfaces
  • Date: Sun, 4 Dec 2011 20:14:13 +0100

>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.




Archive powered by MhonArc 2.6.16.

Top of Page