3 ms·
Nope. CompCert (a C compiler) has zero bugs. It is formally proven correct down to assembler level.
by mbrodersen 5y ago
Nope. CompCert (a C compiler) has zero bugs. It is formally proven correct down to assembler level.
- mikewarot 5y agoI just cringe at the thought of making that bold of a claim on anything computer related, let alone something as complex as a compiler. So, as long as the specifications, and CPU documentation are correct, it will work as intended, a high percentage of the time. (Random bit flips, disk errors, etc. are still a thing)
- mbrodersen 5y agoI highly recommend learning more about what formal software verification actually is and what it guarantees and what it doesn’t.