3 ms·

Writing a Compiler by Proving It Correct

139 points by kachnuv_ocasek 11y ago

hbbio 11y ago
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 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.
- mafribe 11y ago
  CompCert There's now a lot of work in this space, e.g. http://sf.snu.ac.kr/sepcompcert 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 http://fbinfer.com) and Microsoft (https://www.fstar-lang.org https://www.fstar-lang.org) use it, but sparingly.
  - cwzwarich 11y ago
    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.
    - mafribe 11y ago
      I agree, FB Infer is not a certifying compiler, but it's based on program logic.
  - truncate 11y ago
    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/sound-verification.pdf https://lirias.kuleuven.be/bitstream/123456789/471365/3/soun...
  - nickpsecurity 11y ago
    Even more interesting from sepcompcert team: http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf
nv-vn 11y ago
This got me thinking, how feasible would an implementation of APL be as a DSL embedded inside of Agda (or some other similar language)?
fizixer 11y ago
And there's not one mention of the word 'optimization'.
skybrian 11y ago
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.
- bweitzman 11y ago
  Replace `find [] s = nothing` with `find [] s = left ("variable " ++ s ++ " not defined")` (assuming types/functions similar to Haskell, I don't actually know Agda)

139 points by kachnuv_ocasek 11y ago

hbbio 11y ago

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 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.

mafribe 11y ago
CompCert There's now a lot of work in this space, e.g. http://sf.snu.ac.kr/sepcompcert 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 http://fbinfer.com) and Microsoft (https://www.fstar-lang.org https://www.fstar-lang.org) use it, but sparingly.
- cwzwarich 11y ago
  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.
  - mafribe 11y ago
    I agree, FB Infer is not a certifying compiler, but it's based on program logic.
- truncate 11y ago
  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/sound-verification.pdf https://lirias.kuleuven.be/bitstream/123456789/471365/3/soun...
- nickpsecurity 11y ago
  Even more interesting from sepcompcert team: http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf

nv-vn 11y ago

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

fizixer 11y ago

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

skybrian 11y ago

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.

bweitzman 11y ago
Replace `find [] s = nothing` with `find [] s = left ("variable " ++ s ++ " not defined")` (assuming types/functions similar to Haskell, I don't actually know Agda)