5 ms·

COGENT: Certified Compilation for a Functional Systems Language

60 points by luu 11y ago

eatonphil 11y ago
I'm having trouble finding information on the language they are talking about. It doesn't seem like the language (COGENT) is presented in this paper, just a compiler for language. Is there a page on the language itself? A quick Google search shows only completely unrelated results. There is another language CoGenT[0] at UMass, but it is not the same thing. [0] https://people.cs.umass.edu/~trekp/cogent-manual.pdf https://people.cs.umass.edu/~trekp/cogent-manual.pdf
- drostie 11y ago
  It is defined in this paper itself; see section 3 titled "Language," beginning "In this section we formally define Cogent, including its linear type system, its two dynamic semantics — update and value — mentioned earlier in §2, and the refinement theorem between them." Also see figure 5, which is its formal syntax after desugaring.
  - eatonphil 11y ago
    Thanks for that, should have read a little further.
    - deleted 11y ago
      [deleted]
kmicklas 11y ago
It looks like they have an unverified compiler, which assuming correctness of the compiler code, will produce a proof of correctness for each program it compiles. This is significantly less cool and useful than proving that the compiler itself is correct.
- rntz 11y ago
  No, the proof that the compiled code is "correct" does not depend on the compiler being correct - it can be checked independently. Of course, if the compiler is incorrect it might generate incorrect code, but then the "proof" that the code is correct would not check. Mind you, it's very ambiguous to describe what their compiler is doing as producing a proof of "correctness". Any time someone says "correct", you should ask, "correct with respect to what?" In this case, AIUI, their compiler produces: (a) a formal description of what the program does (what they call "a high-level shallow embedding of the program's semantics") (b) a proof that this is in fact what the program does (its "correctness") The idea being that if you want to show that your program is actually correct with respect to the specification you really care about, you do the proof on the formal description (a), and then (b) automatically guarantees your proof carries over to the actual program.
  - kmicklas 11y ago
    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
        11y ago
nickpsecurity 11y ago
Really good stuff. Here I am waiting to see what Leroy et al will deliver on mini-ML compiler or more from Habit team when Klein et al deliver a systems-oriented, certified compiler. Heck yeah! Interesting, too, in that it splits the supporting argument between the functional language and stuff in C. Its focus on being essentially an executable spec with verified translations will help in high assurance where spec to implementation correspondence is quite important. Could be a shortcut when this produces acceptable implementations.

60 points by luu 11y ago

I'm having trouble finding information on the language they are talking about. It doesn't seem like the language (COGENT) is presented in this paper, just a compiler for language. Is there a page on the language itself? A quick Google search shows only completely unrelated results. There is another language CoGenT[0] at UMass, but it is not the same thing. [0] https://people.cs.umass.edu/~trekp/cogent-manual.pdf https://people.cs.umass.edu/~trekp/cogent-manual.pdf

drostie 11y ago
It is defined in this paper itself; see section 3 titled "Language," beginning "In this section we formally define Cogent, including its linear type system, its two dynamic semantics — update and value — mentioned earlier in §2, and the refinement theorem between them." Also see figure 5, which is its formal syntax after desugaring.
- eatonphil 11y ago
  Thanks for that, should have read a little further.
  - deleted 11y ago
    [deleted]

kmicklas 11y ago

It looks like they have an unverified compiler, which assuming correctness of the compiler code, will produce a proof of correctness for each program it compiles. This is significantly less cool and useful than proving that the compiler itself is correct.

rntz 11y ago
No, the proof that the compiled code is "correct" does not depend on the compiler being correct - it can be checked independently. Of course, if the compiler is incorrect it might generate incorrect code, but then the "proof" that the code is correct would not check. Mind you, it's very ambiguous to describe what their compiler is doing as producing a proof of "correctness". Any time someone says "correct", you should ask, "correct with respect to what?" In this case, AIUI, their compiler produces: (a) a formal description of what the program does (what they call "a high-level shallow embedding of the program's semantics") (b) a proof that this is in fact what the program does (its "correctness") The idea being that if you want to show that your program is actually correct with respect to the specification you really care about, you do the proof on the formal description (a), and then (b) automatically guarantees your proof carries over to the actual program.
- kmicklas 11y ago
  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
      - 11y ago

nickpsecurity 11y ago

Really good stuff. Here I am waiting to see what Leroy et al will deliver on mini-ML compiler or more from Habit team when Klein et al deliver a systems-oriented, certified compiler. Heck yeah! Interesting, too, in that it splits the supporting argument between the functional language and stuff in C. Its focus on being essentially an executable spec with verified translations will help in high assurance where spec to implementation correspondence is quite important. Could be a shortcut when this produces acceptable implementations.