CompCert - Compilers you can formally trust

Re:CompCert - Compilers you can formally trust by MostAwesomeDude on Saturday June 04, 2011 @02:01PM (#2620006)

Yeah, the big thing here is that almost all of this thing is proven, meaning that the compiler's behavior is well-defined and correct, all the time, on all inputs.

I still had a jaw-drop moment the first time I heard about this; Coq is not a pleasant language, and proving this thing must have been a nightmare.

[ Parent | on HN ]

Re:CompCert - Compilers you can formally trust by justincormack on Saturday June 04, 2011 @02:57PM (#2620178)

What does it do about the undefined behaviour parts of the spec?

[ Parent | on HN ]

Re:CompCert - Compilers you can formally trust by skew on Saturday June 04, 2011 @08:58PM (#2620929)

You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_pro...

A C compiler doesn't have to promise much of anything about the behavior of the code produced for a program with undefined behavior.

This statement could be vacuous for a program p with undefined behavior if (Cstrategy.exec_program p beh) isn't true for any behavior beh, or only true for a behavior which makes (not_wrong beh) false.

If they don't always, then they actually give you a guarantee for some bad programs as well. Nothing in the spec says running a bad program has to make demons fly out your nose.

[ Parent | on HN ]

Re:CompCert - Compilers you can formally trust by beza1e1 on Saturday June 04, 2011 @03:20PM (#2620231)

The frontend is not verified. This part parses, checks and lowers C code to a Clight. There is no formal specification of C itself and that would be the first step to verify the frontend.

[ Parent | on HN ]