Proof and Code Generation in LCF Systems
We next explain how to obtain benefits of proof generation in systems based on theorems as ADT.
To obtain (low-level) proofs: store proofs and ancestores with each formula in the 'theorem' ADT.
To use proofs and avoid overhead of checking on-the-fly:
- first construct a proof (it can be arbitrarily domain-specific, high-level proof)
- then write a checker that traverses the domain-specfic proof, applying proof commands and evaluating proof into a 'theorem' value
Code Generation and Proving Correctness of a Prover
Modern LCF-based provers such as Isabelle contain 'reflection' capabilities as an additional feature.
If we prove, within the system, that certain executable function preserves the truth value of a formula, we can
- generate the code for this function
- use the generated code as a built-in formula transformation
Such approaches were used within Isabelle in recent work on “Linear quantifier elimination”.
More generally, suppose we have two functions
deriveFact : a -> theorem computeFact : a -> formula
Suppose we have a an unsafe function
mkTheorem : formula -> theorem
that just postulates formula as a theorem.
If we prove that, for all a,
mkTheorem (computeFact a) = deriveFact a
then this shows that function deriveFact always produces a valid theorem. Whenever we use expression on LHS, we could hace used expression on RHS. While RHS constructs a theorem, the LHS directly computes it, without invoking primitive rules, so it can be much faster. It is the theorem prover in the usual sense.
- define executable functions (typically as pure, terminating, recursive functions) within HOL prover
- use interactive prove to show that functions satisfy desired properties
- automatically generate code for these functions
- start with code in some programming language
- generate verification conditions in HOL
- use interactive proof to prove these verification conditions
Characteristic of Aprooach 1:
- more flexible: we choose how to organize the proof, need not use particular VCGen strategy
- can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover
- no need to trust verification-condition generator
- limitations in terms of generated code, especially to generate imperative and concurrent code
- need to trust code generator