4 ms·

This old Knuth quote seems apt: "Beware of bugs in the above code; I have only proved it correct, not tried it."

cwzwarich 15y ago
That seems like it either a statement about the nature of informal proof or the disconnect between the proof and the code. How does that apply to something written in Coq, where the program is extracted from a mechanically verified proof?
- shasta 15y ago
  Mechanical proof of what, though? The spec can fail to capture intent.
  - njs12345 15y ago
    In this case, the semantics of the C subset chosen are captured perfectly by the assembly produced by the compiler. Seems like that's the intent of a compiler to me :)
    - shasta 15y ago
      Right, but first you have to specify "the semantics of C" and "the semantics of assembly". How do you prove you did that right?
      - njs12345 15y ago
        The semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PPC/ARM or whatever but some subset with defined semantics which happen to line up perfectly with observed behaviour). The first is fine I think (accepting a subset you define formally); the second is an issue but it's currently impossible to do any better. Still, if you look at this compared to the backends of LLVM and GCC it's certainly an improvement.
      - cwzwarich 15y ago
        Compcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final statement of the semantic preservation theorem). Specifying such a semantics is basically like writing a very simple functional interpreter for the language. I don't see how it could get much simpler. Here is the description of the semantics for their input language: http://compcert.inria.fr/doc/html/Csem.html http://compcert.inria.fr/doc/html/Csem.html and their PPC output: http://compcert.inria.fr/doc/html/Asm.html http://compcert.inria.fr/doc/html/Asm.html
        shasta 15y ago
        Yes. The approach is probably as good as it can get. And yet, it's not perfect. That functional interpreter could have a bug. And thus Knuth's quote is applicable. Testing the compiler could reveal to you that your specification wasn't really what you intended.
  - archgoon 15y ago
    Then the spec is wrong, and there are no correct compilers.
    - shasta 15y ago
      There is already a C spec and it isn't formalized in coq. You can formalize it incorrectly.

That seems like it either a statement about the nature of informal proof or the disconnect between the proof and the code. How does that apply to something written in Coq, where the program is extracted from a mechanically verified proof?

shasta 15y ago
Mechanical proof of what, though? The spec can fail to capture intent.
- njs12345 15y ago
  In this case, the semantics of the C subset chosen are captured perfectly by the assembly produced by the compiler. Seems like that's the intent of a compiler to me :)
  - shasta 15y ago
    Right, but first you have to specify "the semantics of C" and "the semantics of assembly". How do you prove you did that right?
    - njs12345 15y ago
      The semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PPC/ARM or whatever but some subset with defined semantics which happen to line up perfectly with observed behaviour). The first is fine I think (accepting a subset you define formally); the second is an issue but it's currently impossible to do any better. Still, if you look at this compared to the backends of LLVM and GCC it's certainly an improvement.
    - cwzwarich 15y ago
      Compcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final statement of the semantic preservation theorem). Specifying such a semantics is basically like writing a very simple functional interpreter for the language. I don't see how it could get much simpler. Here is the description of the semantics for their input language: http://compcert.inria.fr/doc/html/Csem.html http://compcert.inria.fr/doc/html/Csem.html and their PPC output: http://compcert.inria.fr/doc/html/Asm.html http://compcert.inria.fr/doc/html/Asm.html
      - shasta 15y ago
        Yes. The approach is probably as good as it can get. And yet, it's not perfect. That functional interpreter could have a bug. And thus Knuth's quote is applicable. Testing the compiler could reveal to you that your specification wasn't really what you intended.
- archgoon 15y ago
  Then the spec is wrong, and there are no correct compilers.
  - shasta 15y ago
    There is already a C spec and it isn't formalized in coq. You can formalize it incorrectly.