The Coq mailing list

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

Thanks for the pointers. I just skimmed over them and I guess what I
imagined was something between Bedrock(happens inside Coq) and
Frama-C(the programming language is C and not some language specific
to the verification tool, no extraction). Since we don't have what I
imagined, I'll start with Frama-C.

---
Ömer Sinan Ağacan
http://osa1.net


2014-08-29 1:29 GMT+03:00 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.