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

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.

Approach 1:

1. define executable functions (typically as pure, terminating, recursive functions) within HOL prover
2. use interactive prove to show that functions satisfy desired properties
3. automatically generate code for these functions

Approach 2:

1. start with code in some programming language
2. generate verification conditions in HOL
3. use interactive proof to prove these verification conditions

Characteristic of Aprooach 1:

1. more flexible: we choose how to organize the proof, need not use particular VCGen strategy
2. can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover
3. no need to trust verification-condition generator
4. limitations in terms of generated code, especially to generate imperative and concurrent code
5. need to trust code generator