3 ms·
...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 shoul
by 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