Hacker News Reader

Comment by feider | Hacker News Reader

From CompCert site: "What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues."

I'm not very into C language - what are these miscompilation issues? What is the practical impact that CompCert C brings?

View on HN

Miscompilation issues means bugs in the compiler causing incorrect assembly to be generated.

I understood that. Sorry if my question was bit unclear. What I wanted to know was _specifically_ what these bugs are / what causes them / what is practical impact (i.e. probability of application crashing or other serious event due to use of GCC etc)

Check out "Finding and Understanding Bugs in C Compilers": http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf.

The paper explains what-is-bug/what-causes-it/what-is-impact for selected bugs. Complete list of 282 compiler bugs found (79 GCC, 203 LLVM) is also available online: http://embed.cs.utah.edu/csmith/.

Thank you, that paper seems to be surprisingly easy to read (being an academic paper that is).

Especially see the CompCert section on page 6 of the Csmith PDF to see what a difference formal verification made. Note that compilers don't have to go that far: typed, functional, thoroughly-tested code in something like Ocaml or Haskell can achieve 80-90% of that quality with relatively little effort. Hence, why I promote rewriting and further extending things like LLVM in languages like ML, Ada, or Eiffel that support advanced checks.

Reply on news.ycombinator.com