守株阁

形式化方法导引主线 13 篇结束后，常被问的延伸问题是："Curry-Howard 同构是不是只有’逻辑 ↔ 类型’这两端？"答案是不完全：1980 年前后 Lambek 把这条同构补成了一个三角——加入范畴论作为第三个等价表述。 逻辑、类型论、范畴论说的是同一件事，只是观察镜头不同。这条三角对应被叫 Curry-Howard-Lambek 同构，是任何想往程序语言语义、依值类型基础、同伦类型论方向走的人必须越过的一座山。 本文是系列附录，不属于主线 13 篇，目的是给硕士生指一条范畴论入门的最短路径。不展开范畴论基础，重点把"三角"的形态点清楚。 三角的形态 123456789101112 逻辑 (直觉主义命题逻辑 IPC) /\ / \ / \ / \ / \ / \ / \ / ...

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

第 10 篇展示了 CompCert、seL4、Four Color、Mathlib4、Feit-Thompson 五个把形式化推到极致的项目。它们也共同暴露了一件事：形式化的代价非常高，证明/代码比常在 2-25:1，时间跨度通常以年计，依赖少数 deep expert。 本篇接着这条线，回答"什么时候不该上形式化"。判断的边界与判断的成本本身同等重要：错用形式化的项目要么半途而废，要么变成一份维护负担巨大的"科研作品"。 本篇分四部分：形式化能给的与不能给的、与传统验证手段的关系、典型决策维度、几条可操作的判断准则。 形式化能给的与不能给的 能给的： 对被建模部分的深层正确性保证。证完后该部分的实现错误被排除到内核 + 模型外。 一致的接口：能用同一种语言（Lean / Coq）同时写程序、写规约、写证明、写元理论。 跨变更的稳健性：每次修改 Lean 都重新检查全部依赖；不存在"改完忘补测试导致 regression"这种事。 公开的信任面：通过 #print axioms 与代码评审可精确审计相信了什么。 ...

到第 09 篇为止，本系列把形式化方法的概念骨架、工具操作与可信基底都说清楚了。本篇离开理论，看四个被广泛引用的真实大型形式化项目：CompCert、seL4、Four Color Theorem、Mathlib4。 每个案例按同一个模板梳理： 它证了什么。 代价多大（人月、行数、时间跨度）。 信任面在哪里。 对工程或数学意味着什么。 读完本篇之后，"形式化能在工程里干到多深"这件事不再抽象——四个案例给出了四种不同形态的答案。 CompCert：一个被形式化验证的 C 编译器 证了什么：CompCert 是一个 C 子集（接近 C99，但去掉部分边角语义）的优化编译器，从 C 源代码编译到 PowerPC、ARM、x86、RISC-V 汇编。它在 Coq 里证明了一条语义保持定理： 若源程序 S 没有未定义行为，则编译后的目标程序 T 的所有可观察行为都是 S 的可观察行为的子集。 形式化的"正确"在这里被精确定义成"源语言形式化语义与目标语言形式化语义之间的精化关系"。CompCert 给两端都写了形式化语...

题面 把一个真实落地的项目折叠成一道架构题： 有一个 git 仓库，里面散落着 N 个 SKILL.md 文件（带 YAML frontmatter + 同目录的资源文件）。要做一个内部「Skill Hub」服务： 浏览、搜索、分类、查看详情 在线预览 markdown 与文件树 一键下载某个 skill 的 zip 包 源仓库 push 时 Hub 要自动跟上 部署形态是单 Node 进程（容器平台只给一个端口） 怎么设计？ 约束是分批给的。每听完一版方案，就追加一个新约束逼着方案迭代。下面 14 层按这个节奏走。每层先写最朴素的版本，再写暴露出来的问题，最后写改进，配最小可读的代码片段。 代码片段、字段名、目录名都是从一个真实落地的项目里抽出来的，业务和组织信息已经全部抹掉。 第 1 层：最朴素的版本 最直接的实现： 12345app.get("/api/skills", async () => { await exec("git clone --depth 1 $REPO /tmp/work"); con...

到第 08 篇为止，"编译通过 = 定理得证"的等式在 Lean 4 里已经成为肌肉记忆。但每个写过证明的读者迟早会问： 我相信 Lean 编译通过等价于定理得证。但这条信任传到底是信什么？ 本篇专门回答这个问题。形式化方法不让人脱离信任，它让人把"信什么"明确化。明确化的边界叫可信计算基底（Trusted Computing Base，TCB）。形式化系统的 TCB 越小越好；任何 sorry、任何坏公理、任何元理论缺口都会让 TCB 撑大。 本篇按"哪些东西必须信、哪些东西不必信、信任面破口长什么样、坏公理怎样让整套系统崩"四段展开。 什么是 TCB TCB 在安全领域指"必须正确才能保证系统安全的最小组件集合"。在形式化系统里它有一个对位的定义： 必须正确才能让"编译通过 = 定理得证"这条等式成立的最小组件集合。 对一个用 Lean 4 写出的证明，TCB 通常包括： Lean 4 的类型检查器内核——按规则机械验证每一段良类型项。 Lean 4 内核所依赖的底...

第 07 篇把 Lean 4 环境装好了。本篇真在 Lean 4 里写一组经典命题的完整证明：合取交换律、析取交换律、等价、自然数加法交换律、列表拼接长度。每条命题给出 term mode 与 tactic mode 两种写法。 读完本篇之后，"在 Lean 4 中写一段非平凡证明"对读者来说不再是抽象。系列的主线问题"为什么编译通过就是定理得证"也由这些可在 InfoView 里看到 No goals 的具体证明落到肌肉记忆。 推荐的最小工程结构 把本篇所有代码放进 FormalIntro/First_Theorems.lean： 123456namespace FormalIntro.First-- 后面的代码都在这里-- ...end FormalIntro.First 每条命题都写两遍：term mode 优先，tactic mode 对照。看到等价的两种形态可以加深"tactic 是构造项的元程序"这条直觉。 命题逻辑 合取交换律 12345678-- term modetheorem and_comm_t ...

到第 06 篇为止，本系列的所有概念都已铺开。从本篇开始换姿势：不再用 Python 模拟，也不再贴 Lean 4 片段当示意，而是让读者在自己机器上跑 Lean 4，写下第一个证明，看着编辑器右栏的 No goals 出现。 本篇是一篇短工具文：装 elan、跑 lake new、配 VS Code、写一段会动的 Lean 代码。系列从下一篇开始所有 Lean 示例都默认在这套环境里跑。 一句话总结要装什么 组件 作用 安装方式 elan Lean 4 版本管理器（类似 Rust 的 rustup） 官方脚本一行 lean Lean 4 编译器与类型检查器 elan 自动拉 lake 项目与依赖管理器（类似 cargo） 随 lean 一起 VS Code + Lean 4 插件 编辑器 + InfoView 应用商店搜 lean4 完全不想装本地环境的读者，可以直接用 Lean 官方 Web 编辑器 https://live.lean-lang.org/。本篇先讲本地路径，最后留 Web 编辑器的最小回退方案。 安装 elan elan 是 ...

第 05 篇把 STLC 升级到带 Π 与 Σ 的依值类型，量词被纳入类型系统。但要在自然数、列表、树这些数据结构上证明命题，还差一件事：归纳法。 直觉上，“自然数加法可交换"这种命题的证明依赖"对所有自然数都成立”，而自然数本身是一个归纳定义的对象。要让证明跟着数据结构走，类型系统需要支持归纳类型：用一组构造子定义一族数据，然后允许"按构造子分情况讨论"——模式匹配——作为消去规则。 本篇说清楚归纳类型怎样定义、模式匹配怎样替代逻辑里的归纳推理、为什么"归纳法"在依值类型系统里就是"良基递归"。 inductive：用构造子定义一族数据 自然数在 Lean 4 里是这样定义的： 123inductive Nat where | zero : Nat | succ : Nat → Nat 这条 inductive 声明在做四件事： 引入一个新类型 Nat。 声明两条构造子：zero 与 succ。 自动生成一组消去规则：可以对 Nat 做模式匹配。 自动生成一条递归子（recursor）Nat...

到第 04 篇为止，STLC 已经把直觉主义命题逻辑全部装进类型系统。但日常数学和工程里大量命题超出命题逻辑范围：“对任意自然数 n，n + 0 = n”、“对任意列表 xs，reverse (reverse xs) = xs”。这些命题都带量词，命题逻辑写不出来。 让类型系统能表达量词的关键扩展叫依值类型（dependent types）：允许类型本身依赖值。一旦允许类型依赖值，∀ x : A, P(x) 就能翻译成"对每个 x : A 都给出 P(x) : Prop 的函数"——这条函数本身有依值的返回类型。 本篇说清楚依值函数 Π、依值积 Σ、Vec n α 这种经典例子，并把它们与一阶逻辑的 ∀、∃ 精确对应起来。 STLC 卡在哪里 STLC 里函数类型形如 τ1 → τ2，τ2 必须是与 τ1 完全无关的、固定的类型。例如可以写： 1length : List Nat → Nat 但写不出： 1replicate : (n : Nat) → Vec n Nat 后者的返回类型 Vec n Nat 依赖输入 n。STLC 的 → 不允许这件事。 类...