Proof assistants: Agda, Idris, Lean

A proof assistant is a programming language whose type-checker is also a proof-checker. Via Curry-Howard, writing a program of type T is constructing a proof of proposition T. These tools take that identity seriously and let you prove your code correct — sometimes about the code, sometimes about mathematics itself.

The big four

All four are dependently typed (types can mention values), and all four can express both functional programs and mathematical proofs in the same language.

What "proof" means

You don't prove a property about the code — the code itself is the proof. The type expresses the proposition. Construct a value of that type and you've proved it.

-- Agda: the proposition "for all naturals n, n + 0 = n"
+-identityʳ : ∀ (n : ℕ) → n + zero ≡ n
+-identityʳ zero     = refl
+-identityʳ (suc n)  = cong suc (+-identityʳ n)

The right-hand side is a value of the type on the left. Type-checks ⇒ proof holds.

The pragmatic spectrum

Idris  ←————————————————————————————————→  Coq
"write programs, occasionally prove"     "write proofs, occasionally extract"

• Idris wants you to ship code. Total functions, runtime efficiency, effect system, foreign function interface. Proofs sneak in where types carry invariants.
• Coq is grown out of constructive logic research. Code extraction (to OCaml, Haskell) exists but the focus is the proof. The Russell-style tactics language (Ltac) is half the experience.
• Agda sits between — closer to a programming language than Coq, but with the dependent-type machinery exposed all the way down. Great for teaching the theory.
• Lean has eclipsed Coq for new math formalization due to its speed, tactic ergonomics, and the enormous Mathlib library. Lean 4 is also a serious programming language.

What gets proved in practice

What it feels like

Imagine GHC's type-checker, but the error messages are the steps still missing in a proof, and you talk to the compiler interactively via tactics:

;; Coq-ish pseudocode
Theorem rev_involutive : forall (xs : list nat), rev (rev xs) = xs.
Proof.
  induction xs as [| h t IH].   ;; case split: nil and cons
  - reflexivity.                ;; nil case is trivial
  - simpl. rewrite rev_app.     ;; unfold and use a lemma
    rewrite IH. reflexivity.    ;; finish using the induction hypothesis
Qed.

Each line peels off a goal. When all goals are closed, Qed. checks the underlying term and you have a certificate.

Connection to mainstream FP

You don't need to use a proof assistant to benefit from their ideas:

• GADTs in Haskell / OCaml borrow inductive type tooling.
• Refinement types (LiquidHaskell, F*) bring lightweight proofs into ordinary FP.
• Type-driven development (the Idris idea — write a type, then let the IDE help you fill the holes) has migrated to Haskell, Rust, even TypeScript.
• Property-based testing (QuickCheck) is "the engineer's version of a proof" — try the property on a thousand random inputs instead of proving it for all.

Clojure has no proof assistant, but clojure.spec and malli move in the property-checking direction (generate inputs, run the program, observe the postcondition).

When to reach for one

The cost: 5–10× the dev time relative to a regular FP language. The payoff: absolute correctness in domains where bugs are catastrophic.

Check yourself

Exercise

Pick a small property you believe about a function you've written (e.g., "reverse is involutive: reverse (reverse xs) = xs"). Sketch the induction you would do to prove it on paper — base case + inductive step. That's the skeleton you'd type into Agda or Coq.