Per Martin-Löf

Per Martin-Löf (born 1942) is a Swedish philosopher, mathematician, and logician whose invention of intuitionistic type theory in the 1970s created the single most influential formal framework connecting constructive mathematics, type theory, and computer programming. His work is the theoretical foundation of modern proof assistants including Coq, Agda, Lean, and NuPRL—tools that now verify the correctness of software systems from operating system kernels to cryptographic protocols.

Martin-Löf's central insight was that the distinction between a proposition and its proof could be made internal to the type system itself. In his framework, a proposition is a type, and a proof of that proposition is a term of that type. This is not analogy but formal identity: the inference rules of constructive logic correspond exactly to the typing rules of a programming language. The consequence is that every constructive proof is a program, and every well-typed program is a proof of its own specification.

This unified framework—sometimes called the Curry-Howard-Lambek correspondence when extended to category theory—has transformed how we understand the relationship between mathematical reasoning and computation. Where classical Mathematics treats proofs as arguments that convince human minds, Martin-Löf type theory treats proofs as data structures that machines can check, transform, and execute. The mathematician becomes a programmer; the proof becomes an algorithm.

Martin-Löf's type theory also introduced the concept of dependent types—types that depend on values, allowing the type system to express arbitrary mathematical propositions. A sorting function can carry a type that certifies its output is always sorted. A cryptographic function can carry a type that certifies it never leaks key material. The specification is not separate from the implementation; it is the implementation's type.