Agda

Agda is a dependently typed functional programming language and interactive proof assistant developed at Chalmers University of Technology. Named after the Swedish mathematician Agda Wester, the language occupies a distinctive position in the design space of formal verification tools: it is simultaneously a programming language in which one writes executable code and a logic in which one proves theorems about that code. This unity of programming and proving — what the designers call 'programming with dependent types' — makes Agda a tool for writing programs that come with certificates of correctness.

Dependent Types and the Curry-Howard Correspondence

The foundational insight of Agda is the Curry-Howard correspondence, which identifies propositions with types and proofs with programs. In Agda, the type of a function is not merely a specification of its input and output domains; it can be a precise logical claim about what the function computes. A function of type '∀ (n : ℕ) → n + 0 ≡ n' is not merely a function that takes a natural number and returns something — it is a proof that addition by zero is a right identity, encoded as a program that the compiler checks.

Dependent types extend this correspondence by allowing types to depend on values. The type of vectors — lists of fixed length — is 'Vec A n', where 'A' is the element type and 'n' is a natural number that appears in the type itself. The append function for vectors has the type 'Vec A n → Vec A m → Vec A (n + m)', and the type checker verifies that the length of the output is the sum of the lengths of the inputs. This is not a runtime check; it is a compile-time proof that the program cannot produce a vector of the wrong length.

Programming with Proofs

Agda's syntax is a refinement of Haskell's, with similar constructs for pattern matching, higher-order functions, and lazy evaluation. The critical difference is that Agda is total: every function must terminate on all inputs, and every pattern match must be exhaustive. This totality is not a bureaucratic constraint but a logical necessity. If programs are proofs, then non-termination is a proof of falsehood — the proposition '⊥' — from which anything follows. The termination checker ensures that Agda remains a consistent logic.

The language supports interactive proof development through Emacs and VS Code integration. Programmers write 'holes' — marked with '?' — that represent incomplete proofs, and the system reports the type of the hole along with the variables in scope. The user then refines the hole by applying constructors, functions, or lemmas, gradually constructing a complete program. This interaction is not merely debugging; it is a dialogue with the type system in which the type checker acts as a theorem-proving assistant.

Agda's proof tactics are less automated than those of Coq or Isabelle, but the language compensates with greater transparency. Every proof step is explicit, and the term language is the proof language. There is no separate tactic language generating hidden proof terms. The cost is verbosity; the benefit is that the proof is the program, and the program is inspectable.

Connections and Limitations

Agda is part of a broader ecosystem of dependently typed languages that includes Idris, Lean, and Coq. It shares with these languages the ambition of making formal verification accessible to working programmers rather than confining it to specialist theorem provers. The Mathematical Components library, developed in Coq, demonstrates that large-scale mathematics can be machine-checked; Agda extends this vision to programming-in-the-large, where the 'mathematics' is the correctness of software systems.

The practical limitations are significant. Agda's type checking is computationally expensive; the same expressive power that enables precise specifications makes type checking undecidable in general. The language relies on user-supplied annotations and heuristics to keep verification feasible. Compilation to executable code is slower than conventional languages, and the ecosystem of libraries and tools is smaller than those of Coq or Isabelle. Agda is a research language and a teaching language; it has not yet been deployed in the large-scale industrial verification projects that Coq has tackled.

Yet Agda's influence extends beyond its own user base. The ideas of dependent types, interactive proof construction, and programming-with-proofs have shaped the design of modern type systems, including Rust's borrow checker, Haskell's GADTs, and the refinement types of Liquid Haskell. Agda is a laboratory for what programming could become if correctness were not an afterthought but a design principle.

The deeper question that Agda poses is whether the distinction between programming and proving is a historical accident or a fundamental divide. If every program can carry a proof of its correctness, and every proof is a program, then the separation of software development from formal verification is not a technological necessity but a cultural habit. Agda does not settle this question, but it makes the alternative viscerally real.