形式化方法课程开学第一周通常会出现一个让 CS 背景的学生愣住的演示：教师在 Lean 4、Coq 或 Agda 里敲完几行代码，按下保存键，编辑器右侧弹出 No goals 或者编译进程打印 Build completed successfully，然后教师宣布：定理已被证明。

让人愣住的不是命题本身，而是这条等式：编译通过 = 定理得证。命令式语言里编译通过只意味着语法和类型对得上，离"这段程序做的事是对的"还远；可在形式化系统里，编译通过却被当成数学意义上的"得证"。

这条等式要怎样才能成立？需要类型系统强到什么程度？类型检查器到底替人类干了哪些活、又留下哪些活没干？这个系列从这个具体问题展开，写给硕士一年级、刚开形式化方法课、有 CS 背景但还没真正用过证明助手的读者。

一个具体场景

Lean 4 里写一条命题以及它的证明可以是这样：

1
2
3
-- 命题：∧ 满足交换律
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

把这段代码塞给 Lean 4 编译器，没有任何错误信息。从工程视角看，“编译通过"就是这件事的全部；从课程视角看，编译器刚刚验证了"对任意命题 P、Q，从 P ∧ Q 可以推出 Q ∧ P”。

紧挨着写一段处理对偶的函数：

1
2
3
-- 程序：交换二元组的两个分量
def pair_swap {α β : Type} : α × β → β × α :=
  fun p => (p.2, p.1)

抹掉 theorem/def 的区别和类型层（Prop/Type），两段代码的主体几乎一致：都是 fun ... => ⟨..., ...⟩ 这种"拆开 / 反向打包"的小程序。这不是巧合。系列要花很长篇幅说清楚的事情，浓缩成一句就是：

证明就是程序，命题就是类型，证明检查就是类型检查。

这条命题叫 Curry-Howard 同构，是把"编译通过 = 定理得证"撑起来的核心结构。

三种直觉的汇合

读者打开形式化方法课程时，至少带着三种已有直觉。这三种直觉在课程开始前往往是分开的，课程的工作之一就是让它们合流。

来源 已有直觉 在系列里要做的事
编程 类型系统能拒绝"明显写错"的程序，但通常和"程序是不是符合需求"无关 升级为：类型系统可以表达"程序符合规约"这件事本身
逻辑 证明是一棵自然演绎树，节点是规则，叶子是公理或假设 升级为：那棵树本身可以重新读成一段良类型的程序
数学 证明是文字+符号写成的论证，需要同行评议 升级为：把同行评议的工作拆出"机械步骤"，交给类型检查器去算

三种直觉合流后，"编译通过 = 定理得证"就不再是修辞，而是字面意义。

把"编译通过即定理得证"拆成三层翻译

要让等式成立，需要三层翻译同时对位：

逻辑端 类型端 程序端 检查端
命题 P 类型 P — —
假设 H : P 变量 H : P 形参 H : P —
P → Q 的证明 函数类型 P → Q 的元素 函数 fun h => ... 子程序的类型
P ∧ Q 的证明 积类型 P × Q 的元素 二元组 ⟨a, b⟩ 各分量的类型
P ∨ Q 的证明 和类型 P ⊕ Q 的元素 Sum.inl a / Sum.inr b 标签 + 子项类型
∀ x : A, P x 的证明 依值函数类型 (x : A) → P x 的元素 依值函数 函数体在每个 x 下的类型
∃ x : A, P x 的证明 依值积类型 (x : A) × P x 的元素 依值二元组 见证 + 性质
证明检查 类型检查 — 编译器内核

最右边一栏是这套等式真正的引擎：编译器内核拿到一段程序，按一组固定的类型规则一步步检查，整段程序通过类型检查 ⟺ 中间那棵语法树是一棵合法的证明树。

后续文章会逐行展开这张表，本文只先点出整体形状。

系列要回答的主线问题

主线问题保持不变：

为什么形式化编译器编译通过，就证明命题得证？

围绕这个主线，系列要分别回答：

  1. 在构造主义视角下，“什么算一个证明"为什么能简化成"构造一个见证物”。
  2. 命题、类型、程序之间的对应到底有多严格，哪些逻辑联结词对应哪些类型构造子。
  3. 简单类型 lambda 演算 (STLC) 这种最小系统已经能表达哪些命题逻辑。
  4. 为什么类型检查算法在足够好的系统里就是证明检查算法，而且是机械、可终止的。
  5. 依值类型、归纳类型怎样把表达力从命题逻辑推到一阶逻辑，再推到日常数学。
  6. 真上手 Lean 4 之后，写定理、跑 tactic、读类型错误的实际体验是什么样的。
  7. 类型检查器的可信基底（TCB）由哪些东西组成；坏公理、sorry、不一致定义会从哪里入侵。
  8. CompCert、seL4、Four Color Theorem、Feit-Thompson 这些大型形式化案例分别证了什么、代价是什么、可信度是什么。
  9. 形式化方法在工程上的局限和取舍，与传统测试、模型检查的关系。

每一个问题对应系列里 1 到 2 篇文章，不会跳着写。

系列地图

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
直觉与逻辑层
  -> 直觉主义逻辑与 BHK 解释
  -> 命题即类型：Curry-Howard

最小可证明系统
  -> STLC 语法与类型规则
  -> 类型检查算法 = 证明检查算法

走向一阶与高阶
  -> 依值类型：Π 与 Σ
  -> 归纳类型与递归

落地证明助手
  -> 准备 Lean 4 环境
  -> 在 Lean 中证明经典命题

可信度与边界
  -> 可信基底：内核、坏公理、一致性
  -> 大型形式化案例
  -> 局限与工程取舍
  -> 收束到日常工具

工具选择

主线工具选 Lean 4，原因有三个：

  1. 文档完善、社区活跃，Mathlib 已经积累了大量样例，从代数到拓扑再到数值分析都有可读的真实证明。
  2. 既能当通用编程语言（产出可执行二进制），也能当证明助手，能自然演示"证明就是程序"的双重身份，这正是系列的主线。
  3. 元编程接近现代编程语言习惯，对 CS 背景读者门槛比 Coq 略低。

不强求读者立刻装本地环境。Lean 官方提供了 Web 编辑器，可以直接在浏览器里跑示例。系列第 07 篇会专门讲本地环境搭建。

辅助工具：

  • 早期讨论 STLC、BHK 解释时用 Python 写一个最小类型检查器，跟读者已有的"自己写解释器"经验衔接。
  • 引用 Coq 与 Agda 的语法做对比，但不要求读者搭这两套环境。

给读者的预期

读者画像：

  • 修过离散数学、一阶逻辑、可计算性，能读 BNF、推导规则、归纳定义。
  • 写过命令式语言（C / Java / Python），对函数式语言有零星接触。
  • 对"编译器"有直觉（gcc / javac / rustc 用过），但没把编译器当过证明检查器。
  • 没系统用过 Coq / Lean / Agda。

预期收获：

  • 看完系列后能说清楚"编译通过 = 定理得证"在什么前提下成立、什么前提下不成立。
  • 能在 Lean 4 里独立写出 20 行以内的证明，能读懂常见 tactic。
  • 能给一段非平凡的工程程序判断"形式化是否值得"，并给出可解释的理由。

不在系列覆盖范围内的话题：

  • 同伦类型论、立方类型论的内部机制（点到为止，留给延伸路线）。
  • 范畴论、Curry-Howard-Lambek 三角的范畴侧（同上）。
  • SAT/SMT 求解器、模型检查、TLA+ 的细节（属于"形式化方法"这把大伞下的另一支，本系列不主动展开）。

写作约束

每篇文章的写作约束抄录自仓库内 writing-plans/形式化方法导引系列写作计划.md（这份计划不进 Hexo 发布流，只服务后续协作）：

  • 一篇只回答一个核心问题。
  • 含代码必须实际运行，文章输出与真实输出一致。
  • 至少一处把概念映射到读者熟悉的工程对象。
  • 落盘前扫常见 AI 味与拟人味表达。

阅读次序与写作次序一致，不必跳读，但允许只读概念骨架（前 6 篇）或只读工程实践（后 6 篇）的人挑各自的子集。

一段提前的告诫

"编译通过 = 定理得证"读起来像免费午餐，工程实践里却不是。系列在收束时会把账算清楚：

  • 编译通过依赖一个最小可信内核（kernel），内核之外的一切都是元数据。
  • 内核之外不假思索引入的 axiom 可能让整套系统变成"任何命题可证"，得证不再有意义。
  • 形式化把"哪部分被信"明确化，但并不让人脱离信任：信变了形状，没有消失。
  • 大型形式化案例（CompCert、seL4、Mathlib）展示的是"在多少代价之下能换到多少可信度"，不是"形式化让 bug 消失"。

后续文章会一项一项把这些代价摊开，让读者在课程结束时既能写证明，也能判断什么时候不该写证明。

下一篇从 BHK 解释入手，讨论"什么算一个证明"在构造主义视角下被怎样重新定义，以及这次重新定义为什么是 Curry-Howard 同构能成立的前提。

参考资料