本系列的主线问题是"为什么形式化编译器编译通过就证明命题得证"。从第 00 篇到第 11 篇，答案已经分层给出：

  • 直觉主义逻辑把"证明"重新定义成"构造一个见证物"（第 01 篇）。
  • Curry-Howard 同构把命题、类型、程序、证明检查四件事压成同一个对象（第 02 篇）。
  • STLC 是最小可证明系统，能精确表达直觉主义命题逻辑（第 03 篇）。
  • 类型检查算法是机械、可终止、可被任何语言实现的（第 04 篇）。
  • 依值类型把表达力从命题逻辑扩到一阶逻辑（第 05 篇）。
  • 归纳类型让数据嵌入证明，递归即归纳法（第 06 篇）。
  • Lean 4 把这套机制工程化，环境可在本地或浏览器跑起来（第 07-08 篇）。
  • 可信基底说清了"编译通过"到底信什么（第 09 篇）。
  • 大型案例（CompCert、seL4、Four Color、Mathlib）展示了"能干到多深"（第 10 篇）。
  • 局限与取舍说清了"什么时候不该上"（第 11 篇）。

本篇收束。它要回答两个尾问：

  1. 一个普通工程师在不进研究院、不写编译器的前提下，可以怎样把形式化思维带进日常代码？
  2. 系列结束后，读者下一步该往哪里走？

工具的连续谱

把形式化按"自动化程度"与"表达力"摆在一张连续谱上：

1
2
3
4
5
6
7
8
[低门槛 / 弱保证]                                          [高门槛 / 强保证]

普通类型系统(Java/Python/C)
  → 严格类型系统(Rust/Kotlin/TypeScript)
    → 精化/契约类型(Liquid Haskell/Dafny/Frama-C)
      → 自动定理证明(F\* + Z3)
        → 模型检查(TLA+/Spin)
          → 交互式证明助手(Lean 4/Coq/Agda/Isabelle)

每一档相对前一档加强保证、加大成本。读者今天大概率在最左两档之间。把"形式化"当成日常工具，第一件事不是跳到 Lean，而是认清自己当前在哪一档、下一档迈一步能带来什么。

普通工程师可以从今天开始做什么

不必装 Lean。下面这五件事在任何已经用着的语言里立刻可做，每一件都是把形式化思维内化的小台阶。

一、把"不变量"写进类型

观察自己的代码里有多少运行时断言、防御性 if、assert、隐式约定。挑一个最常被违反的，问"能不能让它在编译期就不可能违反"。

  • Java/Kotlin 里用 sealed class + when 强制分情况穷尽。
  • TypeScript 里用 discriminated union 取代魔术字符串。
  • Rust 里用 enum、NonZero<T>、Option<T>、Result<T, E>、newtype。
  • Python 里用 Literal、Annotated、NewType，再加 mypy --strict。

这些都是把"运行时检查"提前到"编译期/类型检查期"的轻量形式化。

二、写规约前于实现

把"这段代码必须满足什么"用一段普通注释写下来，再写实现。再小的函数都这样做几次，会发现 30% 的实现选择本来就被规约暗中规定，只是没写出来而已。

进阶版本是契约：requires、ensures、invariant。Java 有 JML，C# 有 Code Contracts，Python 有 icontract。即使工具只在运行时检查，写下契约这件事本身已经把"规约"从隐含变成显式。

三、用 fuzzer 找规约漏洞

写完规约后跑 cargo fuzz、afl、atheris（Python）、jqwik（Java）。fuzz 不证明任何事，但能在十分钟内发现"我以为穷尽了情形但没"。

形式化项目的一条经验是：规约比实现更容易写错。fuzz 是"廉价规约审计器"。

四、设计阶段写 TLA+

任何涉及并发、分布式、状态机的设计，先写一份 TLA+ 规约，跑 TLC 模型检查器看会不会出现违反不变量的执行。

Amazon 的实战经验：写 TLA+ 平均花 1-2 周/feature，每次找到 1-3 个严重设计 bug，回报远大于成本。Learn TLA+ https://learntla.com/ 几个小时入门。

五、读一段 Lean 4 / Coq 别人的证明

不写不要紧，读一段。挑 Mathlib4 里一条你熟悉的定理（Nat.add_comm、List.length_append、zero_lt_one），通读 theorem 的 tactic 脚本。

读 30 段之后，“证明 = 程序"这条直觉会从书上的话变成肌肉记忆。再回头看自己代码里那些"运行时 assert”，会本能地想"如果我能把这条 assert 编进类型"。

系列结束后下一步走哪里

按读者的兴趣方向，下面五条路径每一条都有清晰可走的下一步资源。

路径一：深耕 Lean 4

走完这条线，6-12 个月可独立形式化中等规模数学或工程定理。

路径二：转向 Coq

Coq 比 Lean 4 资料更厚，但社区动量在 Lean 一侧。两个工具的概念高度一致，学一个就能切换。

路径三：轻量形式化方向

这条路径不依赖纯函数式背景，工业上回报最快。

路径四：操作系统/编译器/协议方向

  • 读 seL4 主论文 + 后续 ASPLOS / SOSP / OSDI 上的形式化系统文章
  • 读 CompCert / CakeML / Cogent 的论文与源码
  • 读 Verified Cryptography / HACL* / Vale 工程报告
  • 跟踪 OPLSS、POPL、PLDI 这几个会议的形式化议题

这条路径门槛最高，但产出最有"实物感"。

路径五：纯数学方向

  • 跟 Lean 社区的 Liquid Tensor Experiment、PolyMath、Mathlib 重大里程碑
  • 选一本你熟悉的数学教材（线性代数、实分析、抽象代数），尝试形式化其中一章
  • 读 Kevin Buzzard、Patrick Massot、Heather Macbeth 的 Mathlib 贡献

这条路径回报来自数学本身的兴趣。

一些常见疑问

“形式化是不是会被 LLM 替代？”
LLM 已经在帮忙写 tactic，效率提升不小（Lean Copilot、Llemma、ProofNet 这些项目都是这方向）。但形式化的核心价值在 TCB——内核必须独立验证 LLM 给出的证明，不能"信" LLM。LLM 把人从"写 tactic 的体力活"里解放，但不取代"决定 TCB 在哪里"的判断。

“我学了 Lean 能找到工作吗？”
直接以 Lean 为主业的工程岗很少（Amazon Web Services、Microsoft、AWS Crypto Lab、Galois、Trail of Bits 等少数公司）。但形式化思维——把不变量编进类型、写规约、设计契约、用 TLA+——是几乎所有 senior 工程岗的加分项。Rust 社区里有大量"懂一点形式化但写 Rust"的人，比"全职 Coq"的人多两个数量级。

“形式化要先学好数学吗？”
数学功底有助于读 Mathlib，但不是必要条件。CompCert 与 seL4 团队主力是 PL/OS 背景而非数学家。先从工程角度入手，遇到具体需要的数学再补。

“形式化是不是只是学术游戏？”
看第 10 篇与第 11 篇的案例与判断框架。形式化已经是航空电子、汽车、加密、操作系统、智能合约的生产级技术，但它不适合所有项目——把它当工具而不是信仰。

模式提炼

模式 内容
形式化是连续谱 从类型系统到 Lean，每一档都是形式化思维的一部分
思维先于工具 把规约写下来、把不变量编进类型，不必装 Lean 也能动
选场景前于选工具 失效后果、规约稳定、清晰语义决定值不值
TCB 是核心 形式化的可信度永远等于 TCB 的可信度
路径自选 数学、操作系统、轻量工具、Lean 深耕、转 Coq——按兴趣定方向

系列收束的一句话

"为什么形式化编译器编译通过就证明命题得证"这个问题的最终答案：

因为命题就是类型，证明就是程序，类型检查就是证明检查，而类型检查器是一段被精心控制可信基底的机械算法。

这条等式不是修辞，不是免费午餐，不是消除信任。它把信任聚集到一个小内核上，让信任本身变得可被审计、可被审查、可被减小。能够这样做的工程实践，在历史上是少数。

形式化把"我的程序对不对"这个问题，部分地转换成"我对’对’的定义是什么"。这种转换不是终点，而是起点：定义清楚了，剩下的事情交给类型检查器去算。

后续如何深入由读者自己选。本系列到此结束。

系列回顾

序号 文章
00 编译通过为什么就是定理得证：形式化方法系列导引
01 直觉主义逻辑与 BHK 解释：什么算一个证明
02 命题即类型：Curry-Howard 同构
03 简单类型 lambda 演算：最小可证明系统
04 类型检查算法：证明检查算法的机械实现
05 依值类型：从命题逻辑到一阶逻辑
06 归纳类型与递归：把数据嵌入证明
07 准备 Lean 4 实验环境
08 在 Lean 4 中证明经典命题
09 类型检查器的可信基底：编译通过到底信什么
10 大型形式化案例：CompCert、seL4、Four Color 与 Mathlib
11 形式化方法的局限与工程取舍
12 收束：作为日常工具的形式化（本文）

参考资料