Types as propositions

Everything on the preceding pages is an ordinary functional language. This is the part that is not.

The correspondence

Albite is built on the Curry-Howard correspondence: types are propositions, and programs are proofs. A function’s type states a claim; its body is the argument for that claim. Producing a value of a type is proving the corresponding proposition.

Read the usual type constructors as logic and the mapping is exact:

A function f: A -> B is a procedure turning evidence for A into evidence for B — which is what implication means. Writing one proves the implication.

Why this is more than a pun

Because it means proof checking and type checking are the same operation. There is no separate proof language, no verification pass after the fact. When albite check accepts your file, it has verified the logical content of every signature in it.

That in turn is why the trusted core matters so much. The kernel that checks core terms is about 1,500 lines of Rust. If it is correct, every proof Albite accepts is sound — and the elaborator, parser and code generator, however large they grow, cannot undermine that. They can only fail to compile a program that should have compiled. Soundness has one place to be wrong, and it is small enough to read.

Equality

The proposition that two things are equal is written Eq<T, a, b> — “a equals b at type T”. Its proof is refl, reflexivity, which proves x = x:

theorem zero_eq_zero() -> Eq<Nat, 0, 0> {
    refl
}

Note the spelling: refl is lower-case.

refl proves more than syntactic identity — arithmetic on both sides is evaluated first, so this holds:

theorem two_plus_two_is_four() -> Eq<Nat, 2 + 2, 4> {
    refl
}

How far reduction goes

This is worth being precise about, because it bounds what you can prove with refl alone. Built-in arithmetic reduces, and since 2.0-beta so does a call to a function the compiler has proven terminates, within a work limit:

fn double(n: Nat) -> Nat { n * 2 }

theorem double_two() -> Eq<Nat, double(2), 4> {
    refl
}

A function the compiler cannot see stop is never unfolded. Mark double #[partial] and the same theorem is refused — a proof may not depend on a partial definition at all (see Partial definitions in proofs).

Unfolding settles most facts about concrete arguments. A fact about every natural generally needs induction, by hand or with the induction tactic.

Three combinators build bigger proofs from smaller ones:

let flipped: Eq<Nat, 0, 0> = sym((refl : Eq<Nat, 0, 0>));
let chained: Eq<Nat, 0, 0> = trans((refl : Eq<Nat, 0, 0>), (refl : Eq<Nat, 0, 0>));

sym flips an equality, trans chains two, and cong lifts one through a function. subst rewrites: given a = b and a proposition about a, it gives you the proposition about b.

The (expr : Type) form above is an inline type annotation, which these combinators often need — a bare refl does not say which equality it is proving.

Where this goes

refl proves things that hold by computation. That covers a surprising amount for concrete values, but not a statement about all naturals — for that you need induction, which is the next page.

Be clear about the current stage: this is a real proof system with a small trusted kernel, and it is young. Since 2.0-beta a theorem can also be proved with tactics — theorem … by { … }, with induction, cases, rewrite, simp, ring and omega — and the kernel re-checks the term they build. This manual shows proof terms; the tactics are listed in the 2.0-beta release notes.