The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I think a combination of Frama-C ( http://frama-c.com/ ) and Why (
http://why.lri.fr/ ) could be used for verifying C programs using Coq.
I haven't tried either myself, though.
-- 
Daniel Schepler

On Thu, Aug 28, 2014 at 2:49 PM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 wrote:
> Proving on Coq functions and later extracting OCaml/Haskell programs
> is useful but I think lots of interesting stuff and opportunities for
> verification/proving are happening outside of Coq world.
>
> For example, I may want to prove that a type checker implemented in
> Haskell really checks for compliance of a particular type system. Type
> system definition may be given in Coq and progress, preservation etc.
> properties may be proven in standard way. To prove this, I need to
> somehow express propositions on Haskell programs and give proofs of
> them.
>
> Another example may be proving some properties of algorithms written
> in C, running on an embedded device etc.
>
> I'm wondering how these could be done and if anyone's doing that.
>
> I have something like this is mind:
>
> * As a first step, we need to define the language in Coq. Not just
> syntax but we need execution/evaluation rules in all details. (should
> be very painful to do for languages like C, relations should be very
> carefully crafted so that undefined behaviors are excluded etc.)
> * We should be able to parse programs written in the language and have
> a term in Coq.
> * The rest should be same. Except it's be much harder than doing same
> thing on Coq programs.
>
> If such a thing is possible right now, can anyone give me some
> pointers to follow? Thanks.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net