我与Leslie Lamport合写那篇论文的经历

# 我是如何与Leslie Lamport合著那篇论文的 来源：https://lawrencecpaulson.github.io/2026/08/21/Lamport.html 2026年8月21日 \[`综合` (https://lawrencecpaulson.github.io/tag/general) `类型论` (https://lawrencecpaulson.github.io/tag/type_theory) `集合论` (https://lawrencecpaulson.github.io/tag/set_theory) `回忆录` (https://lawrencecpaulson.github.io/tag/memories)\] 随着年龄增长，人们会变得更智慧，或者至少他们自认为如此。于是他们便有责任将积累的智慧传授给年轻一代。 Leslie Lamport（https://lamport.org/）因在分布式系统与容错领域的成就而成名。对许多人而言，他更著名的身份是LaTeX（https://www.latex-project.org/）的作者——这个著名的宏包让Donald Knuth（https://cs.stanford.edu/~knuth/）传奇的TeX排版系统（https://tug.org/whatis.html）得以被我们普通人所用。随着年岁渐长，Leslie感到必须撰写一系列颇为离奇的论文，标题诸如《如何编写长公式》（https://doi.org/10.1007/BF01211870）。另一篇名为《类型被认为有害》（https://lamport.azurewebsites.net/tla/notes/types.tex.Z），这是对规范语言中类型概念的抨击。其标题呼应了Edsger Dijkstra著名的信件《goto语句被认为有害》（https://doi.org/10.1145/362929.362947）。那封信的标题（由期刊编辑选择）后来被许多反对某些事物的作者借用。Leslie反对类型。但我又是如何卷入其中的呢？ ### 类型被认为有害 Leslie的核心论点是：规范语言应基于无类型形式主义（一种集合论），而非有类型形式主义。他提出了几项支持理由：无类型形式主义更灵活；有类型形式主义引发诸多异常问题；规范中的类型错误在验证阶段终将被发现。 这一论点在某种程度上有其道理。1992年该笔记撰写时，类型系统正处于剧变期。Coq（现称Rocq）刚刚出现，Martin-Löf类型理论正经历重大变革。而简单类型理论方面，HOL的早期实现问世仅数年。当时尚不清楚任何类型化演算能实现什么功能。证明助手尚未支持类型类（type classes）。John Harrison距离引入其低成本依赖类型技巧（https://www.cl.cam.ac.uk/~jrh13/papers/hol05.html）还有数年时间——该技巧已足够表达$T^n$形式的类型。 另一方面，Lamport的笔记相当混乱。他似乎对实际的有类型形式主义缺乏了解，将大部分篇幅用于驳斥一些虚构的靶子。因此当该笔记提交至TOPLAS（https://dl.acm.org/journal/toplas）期刊并转交我审稿时，我的裁决是拒绝。另一位审稿人David McAllester也得出了相同结论。这本应就此终结，但编辑Andrew Appel却另有打算。 ### "稍微修饰一下" 他说，辩论是有益的。这些观点值得探讨，大意如此。但TOPLAS不能容许技术错误。不如你与Lamport合作成为共同作者，将论文改写为技术准确且保持原意的版本？我表示同意：我对类型系统颇有研究，同时也有自己的无类型集合理论形式主义（Isabelle/ZF，https://rdcu.be/bRiRA）——我正乐于推广它。David最初参与了一段时间，但很快退出了。他很明智。¹ Leslie和我合作了相当长一段时间。这是一种奇特的被动合著关系，但我们设法完成了。新论文既保留了Leslie论点的核心，又对类型运作机制给出了更合理的描述。在此过程中，我见证了Leslie无与伦比的TeX技巧：一些底层操作手法是我此后再未见过的。 ### 第二轮审稿，天哪 与此同时，Andrew Appel已卸任TOPLAS编辑。新编辑Carl Gunter并未被告知这篇论文的特殊背景。因此当稿件送达时，他将其送交新的审稿人。这不在原计划内。而新审稿人同样决定拒绝论文。其中一份审稿意见逻辑混乱——显然作者是在情绪极度激动时写成的。于是我联系Carl表示：等等，我的拒稿意见变得一文不值，而这位的意见反而生效了？何况，他简直疯了。最终论文得以发表，附带一段说明文字，表达了期望引发热烈讨论等意愿。我不确定讨论是否真的发生了。 ### 回顾 如今我们可以探讨Leslie的论点在27年后站得住脚的程度。公平地说，情况并不乐观。类型系统已显著发展，在众多规范与验证任务中证明了其价值——部分项目已达到工业规模： - CompCert（https://compcert.org/）经过验证的C编译器 - seL4（https://sel4.systems/）："全球最高可信度与最快速度兼得的操作系统内核" - 亚马逊的Nitro隔离引擎（https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/） 与此同时，困扰集合理论形式主义的问题却进展甚微。没有类型，就无法实现符号重载——这在原理上很简单（只需使用不同符号即可），但在实践中却至关重要。更糟的是，能书写任何内容的自由本质上是为错误敞开大门。验证是发现此类错误极其昂贵的方式，而未被发现的错误可能让你的证明一文不值。据我所知，即使是Lamport自己的规范语言TLA+，最终实现时（https://github.com/tlaplus/tlaplus）也加入了一些类型限制。 因此，实际上你的规范语言很可能应该是有类型的。但寻找改进集合理论表示法的方式依然值得探索。 --- ¹ 原文注释标记保留。