Hacker News new | past | comments | ask | show | jobs | submit login

It’s enough of an issue for C at least that a fully formally verified compiler exists: 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.




Note 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.)


Yeah, 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


Ah, thanks for the clarification!




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: