3 ms·
It’s enough of an issue for C at least that a fully formally verified compiler exists: https://en.m.wikipedia.org/wiki/CompCert https://en.m.wikipedia.org/wiki/
by dbaupp 6y ago
It’s enough of an issue for C at least that a fully formally verified compiler exists: https://en.m.wikipedia.org/wiki/CompCert https://en.m.wikipedia.org/wiki/CompCert . That is, there’s proof that its (limited) optimisation passes are correct.
There’s other approaches to assurance of compiled code too, such as seL4 which has proofs that the binary itself is correct, I believe.
- astrange 6y agoNote that fuzzing CompCert has still found bugs in it - because the entire compiler actually isn't verified. They've extended the proof over time. (Note that "formally verified" still does not mean "bug free", it just means it's a refinement of a proof that is also a program which can have bugs in it. And "formally" sounds like a weasel word.)
- dbaupp 6y agoAh, thanks for the clarification!
- ralfj 6y agoYeah, there were some bugs in the frontend and I think one in the backend. But there were zero bugs in the optimization pipeline, which is where typically the most subtle bucks lurk. For more details, see https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf