8 ms·

How does one prove the correctness of the correctness proofs?

• jkhdigital 5y ago
  Gotta formally verify the source code of the proof checker… then the entire bootstrapped tool chain that was needed to compile it. No big deal
• junon 5y ago
  Generally using a language like OCaml, which is the language of choice for most large formal proofing projects.
• AmericanChopper 5y ago
  You can’t. The headline is missing a piece of context in that the proved it was free of runtime errors… according to a specification they chose to evaluate it against. What if their specification contained an error? You could verify that specification against another specification, you could even do that formally if you want to. Eventually you have to confront Gödel’s incompleteness theorem, and accept that such a level of proof is not possible. Formal verification btw is just a formalised methodology for evaluating something against a specification. It doesn’t prove that errors don’t exist, or that the verifier hasn’t managed to independently make their own error. It’s just a rigorous PR.
• pharmakom 5y ago
  The idea is that we have more confidence in the model and model checker than the actual code. At the very least, this is a form of double entry.