3 ms·
He also points to Compcert: a certified compiler for a subset of C. The compiler is specified, programmed and proved in Coq. It is a really impressive project:
by primodemus 16y ago
He also points to Compcert: a certified compiler for a subset of C. The compiler is specified, programmed and proved in Coq. It is a really impressive project: http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html
- rwmj 16y agoCompcert is great (it's by the same team who do OCaml). Unfortunately however it's not free software.