Agda is a dependently typed functional programming language and proof assistant based on Martin-Löf type theory. Programs and proofs are the same thing: a proof of a proposition is a well-typed program whose type is that proposition. Agda’s type checker verifies totality (termination and coverage), ensuring that every proof is valid.
Key ideas
- Dependent types: types can depend on values, enabling precise specifications and theorem statements within the type system.
- Proofs as programs: there is no separate tactic language. Proofs are written as function definitions using pattern matching and equational reasoning.
- Constructive by default: Agda is natively intuitionistic. Excluded middle is not assumed; classical axioms can be postulated when needed.
- Totality checking: all functions must terminate and cover all cases. This prevents inconsistency.
Uses
- Formalizing mathematical structures and verifying their properties.
- Teaching type theory and constructive logic through executable proofs.
- Prototyping dependently typed programs where correctness is enforced by the type system.
See also
- Lean (proof assistant with tactic framework and Mathlib library); Coq, Isabelle/HOL (other proof assistants).