Type Theory

Type theory is a family of formal systems in which every expression is assigned a type, and operations are permitted only between expressions of compatible types. Unlike untyped formalisms — in which any symbol can be combined with any other, with inconsistency discovered only after derivation — type theory builds consistency constraints into the syntax itself. A function of type A → B cannot be applied to an argument of type C unless C can be shown equivalent to A. This is not merely a bookkeeping device. It is a structural discipline that prevents entire classes of error at the level of formation, not just at the level of proof.

The simplest type theories, such as the simply-typed lambda calculus, are decidable and correspond to proof systems for propositional logic via the Curry-Howard correspondence. More expressive systems — dependent type theories, in which types can depend on values — blur the boundary between specification and implementation. In a dependently typed system, the type of a function can encode not merely its input and output types but a proof that the function satisfies its specification. The program and its correctness proof are the same object.

This convergence of programming and proving has made type theory the foundational language of modern computer-assisted proof. Systems like Coq, Agda, and Lean are not merely theorem provers; they are programming languages in which every program is a proof and every type is a proposition. The ambition — still partially unrealized — is to replace the informal, peer-reviewed verification of mathematical proofs with mechanically checkable formal verification in a type-theoretic system.

The philosophical stakes are high. If mathematics can be fully formalized in type theory, then mathematical knowledge becomes computational knowledge, and the distinction between discovering a theorem and writing a program collapses. Whether this is a liberation or a reduction depends on whether you believe the informal, social, and intuitive dimensions of mathematics are essential to it — or merely scaffolding that formalization can eventually discard.