Writing a Compiler by Proving It Correct | Hacker News Reader

Writing a Compiler by Proving It Correct

liamoc.net

139 pointskachnuv_ocasek10 comments

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!"

Quite strange that the article doesn't mention CompCert though, which has an extensive bibliography:

http://compcert.inria.fr/publi.html

Edit: The person I quote is a researcher in formal verification, I think it's Gérard Huet from Inria.

   CompCert

There's now a lot of work in this space, e.g. http://sf.snu.ac.kr/sepcompcert

   and it's going to stay that way!

Whoever said this has been proven wrong. This stuff works, it's just expensive. The only real question is: when will formal verification be convenient enough to be widely used in industry. I reckon that's 15-20 years away. Right now organisations like Facebook (http://fbinfer.com) and Microsoft (https://www.fstar-lang.org) use it, but sparingly.

Facebook's Infer is just an ordinary static analysis tool, albeit one inspired by separation logic. It is unsound and does not prove that code is correct.

I agree, FB Infer is not a certifying compiler, but it's based on program logic.

The problem is most languages we use are not very safe, and which means if you have one unverified part in code, you can't prove code correct. I read a paper recently which tried to do modular verification of C by adding runtime contracts are boundaries[1]. Theory wise its sound, but it's really slow. You may even have to rewrite code certain ways to make it perform better.

[1] https://lirias.kuleuven.be/bitstream/123456789/471365/3/soun...

Even more interesting from sepcompcert team:

http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf

It looks like this compiler never actually reports any errors. (It uses the Maybe type, so you just get nothing.)

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.

Replace `find [] s = nothing` with `find [] s = left ("variable " ++ s ++ " not defined")`

(assuming types/functions similar to Haskell, I don't actually know Agda)

This got me thinking, how feasible would an implementation of APL be as a DSL embedded inside of Agda (or some other similar language)?

And there's not one mention of the word 'optimization'.

Reply on news.ycombinator.com