News for hackers. Stuff that matters.

A comment on Pointers Are Complicated II, or: We need better language specs. Parent comment

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 ]