The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

Thanks for the quick reply, CPDT is fascinating. I suspect that other readers similarly wonder, "How does proving an algorithm in Coq certify that my C program is correct?" In future editions, could you include Bedrock examples?

Have you used QuickCheck? I'm not asking to port QuickCheck to Coq, as a brute-force checker would seem redundant to add it to a program verifier. QuickCheck might be a handy tool to check for trivial errors in proofs, but it's by no means a Coq tactic, unless there are negative tactics!

How easy do you think it would be to rewrite calls to the QuickCheck API as calls to the Coq or Bedrock API, given that QuickCheck and Coq seem to do the same thing. QuickCheck tests "properties", Coq tests "propositions". The former uses a brute-force/probabilistic method, the latter uses induction.

A short, pseudocode example of the QuickCheck API (QuickCheck has been ported to several languages).

> bool is_even(int n) = n % 2 == 0
> int gen_int() = random_integer()
> for_all(is_even, { gen_int })
*** Failed!
57

Here, the QuickCheck function forAll generates 100 test cases using the supplied generator functions. In other words, QuickCheck calls is_even(gen_int()) 100 times, supplying random integers to is_even each time. QuickCheck saw that is_even(57) returns false, that the property is_even fails to hold. In Haskell, QuickCheck will even attempt to simplify test cases to the bare minimum failing test case for easier debugging of properties. Haskell can also find out how to generate test cases for arbitrarily-typed propositions.

Hmm, the few programmers who do care about correctness seem to limit themselves to a handful of manual assert() statements. How can we evangelize Coq as an additional testing tool? How exactly can we replace those assertions with Coq proofs?

To clarify my last question, imagine you're a developer at CoolStuff.org. You want to advertise just how safe and correct your software is. Do you, for example, link to a Coq vernacular file on your Products page? If your software is open source, do you link to a vernacular file in a comment section of your code?

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Tue, Nov 1, 2011 at 1:40 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.