3 ms·
Except for compcert, which is basically perfect.
by thechao 6y ago
Except for compcert, which is basically perfect.
- jraph 6y agoWell, not quite, because there are parts of CompCert that are not proven [1]: - Parsing, type-checking, and pre-simplifications - Assembling and linking And there have been bugs on edge cases there. Moreover, correctness is limited to what is specified. COQ does not guarantee that there are no missing specifications or theorems. The C standard is written in English, people had to manually encode the standard in COQ. [1] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html
- touisteur 6y agoAnd the performance of the generated binary might be underwhelming for some.