3 ms·

Yes. CompCert is a project of the French research institute in computer science and automation (INRIA). The goal is to have a certified compiler for the C progr

by p4bl0 15y ago

Yes. CompCert is a project of the French research institute in computer science and automation (INRIA). The goal is to have a certified compiler for the C programming language. I believe they're writing a C compiler in Coq (a proof assistant also developped mainly at INRIA). The main guy behind CompCert is Xavier Leroy (already known for OCaml).

MostAwesomeDude 15y ago
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.
- justincormack 15y ago
  What does it do about the undefined behaviour parts of the spec?
  - beza1e1 15y ago
    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.
  - skew 15y ago
    You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_program_correct 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.
nakkiel 15y ago
There's a list of papers published on his page: http://cristal.inria.fr/~xleroy/ I keep this link in a feel-good folder, next to Bellard's page. Sometimes I need a feel-good break after reading US-centric news.

by p4bl0 15y ago

MostAwesomeDude 15y ago

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.

justincormack 15y ago
What does it do about the undefined behaviour parts of the spec?
- beza1e1 15y ago
  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.
- skew 15y ago
  You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_program_correct 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.

nakkiel 15y ago

There's a list of papers published on his page: http://cristal.inria.fr/~xleroy/ I keep this link in a feel-good folder, next to Bellard's page. Sometimes I need a feel-good break after reading US-centric news.