The Coq mailing list

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

Andrew Pennebaker wrote:
> 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?

I've never meant to claim that CPDT is meant to explain how to use Coq 
to verify C-like programs.  There are many interesting applications for 
Coq, and no book could hope to cover them all.  I also expect only a 
minority of CPDT readers are interested in verifying C programs.  For 
these reasons, I'm not planning to add any extra coverage of the topic.

I do expect, however, that Bedrock will grow more documentation at some 
point. ;)

> Have you used QuickCheck 
> <http://www.haskell.org/haskellwiki/Introduction_to_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!

OK, so I think you're saying that QuickCheck users are already writing 
specifications, so we could hope to write an automatic translator of 
those specifications into Coq, to give us a head start on deciding which 
theorems to prove.  That seems reasonable.  Keep in mind, though, that 
neither of Haskell and Coq is a subset of the other.  In particular, 
translating Haskell into Coq is tricky, because Coq requires 
syntactically apparent termination of all programs.  I can believe a 
reasonably effective solution could exist that translates Haskell 
programs, with their QuickCheck specs, into Coq; but, really, I would 
recommend doing everything in Coq in the first place, and possibly 
extracting to Haskell afterward.  Writing simple, QuickCheck-style specs 
isn't very time-consuming.

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

Perhaps you would like to read about the idea of proof-carrying code (PCC):
    http://www.eecs.berkeley.edu/~necula/pcc.html

And some more recent work on _foundational_ PCC:
    http://flint.cs.yale.edu/
    http://sip.cs.princeton.edu/projects/pcc/

(Quick answer to part of your question: Coq-based solutions will almost 
certainly involve distributing .vo files, not .v files.)