5 ms·

Yes, that's exactly what I meant. But compare this to CompCert. CompCert itself is verified, which means it doesn't have to output a proof for each program it c

Yes, that's exactly what I meant. But compare this to CompCert. CompCert itself is verified, which means it doesn't have to output a proof for each program it compiles. Even if you don't care about the theoretical concerns of for all vs for each, there are two practical concerns with this kind of system. 1) the compiler could just fail to output a valid proof for some program and you're out of luck until the compiler bug is fixed. 2) Proof checking can get pretty time intensive and it'd be better to do it once for the compiler, than every time you run the compiler.

rntz 11y ago
Indeed, but proving a whole compiler correct is really hard. :P
- dbpokorny 11y ago
  Not if you start with a small compiler
  - nickpsecurity 11y ago
    No, it's still hard. The best approach I've seen to this outside CompCert is a project that independently tried my own recommendation of breaking it into stages then using whatever verification works on a per stage basis. So, one prover and approach works best for Stage 1. Then another maybe for Stage 2. Some compositional method to tie them together. They were making a MIPS compiler. Got pretty far in short time paper covered with a fraction of CompCert's effort. Nonetheless, the untrusted compiler plus trusted checker method has the most supporting evidence in literature for getting the job done and ease of building. So, even my recommendation should take that approach where possible.
    - Ericson2314 11y ago
      It's hard, but I've for awhile thought that developing these tools in a more bottom-up would help. And of course orthogonal components, as you say, is a good idea for just about anything.
      - nickpsecurity 11y ago
        I don't agree. Matter of fact, I recommended it here in an answer to the reproducible build meme that pops up. See my conversation with jeffreyrogers here: https://news.ycombinator.com/item?id=10182282 https://news.ycombinator.com/item?id=10182282
      - nickpsecurity 11y ago
        Looking back at it, I meant to say "I don't disagree. I had made similar recommendations before." Totally changes meaning of comment till you click the link haha.
cwzwarich 11y ago
Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in optimization and code generation: http://compcert.inria.fr/doc/html/Compiler.html http://compcert.inria.fr/doc/html/Compiler.html As one particular example, register allocation is performed by an untrusted oracle that may not even terminate, and then verified a posteriori: http://compcert.inria.fr/doc/html/Allocation.html http://compcert.inria.fr/doc/html/Allocation.html They proved a traditional register allocator correct in a paper (https://www.cs.princeton.edu/~appel/papers/regalloc.pdf https://www.cs.princeton.edu/~appel/papers/regalloc.pdf), but I guess there are practical reasons why they are not using it in CompCert by default.

rntz 11y ago

Indeed, but proving a whole compiler correct is really hard. :P

dbpokorny 11y ago
Not if you start with a small compiler
- nickpsecurity 11y ago
  No, it's still hard. The best approach I've seen to this outside CompCert is a project that independently tried my own recommendation of breaking it into stages then using whatever verification works on a per stage basis. So, one prover and approach works best for Stage 1. Then another maybe for Stage 2. Some compositional method to tie them together. They were making a MIPS compiler. Got pretty far in short time paper covered with a fraction of CompCert's effort. Nonetheless, the untrusted compiler plus trusted checker method has the most supporting evidence in literature for getting the job done and ease of building. So, even my recommendation should take that approach where possible.
  - Ericson2314 11y ago
    It's hard, but I've for awhile thought that developing these tools in a more bottom-up would help. And of course orthogonal components, as you say, is a good idea for just about anything.
    - nickpsecurity 11y ago
      I don't agree. Matter of fact, I recommended it here in an answer to the reproducible build meme that pops up. See my conversation with jeffreyrogers here: https://news.ycombinator.com/item?id=10182282 https://news.ycombinator.com/item?id=10182282
    - nickpsecurity 11y ago
      Looking back at it, I meant to say "I don't disagree. I had made similar recommendations before." Totally changes meaning of comment till you click the link haha.

cwzwarich 11y ago

Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in optimization and code generation: http://compcert.inria.fr/doc/html/Compiler.html http://compcert.inria.fr/doc/html/Compiler.html As one particular example, register allocation is performed by an untrusted oracle that may not even terminate, and then verified a posteriori: http://compcert.inria.fr/doc/html/Allocation.html http://compcert.inria.fr/doc/html/Allocation.html They proved a traditional register allocator correct in a paper (https://www.cs.princeton.edu/~appel/papers/regalloc.pdf https://www.cs.princeton.edu/~appel/papers/regalloc.pdf), but I guess there are practical reasons why they are not using it in CompCert by default.