Proof-First Pipeline#

This note compares carrying invariants in a program's type with deriving a program through refinement steps. It is a design comparison, not an empirical claim that one approach always scales better.

1. Curry–Howard and intrinsic verification#

Curry–Howard connects propositions with types and proofs with terms. Intrinsic verification encodes selected properties in the types of program inputs and outputs. An implementation can return data together with evidence that the data meets its specification.

This does not require every proof to be written inline. Helper lemmas, tactics, modules, and separately proved algorithms can contribute to the final term. It also does not prescribe a temporal order: development can start from a specification, an algorithm, or a partial proof.

Specification → type / contract
                    ↓
        implementation + proof obligations
                    ↓
         elaboration and proof construction
                    ↓
         kernel checks the resulting term

In Lean, elaboration and tactics produce terms checked by the kernel. The guarantee is relative to the encoded proposition and assumptions. A successful build containing sorry, extra axioms, or an inadequate specification does not establish the intended end-to-end claim. Runtime compilation and foreign code have their own trust boundary.

2. Length-indexed append#

This self-contained example uses a custom inductive vector, avoiding assumptions about a library's vector representation. It is checked with Lean 4.18.0.

namespace ProofFirst

inductive Vec (α : Type u) : Nat → Type u where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

def append : Vec α n → Vec α m → Vec α (n + m)
  | .nil, ys => by simpa using ys
  | .cons x xs, ys => by
    simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
      using Vec.cons x (append xs ys)

end ProofFirst

The return type rules out a result of the wrong length. The arithmetic proof reconciles index expressions; arbitrary arithmetic identities are not solved by definitional equality alone.

Length is only a partial specification. Duplicating one element while dropping another could preserve length. A full append specification must also relate the contents and order of the result to the inputs.

3. Richer specifications: sorted permutation#

A sorting result bundle can contain:

SortedPermOf(xs) = {
  result : List α,
  sorted : Sorted(result),
  perm   : Permutation(result, xs)
}

This is schematic notation, not executable Lean. A verified mergesort additionally needs a suitable ordering relation, a split preserving elements, decreasing lengths for recursion, and a merge preserving sortedness and permutation.

Several organizations can produce the same checked result type:

• Construct the result and witnesses together.
• Prove properties of a plain sorting function separately, then package them.
• Use intrinsic types for local invariants and separate theorems for global properties.

Rich dependent signatures can increase transport and proof-management costs. This is a tooling and API tradeoff, not an expressivity barrier at mergesort or compiler verification.

4. Dijkstra / refinement calculus#

Refinement replaces specifications with increasingly executable statements while preserving their obligations. For command $S$, precondition $P$, and postcondition $Q$, a typical obligation is

$$P\Rightarrow\operatorname{wp}(S,Q).$$

With total-correctness weakest preconditions, this includes termination. Partial correctness instead says that if the command terminates, its result satisfies $Q$; a loop invariant alone does not prove termination.

Useful local obligations include:

• Assignment: $P\Rightarrow Q[E/x]$ for assignment of $E$ to $x$, with capture-avoiding substitution.
• Sequence: find an intermediate assertion and establish both component contracts.
• Loop: initialize and preserve an invariant, derive the postcondition at exit, and establish a well-founded decrease for total correctness.

Refinement laws, statement semantics, and discharged side conditions must be trusted or checked. A trace of plausible transformations alone is insufficient.

These approaches can be combined. Calling one “intensional” and the other “extensional” would conflate artifact organization with distinct concepts in logic.

5. Extraction and algorithm discovery#

A constructive proof carrying a computational witness can provide an algorithm; extraction may erase proof-only components. The details depend on the system and on where the witness lives. In Lean, an existential proof in Prop is not generally a computational return value in Type; a data-carrying structure or dependent pair is often the appropriate interface. Classical choice can establish existence without an executable algorithm.

Formal systems can automate algorithm construction through proof search and program synthesis in restricted search spaces. The limitation is that arbitrary program correctness has no complete, terminating decision procedure. Practical automation depends on the language, specifications, bounds, and available lemmas.

6. An experiment for verified code generation#

Compare equivalent specifications under different artifact organizations, holding runtime semantics, available automation, and checking budget fixed. Measure verified success, proof/repair cost, runtime behavior, and specification coverage. Kernel acceptance alone should not count as task success when the specification is vacuous or incomplete.

Intrinsic types are useful for local properties such as bounded indices and shape compatibility. Global properties may benefit from separate proofs or a hybrid design. Which interface helps a model is an experimental question. Theorem-proving benchmarks such as miniF2F are not interchangeable with verified program-generation benchmarks.

References#

• Theorem Proving in Lean 4: Propositions and Proofs and Inductive Types.
• Lean reference: Propositions, including proof irrelevance and elimination restrictions.
• Dijkstra, EWD418.
• Related proposal: Dijkstra Method for Verified Code Generation.