9
$\begingroup$

In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:

  1. VCGen to generate verification conditions (safety predicates)
  2. First-order logic theorem prover to prove the conditions
  3. LF proof checker to check the proof from step (2)

I am a bit confused by step (3). Why is it required at all? Will just (1) and (2) not suffice? Why don't we just trust the proof generated by a theorem prover?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
19
$\begingroup$

The purpose of the proof checker is to minimise the trusted computing base.

By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on Page 3:

Neither the compiler nor the prover need to be correct in order to be guaranteed to   
detect incorrect compiler output. This is a significant advantage since the VCGen and  
the  proof checker are significantly simpler than the compiler and the prover.

A proof checker is just a couple of lines of code, and can be hand-inspected for correctness. In contrast, an automated prover that performs well is extremely complex and unlikely to be correct, although with well-tested and widely used provers, the mistakes will be in edge cases that might not be easy to trigger. Have a look at the 30k LOC C code that make up Lingeling, a state-of-the-art SAT solver to see just how complicated automated theorem provers can be. Without a proof checker, you'd have to prove correct that theorem prover. This is beyond whaty we can economically do in 2015.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I am surprised that proofs constructed by ATPs can be buggy. (I thought ATP's can be incomplete but not unsound/buggy) I am less informed here. I'll be happy to know if there are any known instances of expensive mistakes in proofs generated by ATPs. $\endgroup$
    – Ram
    Commented Aug 31, 2015 at 19:42
  • 3
    $\begingroup$ @Ram There are thousands of tiny soundness bugs in the history of any serious automatic theorem prover. See e.g. stackoverflow.com/questions/12281085/… or the revision history of any such tool on github. $\endgroup$
    – cody
    Commented Aug 31, 2015 at 21:19
  • $\begingroup$ @Ram In addition to Cody's great advice, I recommend to learn from experience: write a little ATP such as a basic SAT solver. That can be done in a few lines of code. Then try and make it perform well by adding e.g. clause learning, watched literals or interesting variable selection heuristics. Then think about the experience ... $\endgroup$
    – Martin Berger
    Commented Sep 1, 2015 at 13:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.