The Coq mailing list

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

The Bedrock project <http://plv.csail.mit.edu/bedrock/> involves 
embedding programming languages inside of Coq.  We implement, compile, 
specify, and verify code inside of Coq.  There's no separate step of 
parsing programs with a special tool, as we just use Coq's extensible 
parser for that task.

A related system dealing with more conventional languages is the 
Verified Software Toolchain <http://vst.cs.princeton.edu/> for C, which 
interfaces with CompCert <http://compcert.inria.fr/>.

Compared to Frama-C & Why (mentioned in a previous response), the 
systems I've suggested are distinguished by having much smaller trusted 
code bases.  You don't need to worry about bugs in verification tools 
(beside the Coq kernel) leading you to accept a false theorem.

On 08/28/2014 05:49 PM, Ömer Sinan Ağacan 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.