形式化验证
我关心形式化验证，不只是因为证明本身。
从 Scala、Haskell 的类型系统，到在 CIDER 中使用 property-based testing，我一直在关注同一个问题：我们能否让机器承担更多判断程序是否正确的工作？当 AI 可以极快地产生代码，如何建立与这种速度匹配的验证能力，可能会成为软件工程接下来最重要的问题之一。
AI 与 specification
长任务的瓶颈正在移向 specification
Agent 已经很擅长沿着明确的 spec 实现并持续数小时保持方向。它经常出错的地方，往往正是 spec 留白之处；而如何写出足够好的 spec，仍未被很好解决。
自然语言还不是可以盲信的 spec
把 AI 比作编译器、把生成代码当作机器码，忽略了输入端的差别：自然语言想法仍然含糊。我想学习如何把它推进到够用的 semi-formal specification，而不是追求处处完全形式化。
从测试到证明
这些方法并非互相替代，而是在不同边界上提供机器可以检查的反馈。
- 1
示例测试
检查预先想到的输入与执行路径。
Unit · Integration · E2E
- 2
性质与反例
把预期写成性质，让测试主动寻找反例。
Property testing · Fuzzing
- 3
类型约束
让一部分非法状态在编译前就无法表示。
ADT · Refinement · Dependent type
- 4
状态空间
搜索协议、并发与故障组合中的系统状态。
DST · TLA+ · Model checking
- 5
机器证明
构造证明项，由可信 kernel 逐步检查。
Rocq/Coq · Lean 4
为什么它重要
不是为了证明一切，而是知道每一种保证从哪里来。
把需求变成可以争论的命题
“系统应该可靠”无法验证；明确状态、不变量和前置条件以后，团队才知道自己究竟在保证什么。
发现测试很难碰到的错误
并发交错、协议状态和边界条件往往藏在巨大状态空间里。形式模型可以系统地搜索，而不是等待线上事故替我们采样。
缩小必须依赖信任的部分
Proof assistant 不会消除所有假设，但能把长论证压缩到一个小 kernel 和明确公理上，让“为什么相信它”可以被追踪。
书与入口
三种尺度：程序证明、证明语言与系统规约。
已读
Functional Programming in Lean
David Thrane Christiansen
把 Lean 4 当作函数式编程语言，学习 type class、monad、dependent type，以及程序与证明的结合。
未读
Theorem Proving in Lean 4
Jeremy Avigad、Leonardo de Moura 等
从 dependent type theory、propositions and proofs 进入 Lean 的证明语言与 tactic。
关联笔记
保留原始笔记形态，在独立页面阅读。
Roadmap
Software Foundations
归纳数据类型、递归函数，以及最初的证明 tactic。
用归纳法证明自然数和递归函数的性质。
列表、pair、option 与结构化数据上的递归证明。
多态数据结构、高阶函数与匿名函数。
把常用证明步骤组织为可重复使用的 tactic。
合取、析取、否定、存在量词与命题逻辑。
用归纳定义表达关系、证据和推导规则。
为后续语言语义准备 total map 与 partial map。
把命题看作类型、证明看作程序和 proof object。
理解归纳类型自动生成的 induction principle。
在 Coq 中形式化一套小型命题逻辑及其证明系统。
研究关系的自反、传递、对称等性质。
定义 Imp 语言、状态和操作语义。
在 Coq 中实现 Imp 的 lexer 与 parser。
把关系式语义与可执行 evaluation function 联系起来。
从经过证明的 Coq 定义中提取可执行 OCaml。
用自动化减少重复的证明步骤。
Functional Programming in Lean
FP Lean 01 · Getting to Know Lean
已完成从表达式、定义、类型与函数开始认识 Lean。
FP Lean 02 · Hello, World!
已完成构建第一个可执行程序并处理基础 IO。
FP Lean · Propositions, Proofs, and Indexing
已完成连接命题、证明与 indexed family。
FP Lean 03 · Overloading and Type Classes
已完成用 type class 表达重载操作和可复用接口。
FP Lean 04 · Monads
已完成理解 do notation、状态、异常与 monad。
FP Lean 05 · Functors, Applicative Functors, and Monads
已完成比较 Functor、Applicative 与 Monad 的抽象能力。
FP Lean 06 · Monad Transformers
已完成组合多种 effect，并理解 transformer stack。
FP Lean 07 · Programming with Dependent Types
已完成让类型携带更多程序不变量。
FP Lean · Tactics, Induction, and Proofs
已完成用 tactic 和 induction 完成程序相关证明。
FP Lean 08 · Programming, Proving, and Performance
已完成在可证明性、可执行性和性能之间建立联系。
FP Lean 09 · Next Steps
已完成完成全书并了解后续可探索的 Lean 资源。
Theorem Proving in Lean 4
TP Lean 01 · Introduction
未读Lean 4、证明环境与本书的基本使用方式。
TP Lean 02 · Dependent Type Theory
未读type、term、universe、function 与 dependent type。
TP Lean 03 · Propositions and Proofs
未读命题即类型，以及 proof term 的基本构造。
TP Lean 04 · Quantifiers and Equality
未读全称量词、存在量词与等式推理。
TP Lean 05 · Tactics
未读用 tactic mode 交互式地构造证明。
TP Lean 06 · Interacting with Lean
未读命令、信息输出、namespace 与环境交互。
TP Lean 07 · Inductive Types
未读定义 inductive type，并使用 constructor 与 recursor。
TP Lean 08 · Induction and Recursion
未读归纳证明、递归定义与 termination。
TP Lean 09 · Structures and Records
未读用 structure 组织数据、字段和继承关系。
TP Lean 10 · Type Classes
未读理解 type class、instance 与自动合成。
TP Lean 11 · The Conversion Tactic Mode
未读在 conversion tactic mode 中处理表达式转换。
TP Lean 12 · Axioms and Computation
未读理解公理、经典逻辑和计算行为之间的边界。
后续
后续方向尚未想清楚
尚未想清楚目前确认 Software Foundations 读到第 3 章、Functional Programming in Lean 已读完；下一步等问题自然浮现后再补。