Pointers Are Complicated II, or: We need better language specs

Re:Pointers Are Complicated II, or: We need better language ... by dbaupp on Monday December 14, 2020 @02:44PM (#25422231)

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.

[ Parent | on HN ]

Re:Pointers Are Complicated II, or: We need better language ... by astrange on Monday December 14, 2020 @08:24PM (#25425881)

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

[ Parent | on HN ]

Re:Pointers Are Complicated II, or: We need better language ... by ralfj on Tuesday December 15, 2020 @07:37AM (#25429697)

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

[ Parent | on HN ]

Re:Pointers Are Complicated II, or: We need better language ... by dbaupp on Tuesday December 15, 2020 @03:39AM (#25428277)

Ah, thanks for the clarification!

[ Parent | on HN ]