5 ms·
CompCert (http://compcert.inria.fr/doc/index.html http://compcert.inria.fr/doc/index.html) is a "real-world", optimizing compiler the core of which was written
by panic 13y ago
CompCert (http://compcert.inria.fr/doc/index.html http://compcert.inria.fr/doc/index.html) is a "real-world", optimizing compiler the core of which was written and verified using Coq.
- rwmj 13y agoI love the idea at least of CompCert, but I really wish it was open source. I could drive adoption within Red Hat and in key open source projects tomorrow if it was.
- betterunix 13y ago...why not duplicate the effort as an open source project? Coq, ACL2, and PVS are all open source. Writing a C compiler is certainly not trivial, but it should not take a good programmer more than a few months to do so (including the time needed to learn Coq/ACL2/PVS).
- jbapple 13y agoI think that really trivializes the tremendous effort the CompCert team put into that work. You don't just need to write a C compiler, or learn a bit of a proof assistant, you need to do the actual work of proving the compiler correct. This took person-years of time from people who already were Coq experts.
- vilhelm_s 13y agoFormally verifying software takes much more time than just writing it, perhaps a factor of 10. For instance, the seL4 project[1] states that they used 2.2 person-years to write the kernel itself, and 20 person-years on the proof. Apparently the version of CompCert from 2007 (before any optimizations) took 2 person-years to write[2]. But some of those persons were pretty impressive. [1] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [2] http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf http://memocode.irisa.fr/2007/leroy-compcert-memocode07.pdf