Curry–Howard 对应——证明即程序
上级：logic
这是整条分支的枢纽：命题即类型，证明即程序，证明的规范化即计算。 逻辑与计算是同一种结构的两次显现。
对应词典
| 逻辑 | 类型论 / 编程 |
|---|---|
命题 A | 类型 A |
A 的证明 | 类型为 A 的程序（项） |
A → B（蕴含） | 函数类型 A → B |
A ∧ B | 积类型 A × B（元组） |
A ∨ B | 和类型 A + B（带标签的联合体） |
⊤ / ⊥ | 单位类型 / 空类型 |
∀x.P(x) | 依赖函数 Π(x:A). P x |
∃x.P(x) | 依赖对 Σ(x:A). P x |
| cut / 迂回消除 | β-归约（求值） |
一个假设 A 并推出 B 的证明，实质上就是一个把"A 的证据"转化为"B 的证据"的函数。检验一个证明 = 对一个项做类型检查。
为什么深刻，不只是巧合
- 构造性： 要证明
∃x.P(x)，你必须构造出一个见证x，并给出P(x)的证明——也就是说，一个能产出它们的程序。所以直觉主义逻辑 ⟺ 有类型的 λ-演算，二者严格对应（经典逻辑需要控制算子——Griffin，1990，call/cc）。 - 规范化即运行： cut 消除（简化一个证明）就是 β-归约（运行一个程序）。一个已规范化的证明就是一个值。
- 历史：Curry（组合子逻辑，1930 年代—58 年）、Howard（1969）"公式即类型"、de Bruijn（Automath）。这正是机器验证证明之所以可能的原因。
推论
你可以用证明来计算，也可以把程序当证明来验证。这正是证明助手的根基：依赖类型论提供了足够丰富的类型，使类型可以是任意命题；Lean 4 通过类型检查来检验证明。计算与证明，本是同一个对象。