Constructive Mathematics and MLTT

'A program is a proof'-not a metaphor, but a literal fact. seL4, a formally verified OS kernel in Coq, runs on satellites and medical devices: if it compiles, it is correct.

• **seL4:** Microkernel OS formally verified in Isabelle/HOL - deployed in avionics and IoT devices
• **CompCert:** A C compiler with zero optimizer bugs found, proven correct in Coq
• **Fiat Cryptography:** Cryptographic code (OpenSSL curves) generated from Coq proofs - used in Chrome

Предварительные знания

• Type Theory
• Intuitionistic logic

Constructive Mathematics

Lean 4, used by mathematicians at MIT and Cambridge, is built on constructive type theory. In 2023, Lean formally verified Peter Scholze's condensed mathematics proofs - 200+ pages of math checked in hours. Every proof is a program; existence proofs must exhibit a concrete construction, not just rule out non-existence.

Classically: '√2 is irrational-proved by contradiction, and we know it for certain.' Constructively: '√2 is irrational-here is an algorithm that, given any fraction p/q, shows that |√2 - p/q| > 0.' Every proof is a program.

Martin-Löf Type Theory (MLTT)

Per Martin-Löf (1984) developed a type theory in which **types are first-class mathematical objects**, and proofs and programs are indistinguishable. MLTT is the foundation of Agda, Coq (CIC), Lean, and HoTT.

1) Types (propositions/sets), 2) Terms/elements (proofs/programs), 3) Equality of types (propositional equality). Key idea: 'a : A' reads both as 'a is an element of set A' and as 'a is a proof of proposition A'.

Π-types and Σ-types

The Π-type (dependent product) and Σ-type (dependent sum) are the two main building blocks of MLTT. They generalize →, × and ∀, ∃ simultaneously, uniting logic and type theory.

Πx:A. B(x) is the type of functions whose return type depends on the value of the argument. When B does not depend on x, this is the ordinary function type A→B. Σx:A. B(x) is the type of pairs where the type of the second component depends on the first.

Agda and Coq in Practice

Agda and Coq (Rocq) are programming languages where types are theorems. Programming in them is indistinguishable from proving mathematics. They are used to verify cryptography, compilers, and operating systems.

Agda: pure MLTT, pattern matching, no tactics. Coq: CIC (Calculus of Inductive Constructions), tactic language Ltac, extraction to OCaml/Haskell. Lean 4: modern alternative focused on performance and automation.

Key Ideas

• **Constructivism**: every existence proof must exhibit the object explicitly; LEM is not available
• **MLTT**: types = propositions = sets; Universe₀:Universe₁:… hierarchy avoids Girard's paradox
• **Π-type**: dependent function = ∀; Σ-type = dependent pair = ∃; together they cover all of predicate logic
• **Agda/Coq**: writing a program = proving a theorem; extraction yields a verified executable program

Related Topics

MLTT unites constructivism, type theory, and formal verification:

• Type Theory (System F, CHI) — MLTT extends System F with dependent types; CHI generalizes to full predicate logic
• Intuitionistic Logic — MLTT is the computational interpretation of intuitionistic predicate logic
• Category Theory and Logic — Locally cartesian closed categories = MLTT; HoTT connects MLTT with geometry

Вопросы для размышления

• If all theorems in MLTT are 'constructive', is MLTT weaker than classical mathematics - or just a different mathematics?
• Why is formally verified code in Coq more reliable than code with 100% test coverage?
• Practically: when should one use dependent types (Agda/Coq), and when is Haskell/Rust sufficient?

Связанные уроки

• plt-09-dependent-types