Interesting work. I don't remember who said that "formal verification is the way of the future... and it's going to stay that way!"<p>Quite strange that the article doesn't mention CompCert though, which has an extensive bibliography:<p><a href="http://compcert.inria.fr/publi.html" rel="nofollow">http://compcert.inria.fr/publi.html</a><p>Edit: The person I quote is a researcher in formal verification, I think it's Gérard Huet from Inria.
It looks like this compiler never actually reports any errors. (It uses the Maybe type, so you just get nothing.)<p>I appreciate that it's a toy compiler, but I really wish people wouldn't leave that out. The quality of a compiler's user interface almost entirely depends on its error messages, so it's important to demonstrate how that's done.