The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi andrew,

You may want to have a look at the "related tools" page on coq's
website [1]. If you are looking to certify C code than Frama-C [2]
(Caduceus' successor) looks like a safe bet.

Cheers,

--
guillaume

[1] http://coq.inria.fr/related-tools
[2] http://frama-c.com/

On 1 November 2011 23:32, Andrew Pennebaker 
<andrew.pennebaker AT gmail.com>
 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?
>
> 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.
>
>
>