The Coq mailing list

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

I'm familiar with programming, and I'm familiar with formal methods, but I have trouble understanding the various Coq tutorials.

What prevents me from cheating by assuming enough hypotheses that my goal is reached?

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?

I'm used to unit testing my programs with 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? 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?

Cheers,

Andrew Pennebaker

www.yellosoft.us