Agda (programming language)

Agda is a dependently typed functional programming language and interactive proof assistant developed at Chalmers University of Technology. It is not merely a programming language with a powerful type system; it is a system in which programs, specifications, and proofs are the same kind of object. In Agda, the type of a function can encode not just what the function consumes and produces but what it guarantees: that a sorting function returns a permutation of its input, that a network protocol preserves message ordering, that a cryptographic primitive satisfies its security specification. The type system is not a check; it is a contract that the compiler enforces.

Agda is the intellectual descendant of the Automath project of N.G. de Bruijn, the first attempt to encode all of mathematics in a formal language, and of the Martin-Löf type theory that grounded constructive mathematics in a computational semantics. It sits in the same lineage as Coq and Lean but distinguishes itself by its focus on programming: Agda is designed to be a language in which one writes executable code first and proves properties about it second, rather than a proof assistant in which one writes theorems first and extracts programs from them second. The distinction is subtle but consequential: Agda's programming model is not an afterthought but the organizing principle.

Dependent Types

The defining feature of Agda is dependent types: types that depend on values. In a conventional type system, a type like `List Int` is a type constructor applied to a type argument. In a dependent type system, a type like `Vec Int n` is a type constructor applied to a type argument `Int` and a value argument `n` — the length of the vector. The type `Vec Int 3` is inhabited only by vectors of length 3. The type system knows the length at compile time, and operations that require matching lengths — like concatenation or zip — are type-safe by construction.

This is not merely a convenience. It is a shift in the locus of correctness. In a conventional language, the property "this list has length 3" is a runtime invariant that must be checked with assertions or tests. In Agda, it is a compile-time property that is enforced by the type checker. The program cannot represent a vector of the wrong length; the type system makes it unrepresentable. The space of well-typed programs is the space of correct programs, and the compiler's job is to ensure that no program outside this space can be executed.

The cost of this power is that the programmer must write more type information. Agda is not a language for rapid prototyping; it is a language for building systems where the cost of a bug exceeds the cost of proving correctness. The CompCert verified C compiler, the seL4 microkernel, and the proof of the Four-Color Theorem in Coq all demonstrate that full formal verification is possible. Agda extends this possibility to programs that are not just correct but correct by their very structure.

The Curry-Howard Correspondence in Agda

Agda's type system is a direct implementation of the Curry-Howard correspondence: propositions are types, proofs are programs, and proof checking is type checking. A proof of the proposition "for all natural numbers n, n + 0 = n" is a function that takes a natural number n and returns a proof that n + 0 = n. The proof is not a separate document; it is the program itself. The compiler checks the proof by type-checking the program.

This integration of programming and proving is what makes Agda a tool for correct-by-construction software engineering. The specification is not a comment or a test case; it is the type of the function. The implementation is not a separate artifact; it is the proof that the specification is satisfiable. The two are inseparable, and the compiler ensures that they are consistent. This is the formal realization of Dijkstra's dictum that program testing can show the presence of bugs but never their absence: in Agda, the absence of bugs is a theorem, and the compiler is the proof checker.

Agda in Practice

Agda is used in research and in critical system development where correctness is paramount. It has been used to formalize category theory, homotopy type theory, and constructive mathematics. It has been used to verify compiler correctness, protocol security, and type system soundness. Its community is smaller than Coq's or Lean's, but its design philosophy — programming as proving — has influenced the broader ecosystem of formally verified software.

The practical challenge of Agda is not the language itself but the expertise required to use it. Dependent types are conceptually demanding, and the error messages of a type checker that is also a proof checker are not always intuitive. A type error in Agda is not "you passed a string where an int was expected"; it is "your proof does not establish the proposition you claimed." The learning curve is steep, but the payoff is software that is correct by construction — not tested, not reviewed, but proved.

The systems-theoretic significance of Agda is that it treats correctness as a structural property rather than a behavioral one. A correct system is not one that happens to produce the right outputs on the tests we ran; it is one that cannot produce the wrong outputs because the space of possible outputs has been constrained by the type system. This is a radical reconceptualization of software engineering: from empirical validation to mathematical proof, from testing to theorem proving, from hope to demonstration.