跳转到内容
Jason's Study

Isabelle/HOL — 让程序证明像写数学论文一样可读

是什么

Isabelle/HOL 是一个让你用数学方式证明程序正确的工具。这本 2002 年 Nipkow-Paulson-Wenzel 的教科书，把 1990 年代积累的所有”怎么用机器证明”的经验，第一次系统地写给”会编程但不一定会数学”的工程师。

日常类比：菜谱审核员。你写了一份”做蛋糕”的菜谱，Isabelle 不是替你做蛋糕，而是逐字检查”打蛋打到 200 圈”这一步会不会让面糊塌——它把你的菜谱变成数学公式，再机械验证每一步推理对不对。

theorem add_commutes: "(x::nat) + y = y + x"
proof (induct x)
  case 0 show ?case by simp
next
  case (Suc n) thus ?case by simp
qed

上面 6 行：第 1 行是要证的命题（自然数加法可交换），后 5 行是结构化证明（按 x 归纳，分 0 和 Suc n 两种情况，每步用 simp 自动化）。这种”像论文一样读得通”的写法，就是这本书最重要的贡献：Isar 语言。

为什么重要

不理解 Isabelle/HOL，下面这些事说不清：

  • 为什么 seL4 微内核（NICTA 2009）敢说”内核没有 bug”——它的 10k 行 C 代码配了 ~200k 行 Isabelle/HOL 证明，验证从机器码到规范的每一层等价
  • 为什么 CakeML 编译器号称”端到端被证明正确”——整个编译链（parser / type checker / 后端）的正确性定理全在 Isabelle 里跑过
  • 为什么 lean-prover / Coq / Isabelle 三家长期共存——Coq/Lean 走依赖类型偏数学家，Isabelle 走 LCF + 强自动化偏程序员
  • 为什么 Sledgehammer 能把一个看起来需要人手凑半小时的引理 5 秒解决——它把目标翻成 SMT 丢给 z3-2008 等求解器跑

核心要点

Isabelle/HOL 的设计可拆成 4 个层次：

第 1 层：LCF 内核（可信基只有几百行）

LCF approach 是 Robin Milner 1972 的发明：内核里只暴露一个抽象类型 thm，加几条原始推理规则。所有更高级的策略（simp / auto）最终都派生回这几条规则。意思是：整个系统可信不可信，只看那几百行内核——其余几十万行写错也只会导致”证明失败”，不会让假定理被接受。

类比：央行印钞机。机器本身只能按一种方式造钞，所有理财产品的合规性最终都回到那台机器上。

第 2 层：HOL 高阶逻辑（Church 简单类型论）

HOL = Higher-Order Logic。基础就是 Church 1940 的简单类型 λ-演算 + 选择公理 + 无穷公理。“高阶”指：函数本身能当变量传（你可以量词化”所有 P : nat → bool 满足……”）。和 hindley-milner 同源，但 HOL 加了量词和经典逻辑公理。

注意：HOL 不是依赖类型。你不能写 Vec n α（长度进类型）。要表达”长度为 n 的列表”，得用谓词 length xs = n 或者 record——这是 Isabelle 和 lean-prover 体感最大的差异。

第 3 层：Isar 结构化证明语言

这是 Markus Wenzel 1999 PhD 的发明，也是这本书最大的”工程贡献”。1990 年代主流证明器都用 tactic 脚本——一长串 apply (rule foo) apply (auto simp: bar) apply blast，谁都看不出第 7 步在干嘛。Isar 把证明改成”have ... show ... by ...”块结构，每一步显式写出当前状态：

proof -
  have step1: "x > 0" by simp
  have step2: "x + 1 > 1" using step1 by linarith
  show ?thesis using step2 by auto
qed

读起来就像数学论文。维护性高一个数量级。

第 4 层：自动化策略

  • simp：条件重写。把方程当重写规则，朝某个方向化简。对绝大部分代数恒等式够用。
  • auto：simp + 命题逻辑搜索 + 一阶推理混合，“先试它再说”
  • blast：纯一阶推理，速度快但范围窄
  • Sledgehammer（书中提到，2007 年后才成熟）：把当前目标翻成 FOL，并发跑 z3-2008 / CVC4 / E / Vampire 几个外部求解器，找到证明后回译成 metis/smt 调用——这是把 nieuwenhuis-dpll-t-2006 的 DPLL(T) 真正接进交互式证明的关键工具

实践案例

案例 1：用 Hoare 三元组证一段循环代码

hoare-logic 的 {P} S {Q} 三元组在 Isabelle/HOL 里是深度嵌入的：

lemma "VARS x y
  {x = X ∧ y = Y}
  WHILE y ≠ 0 INV {x * y = X * Y - r}
  DO r := r + x; y := y - 1 OD
  {r = X * Y}"
  apply vcg
  apply auto
  done

VARS / INV / WHILE 是 Isabelle 内置的 Hoare 语法。vcg 自动生成验证条件（VC），auto 把剩下的算术义务清掉。整个流程把”写循环不变式 + 推 VC + 证 VC”拆成三个独立活儿。

案例 2：seL4 怎么用 Isabelle 证一个内核

seL4 ~10k 行 C 代码，对应 ~200k 行 Isabelle 证明。证明分三层：

  1. 抽象规范（abstract spec）：内核要做什么，约 2k 行 Isabelle 函数
  2. 可执行规范（executable spec）：和 C 数据结构对齐的精化
  3. C 代码本身：通过 AutoCorres 工具自动翻成 Isabelle 函数

证明这三层两两 refinement（精化），加上抽象层满足”capability 安全模型”。整套花了 NICTA 团队约 25 人年。这是工业证明规模的天花板参考。

案例 3：Sledgehammer 把不会证的引理外包

lemma tricky: "∀x. P x ∧ Q x ⟹ ∃y. P y"
  sledgehammer
  (* 输出：Try this: by metis 或 by (smt z3) *)

你输入 sledgehammer，几秒后系统给出”Try this: by metis”。点进去定理就证完了。背后是 Z3 在跑——SMT 求解器接受 FOL 形式，证完后给一个核心引理列表，Isabelle 用 metis（一阶 resolution）把这个引理列表重新组装成 LCF 内核能信的证明。

踩过的坑

  1. tactic 脚本写久了就成黑盒：apply (auto simp: foo bar baz) 一行，半年后看完全不知道在干啥。Isar 显式写中间 have 才能维护。

  2. Sledgehammer 不可控：一个项目 1000 个证明，每个 by metis 跑 5 秒就是 80 分钟 CI。生产代码要把 sledgehammer 找到的证明替换成更快的 simp/auto。

  3. 公理加错全盘崩塌：HOL 是经典逻辑，加一条矛盾公理（principle of explosion）整个理论可证一切。Isabelle 提供 Nitpick / Quickcheck 跑反例搜索兜底——证明前先 nitpick 看看有没有反例。

  4. 类型类不是 Haskell 类型类：Isabelle 有 axiomatic type classes（Wenzel 1997）但语义和 Haskell 不一样，是逻辑层的”假定 α 满足这些公理”。新人容易混淆。

适用 vs 不适用场景

适用：

  • 大规模程序正确性证明（操作系统 / 编译器 / 安全协议）——seL4 / CakeML / 各种密码协议都选 Isabelle
  • 需要强自动化的工程导向证明——Sledgehammer + simp + auto 比 Coq tactic 上手平缓
  • 嵌入式领域语义（写 Hoare logic / 操作语义 / 类型系统）——HOL 的简单类型够用且工具成熟

不适用：

  • 需要依赖类型 / 同伦类型论 / Univalence——选 Coq / lean-prover / Agda
  • 需要可执行的程序提取（Coq 的 Extraction 更成熟，Isabelle 也有 code generation 但不如 Coq 主流）
  • 想在工业代码里加几个 spec 就跑——Isabelle 重型、入门曲线陡，轻量场景选 Dafny / F*

学到什么

  1. 可信基越小越好：LCF 把内核压到几百行，几十万行外围都可任意写，错了只会”证明失败”。这是计算机科学里”trusted computing base”思想最干净的体现。
  2. 工程证明 ≠ 写论文：Isar 的发明承认”证明也是要被维护的代码”，可读性比简洁性重要。这套思想后来影响了 lean-prover 4 的设计。
  3. 自动化的极限是把目标外包：Sledgehammer 不试图自己更聪明，而是把目标翻成 SMT 丢给 z3-2008 这类专家求解器，再把答案翻译回 LCF 内核能信的形式。这是”专业化外包”在证明领域的胜利。
  4. HOL 用 50 年没过时：Church 1940 的简单类型论 + 选择公理这套基础，从 HOL88（Gordon）到今天的 Isabelle/HOL，证明者发现”够用 + 自动化好做”比”表达力顶满”更划算。

历史小故事（可跳过）

  • 1972：Robin Milner 在 Stanford 写 LCF（Logic for Computable Functions），首次提出”内核 + 派生规则”。
  • 1986：Larry Paulson 在 Cambridge 写出 Isabelle，但当时是 generic logical framework，能宿主多种逻辑（HOL / ZF / FOL）。
  • 1989：Mike Gordon 在 Cambridge 把 HOL88 单独抽出。Isabelle/HOL 最终在 90 年代初汇合。
  • 1999：Markus Wenzel 在 TU München 完成 Isar PhD，把”tactic 黑盒”翻新成”可读的结构化证明”。
  • 2002：Nipkow-Paulson-Wenzel 合写本书，把 Isabelle/HOL 从研究工具推成可教学的工程工具。
  • 2009：seL4 SOSP 论文发布，证明系统第一次进操作系统主流视野。

延伸阅读

关联