Hacker News Reader

It will be interesting to see once it becomes open source.

My favorite story relating to that is john regher compiler testing effort found a bunch of bugs in a research compiler that was proved to be correct.

[Edit]

Not strictly true. As John noted in comment below:

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

View on HN

actually that story is the opposite of true. John Regher and CSmith fuzzed CompCert and they found no bugs. from the csmith PLDI paper:

"The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task."

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

My error.

Sounds interesting -- is there a paper that describes this?

I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

Reply on news.ycombinator.com