Skip to content

Welcome.lagda.md

Latest commit

 

History

History
97 lines (74 loc) · 3.78 KB

Welcome.lagda.md

File metadata and controls

97 lines (74 loc) · 3.78 KB
Raw

Welcome // 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, recordings 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