【锚点】这一篇只钉一个判断：【「证明」不是一张静态的证书，而是一台会跑的计算。命题=类型，证明=程序，这不是类比，是同构。】

【显式】先摆最小例子。命题「A 蕴含 A」，直觉上证明它是废话：假设 A，则 A。但翻译成类型语言：类型 A → A 的居民是什么？是恒等函数 λx. x。证明「A 蕴含 A」= 写一个「给我一个 A，我还你一个 A」的程序。

【流程节点链路】把对应一路推下去： 起点「A ∧ B 蕴含 A」 → 翻译为类型 (A × B) → A → 居民是「取第一分量」fst → 终点：证明就是投影函数。 再走一条： 起点「A 蕴含 A ∨ B」 → 类型 A → (A + B) → 居民是「左注入」inl → 终点：证明就是打标签。

这不是巧合。联结词与类型构造子一一对应：合取↔积类型，析取↔和类型，蕴含↔函数类型，真↔单位类型，假↔空类型（无居民）。而「证明规范化」（把证明化简到不能化简）恰好对应「程序求值」——一个证明的计算内容，就是它的规范形式。这条对应由 Curry（1934，组合子）与 Howard（1969，自然演绎）独立发现，故称 Curry–Howard。

【隐式】真正让人坐不住的是推论。直觉主义逻辑里排中律 A ∨ ¬A 一般不可证——要对任意 A 给出「A 或 A 的否定」的构造，做不到。但若允许控制算子 call/cc，排中律就变得可证。翻译过来：经典逻辑 = 带控制流的程序。「反证法」不是一条神秘推理规则，它是一个 call/cc——抓下当前续延，跳到别处，再回来。逻辑里的「爆炸」（从假推出一切）和编程里的异常，是同一个东西。

【极难发现】这拆掉一个哲学假设：很多人默认「逻辑在先，计算在后」——先有真理，再谈怎么算。Curry–Howard 说反了：对一个命题的「证明」和对一个类型的「程序」，是同一个对象的两副面孔。你没法先有「A 是真的」再有「怎么构造一个 A」；在这个框架里，「真」就是「有居民」。

【待验证点】边界要说清：Curry–Howard 严格成立于特定形式系统之间（直觉主义自然演绎↔简单类型 λ 演算；线性逻辑↔线性类型；模态逻辑↔模态类型）。它不是「所有逻辑都等于所有计算」，而是「特定证明系统与特定类型系统之间存在可计算的同构」。把这句话说过头，就退化成口号。

结尾留一个值得吵的问题：如果证明就是程序，那「数学是发现还是发明」是不是问错了？也许数学既不是被发现的柏拉图对象，也不是被发明的约定——它是可计算结构的空间；而这个空间本身「存在」意味着什么，恰好又是一个类型论问题：∃(数学) 的居民，长什么样？