Let’s play Agda: running abstract mathematical proofs as programs

The purpose of this website is to help you learn Agda, the functional proof language. It was created for a 2025 course at the University of Padova.

Start here: Agda as a programming language

👋 Padova students: Transcripts and links accompanying our sessions

In a nutshell: Agda is a programming language…

🧊 purely functional, free of mutable state
🐑 similar to Haskell in syntax and vibe
🧱 statically typed, so that many errors are caught at compile-time
🌳 familiar types like integers, lists, …
🧭 type inference, so that we can focus on those types which matter

For instance, an implementation of insertion sort might look like this:

sort : List ℕ → List ℕ
sort []       = []
sort (x ∷ xs) = insert x (sort xs)

And we can imagine functions with type signatures such as…

fibonacci : ℕ → ℕ                                   -- Fibonacci numbers
pi        : ℝ                                       -- arbitrary-precision constant
size      : {X : Set} → Tree X → ℕ                  -- size of binary tree
replicate : {X : Set} (len : ℕ) → X → Vector len X  -- vector of identical elements

…and simultaneously: a proof language…

🧾 types of witnesses for unifying the activities of proving and programming
✨ context assistance for interactively constructing proofs
🎨 sufficiently expressive for vast parts of mathematics
🤹 hole-driven development

In Agda, we prove a proposition by constructing a program which computes a suitable witness. This approach is the celebrated propositions as types philosophy:

grande-teorema   : 2 + 2 ≡ 4
binomial-theorem : (x : ℕ) (y : ℕ) → (x + y) ² ≡ x ² + 2 · x · y + y ²
sort-correct     : (xs : List ℕ) → IsSorted (sort xs)

For instance, there is a type of witnesses…

that 2 + 2 equals 4 (this type is inhabited);
that 2 + 2 equals 5 (this type is empty);
that there are prime numbers larger than 42 (this type contains infinitely many values, for instance the pair (43 , p), where p is a witness that 43 is a prime larger than 42)
that there are infinitely many prime numbers;
that a given sorting function sort works correctly (this type contains functions which read an arbitrary list xs as input and output a witness that sort xs is ascendingly ordered)
that the continuum hypothesis holds;
and so on.

…helping us with…

✅ verifying correctness of proofs
🧮 implementing algorithms
💭 structuring mathematical thoughts
⚙️ appreciating mathematics from a computational angle
🚀 collaboratively engineering mathematical libraries