The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

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