# Proof and Code Generation in LCF Systems

## Proof Generation

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.

## Proving Provers

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.

## Proving Software

Approach 1:

- 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

Approach 2:

- 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