3 ms·
I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
by Cu3PO42 5y ago
I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
- MaxBarraclough 5y agoAlso, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html https://compcert.org/motivations.html I think things may have improved further since the 2011 paper, where they found bugs in parts of CompCert which were not, at the time at least, formally verified. The formally verified parts of CompCert withstood torture testing admirably.
- pfdietz 5y agoPLDI does a "most influential paper" award each year, for the paper from the PLDI 10 years previous that had the most influence. The 2021 winner was that paper.