The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrew Pennebaker wrote:
> What prevents me from cheating by assuming enough hypotheses that my 
> goal is reached?

This changes the theorem statement into an implication over your 
hypotheses.  Coq allows asserting axioms that don't appear in a 
theorem's statement, but the command "Print Assumptions" shows which 
axioms a proof depends on, so it's pretty easy to understand which facts 
you're assuming, given a proof as a black box.

> How can Coq A) prove that an algorithm for reversing a string is 
> correct and B) prove that a C implementation of the algorithm is correct?

Neither question admits a short answer.  Especially the latter is an 
open question, so far as figuring out the best way to do it.

I would hope that CPDT <http://adam.chlipala.net/cpdt/> gives enough 
information to answer the first question.  (If not, please let me know 
what's missing!)

Bedrock <http://adam.chlipala.net/bedrock/> is my work-in-progress on 
tools for verifying C-like programs in Coq.

> I'm used to unit testing my programs with QuickCheck 
> <http://www.yellosoft.us/quickcheck>, a probabilistic verifier that 
> brute forces properties such as |propReversible :: String -> Bool| 
> (Haskell notation). How easy would it be to refactor QuickCheck tests 
> into Coq tests?

I assume there is no deep technical challenge in porting QuickCheck to 
Coq, but we care less about tests when we prove program correctness.  I 
don't know of an extant QuickCheck-for-Coq implementation.

> If Coq verifies that my C code is correct, how should I provide 
> "certificates" of verification? Is it enough to provide a code comment 
> to a URL of a .v file?

I don't know of any standard for such a communication.  There are many 
exercises you can carry out to increase your confidence in the 
correctness of a piece of software, but your question seems somewhat 
ill-formed without information on who you are trying to convince and of 
what.