coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] survey on Coq interfaces, Aaron Stump
- Re: [Coq-Club] survey on Coq interfaces,
Mihai ANDRIES
- Re: [Coq-Club] survey on Coq interfaces,
Adam Chlipala
- Re: [Coq-Club] survey on Coq interfaces,
Mihai ANDRIES
- Re: [Coq-Club] survey on Coq interfaces,
Adam Chlipala
- Re: [Coq-Club] survey on Coq interfaces, Marco Servetto
- Re: [Coq-Club] survey on Coq interfaces,
Ramana Kumar
- Re: [Coq-Club] survey on Coq interfaces, Marco Servetto
- Re: [Coq-Club] survey on Coq interfaces,
Ramana Kumar
- Re: [Coq-Club] survey on Coq interfaces, Marco Servetto
- Re: [Coq-Club] survey on Coq interfaces,
Adam Chlipala
- Re: [Coq-Club] survey on Coq interfaces,
Mihai ANDRIES
- Re: [Coq-Club] survey on Coq interfaces,
Adam Chlipala
- Re: [Coq-Club] survey on Coq interfaces,
Mihai ANDRIES
Archive powered by MhonArc 2.6.16.