Leslie Lamport 在 SCaLE 22x 闭幕主题演讲中，先作出一个容易赞同、实践起来却很难的区分：代码是思想的实现，编程还包括找到正确的思想。这场演讲于 2025 年 3 月在一场开源会议上发表，题为“Coding Isn't Programming”（写代码不等于编程）。语法、提高效率的工具和 TLA+ 概览都不在主题范围内；他谈的是在这些手段发挥作用之前应当完成的工作。[1][2][3]

观看这场演讲时，可以把它理解成一套紧凑的设计流程。第一步写明一次计算必须完成什么，不把具体做法悄悄塞进定义。然后把一次执行描述成一串状态，状态之间由允许的步骤相连。状态中只留下会影响后续步骤的信息。最后，找出一句在每个可达状态中始终成立的话——也就是不变量——用它把初始条件连到承诺的结果。

这套流程对开源软件尤其重要，因为维护者经常接手一份代码，而它的预期行为只存在于代码本身。测试展示特定的执行过程，类型约束特定类别的值，代码审查能够发现一行可疑代码，但这些手段都不会自动补上缺失的行为模型。Lamport 的方法让人在设计阶段写出这个模型，此时改正错误的成本仍低。

图像说明：封面采用 Lamport 2006 年在乌迪内出席 IFIP 时拍摄的真实会议照片。照片早于这场主题演讲，却记录了讲述者本人；他在分布式系统和 TLA+ 上数十年的工作，让这堂看似浅近的编程课有了分量。[8]

00:48–07:11 — 把困难部分提到语法之上

Lamport 从并发讲起，因为并发让算法与代码之间的距离再也藏不住。多个进程的步骤能以许多顺序交错执行。一次测试只对其中少数几种顺序取样，时序条件往往还很相近。某个同步缺陷会依赖一种罕见顺序，一直隐藏到部署之后。增加测试可以扩大样本，却无法把抽样变成一条论证，证明所有相关顺序均属安全。[1]

他的办法是把负责协调系统的那一小段行为单独取出，脱离周围的代码细节加以推理。这是抽象在实际工作中的含义：删去与当前问题无关的细节，保留真正影响答案的选择，再把余下的各种情形清楚摆出来，以便检查。

这里需要特别标出，抽象与含混是两回事。写下“正确处理竞态”的文字框，虽然拿走了代码，却没有保留任何行为。有效的抽象会说明哪些量可以改变、哪些量必须固定，以及哪些后续状态得到允许。它可以远小于整个程序，同时对程序中棘手的部分描述得更加精确。

这也解释了 AI 代码生成器为何没有消除设计难题。它可以更快地把提示转成看起来合理的代码；只要提示中的结果含糊、漏掉故障情形，或重试策略前后矛盾，它描述的仍是错误的系统。从提示生成代码的速度越快，预先明确代码究竟应当表达什么就越有价值。

08:34–16:55 — 选择容器之前，先写清结果

主题演讲选了一个刻意保持普通的教学例子：寻找数组中的最大元素。Lamport 先把做什么与怎么做分开。最初的结果描述初看顺理成章，直到输入为空。此时，“最大的元素”没有指向任何值。即使一行代码都还没写，这已经是一个设计缺陷。[1][3]

这一刻比最后写出的循环更值得留意。规约会让随意语言遮住的选择显形，数学形式只是表达手段。空输入应当被拒绝吗？结果是否应当采用可选值？定义域里有没有哨兵值？不同 API 可以作出不同选择。选择一旦写进契约，就不会沦为初始化时偶然产生的行为。

接着，Lamport 又拿掉一个过早作出的决定。数组带有索引和顺序，可这两项都不影响数学上的结果。对这个问题而言，输入可以视为一个容许重复值的多重集。这个更小的视图容纳多种写法，也免去了与元素位置有关的无关义务。以后若稳定顺序变成可观察行为，抽象层就要把它补回来。因此，抽象是在声明哪些信息与问题相关；凡是会影响承诺的事实都须保留，即使处理起来麻烦。

在 OSS API 工作中，这是一道很有用的审查问题：issue 写清了结果，还是只提出了一种做法？“添加缓存”“使用队列”和“并行运行工作进程”都在描述做法。关于目标的表述则应说明可以返回哪些响应、哪些请求可以合并或重新排序，以及崩溃之后什么仍须成立。等这些内容明确下来，维护者便能比较各种方案，也不会把熟悉感误认成正确性。

17:17–26:04 — 把算法写成一组允许的后继状态

演讲中段把循环语句清单换成状态转移视角。设想 B 存放尚待检查的值，X 是目前见过的最佳候选值。每一步从 B 中选一个值，将它移除，并在需要时更新 X。由于选择顺序未被固定，这个抽象算法代表了所有处理次序。一份描述对应着一组执行过程。[1][3]

一次执行由一串状态组成；一个动作把某个状态关联到一个允许的后继状态。这也是 TLA+ 规约采用的基本形态。在常见的 Init/Next 模式中，Init 描述所有允许的起始状态，Next 则由所有允许转移的析取式组成。带撇号的变量表示后继状态中的值。[4] 开源的 TLA+ 工具仓库包含 TLC 模型检查器，可以探索这类规约；仓库里也有解析器和 PlusCal 转译器。[5]

观看时值得留意的是，Lamport 缩减状态时十分果断。循环计数器、临时表达式和中间赋值，只要不会影响后续转移，就从描述中消失。连初始化有时也能折叠进初始状态的选择。这与代码高尔夫（code golf）无关。状态越小，执行过程之间无关紧要的差别越少，核心行为的各种走向便越容易枚举，不变量也越容易看见。

这种简化受一条严格条件约束：状态必须包含决定后续允许哪些行为所需的全部信息。若两种处境拥有相同的抽象状态，合法的下一步却不同，就说明某项相关信息已被擦除。在数学上不限制次数的协议里，重试计数器可以无关紧要；一个尝试三次后便停止重试的服务则离不开它。时钟对安全性可以无关，对租约却举足轻重。合适的状态，就是仍能解释设计承诺保留的每一种行为的最小状态。

原子性也属于模型的一部分。把多条机器指令合并成一个抽象动作，相当于断言：对于正在研究的性质，观察者无法分辨这些指令的内部顺序。有时，锁、事务或单线程事件循环足以支持这项断言；另一些时候，它会遮住竞态。因此，划定动作边界直接关乎设计，影响远超记号本身。

26:12–32:43 — 找出经受每一步仍然成立的那句话

以 A 表示原始输入、B 表示尚未处理的余项、X 表示当前候选值，证明还需要一座连接进展与结果的桥。在演讲给出的表述中，把 X 和 B 中剩余值放在一起，所得最大值始终等于 A 的最大值。处理一个元素会改变这种表示，事实本身保持不变。[1][3]

这项事实就是不变量。使用它时，需要把三项证明义务分开：

1. 证明每个允许的初始状态都满足不变量。
2. 假设一次允许的步骤发生前不变量成立，再证明步骤发生后它仍然成立。
3. 当算法抵达终止条件时，把该条件与不变量结合，推出承诺的结果。

这种论证比不断累积样例更有力量。单元测试可以显示，[3, 1, 7] 的某一种处理顺序返回 7。不变量则解释了为何每一种允许的下一元素选择都能保持答案。它也更利于诊断：只要某次转移没有维持这句话，问题便落在三处之一——转移写错了、状态缺少信息，或提出的不变量没有表达算法成立的真实原因。

这份证明还没有涵盖终止性。一个系统可以一直维持所有安全性不变量，同时永远继续执行步骤。Lamport 把“坏状态能否抵达”与“有用的进展是否终将发生”分开。调度公平性、网络最终送达、超时或有界重试，都可成为服务取得进展的条件。这些属于环境假设与活性义务；即使留在文字背后，它们也依然存在。

33:15–38:58 — 精化让模型与代码仓库相遇

理解抽象算法之后，就要重新考虑具体方案。数学中的极端值，落到具体语言里可以对应最小值、带标签的结果或错误。一个抽象动作可以展开成受互斥锁保护的多条语句。多重集可以变成带索引的数组。这些映射都属于精化决策：只有当代码的可观察行为对应某次允许的抽象执行时，这份代码才符合要求。

模型检查的能力范围也止于此处。TLC 可以探索给定配置下有限模型的可达状态，并为指定性质找出反例。它无法证明生产代码实现了该模型，无法保证模型囊括环境中每一种敌意行为，也无法保证指定性质正是用户真正需要的性质。一次通过的模型检查，只能为特定假设下的规约提供证据，不能充当无关二进制程序的正确性证书。[4][5]

设计的状态空间有时蕴含巨大风险，代码量却看不出这一点；此时，这种方法仍可带来可观收益。一份 AWS 工程报告介绍了团队如何把 TLA+ 规约和模型检查用于棘手的分布式系统设计，尤其是那些故障与并发事件组合极多、常规测试无法覆盖的设计。[6] 后来一篇回顾十年工业界 TLA+ 实践的系统性综述，在记录各项收益的同时也梳理了采用过程中的实际难题，可用来校正把形式化方法当成魔法或仪式的两种看法。[7]

这场主题演讲本身处理的范围有意超出 TLA+。Lamport 说，大多数日常程序用不到 TLA+ 规约。真正可以带走的是在不同层次之间移动的能力：清楚写下行为层面的想法；当顺序有影响时选择状态与步骤；当正确性横跨这些执行序列时使用不变量；当组合数量超过非形式推理能够可靠处理的限度时，再采用形式语言或模型检查器。[1]

40:29–49:52 — 执行一套可重复的设计惯例

演讲的收尾部分回到了写作。精确解释本身就是设计发生的方式之一，不能等同于设计完成后补上的文档。如果维护者解释一个重试循环时只能逐个背诵分支，就需要继续核对抽象是否仍有缺口。如果一个接口只能指着某份代码来描述，调用者便没有独立依据判断意外结果究竟是不是缺陷。[1]

面对一次真实的 OSS 改动，可以把演讲中的方法整理成一套短小的操作次序：

1. 用调用者可见的语言写下结果与失败行为，暂时不提预定的数据结构或控制流。
2. 只列出会影响后续行为的值。逐项审视；删除某项事实会把合法下一步不同的处境合为一体，就把它补回。
3. 描述初始化与允许的转移，其中包括失败、重试、取消和恢复转移。
4. 提出一个把变化中的状态与承诺结果连起来的不变量。分别检查初始化、不变量保持和终止条件蕴含结果这三项。
5. 明确写出进展假设。确定哪些事情最终必须发生，以及它们依赖调度器、时钟、网络或操作人员的哪些行为。
6. 如果交错次序或故障呈组合式增长，就编码一个小型有限模型，让检查器寻找反例。
7. 把每条重要的代码执行路径映射回模型，再保留测试以检查映射关系、具体边缘情形和集成行为。

这套方法没有要求每个拉取请求都写成证明。一行格式化程序或一个直接适配器，有时用代码表达反倒更清楚。当行为依赖历史时，它的投入才显出价值：协调、重试、缓存、事务、迁移、权限、调度器，以及部分失败后的恢复，都属于这一类。在这些领域，代码越多，中心论证往往越难看清。

Lamport 那个看似小得不能再小的最大值例子，留下了一堂长久有效的课。正确程序无法单靠语法出现。它们源于有人先界定结果的含义，选择能够保留相关后续行为的状态，允许正确的转移，并找出任何转移都无法破坏承诺的原因。代码是这套论证运行的地方，设计本身就是这套论证。

来源

1. Southern California Linux Expo，“Coding Isn't Programming — Leslie Lamport”，SCaLE 22x 闭幕主题演讲，YouTube 视频，2025 年 3 月 9 日。
2. Southern California Linux Expo，“Closing Keynote with Leslie Lamport”，活动页面及日程记录，2025 年 3 月 9 日。
3. Leslie Lamport，“Coding Isn't Programming”，SCaLE 22x 官方演示文稿。
4. TLA+ by Example，“Basic Operators”——Init/Next 模式、动作及带撇号的变量。
5. TLA+ Foundation，tlaplus/tlaplus——TLA+ 命令行工具、TLC、PlusCal 转译器和 Toolbox 的源代码仓库及文档。
6. Chris Newcombe 等，“How Amazon Web Services Uses Formal Methods”，Communications of the ACM，2015 年。
7. Roman Bögli 等，“A Systematic Literature Review on a Decade of Industrial TLA+ Practice”，Integrated Formal Methods，2025 年。
8. Wikimedia Commons，“File: Leslie Lamport September 2006.jpg”——Andrej Bauer 摄影，CC BY-SA 2.5 SI。