「 Lamport讲座-实录」编码不是编程（Coding isn't Programming）

10 Apr, 2025

Coding isn't Programming

视频链接：Coding isn't Programming - Closing Keynote with Leslie Lamport - SCaLE 22x
官方频道：Southern California Linux Expo

内容介绍

以下为您呈现的是图灵奖得主、分布式计算领域的先驱 Leslie Lamport 在 SCaLE 22x (南加州 Linux 博览会) 上发表的闭幕主题演讲实录。本次演讲的核心观点是“编码不是编程”(Coding isn't Programming)。Lamport 认为，真正的编程远不止于编写代码，其关键在于编码之前进行严谨的、高层次的抽象思考。他从自己研究并发系统的经验出发，提炼出适用于所有程序开发的通用原则。

在演讲中，Lamport 深入探讨了“算法”与“程序”的区别，强调了“抽象”在软件开发中的核心地位。他通过一个简单的“计算最大值”示例，生动地展示了如何通过优化问题的定义（“What”）来简化实现方法（“How”），甚至引入了数学概念（如负无穷）来达成更简洁优雅的设计。进而，他介绍了通过“状态序列”和“不变量”来理解和证明程序正确性的强大方法。

为了证明抽象思维的现实价值，Lamport 引用了亚马逊 AWS 和欧洲航天局 Virtuoso 操作系统等实际案例，说明在高层设计上投入思考能够发现深层缺陷、极大提高代码质量和效率，其回报远超单纯改进编码技巧。他还讨论了即使在需求无法完全精确定义的情况下，抽象思维依然是不可或缺的工具。最后，他分享了关于如何培养抽象思维能力的见解，并补充探讨了为何现代软件（尤其是依赖库的软件）因缺乏精确规范而难以定义“Bug”。

内容纲要

Leslie Lamport's SCaLE 22x Keynote: Coding isn't Programming
├── 引言：编程的核心在于思考
│   ├── 明确讲座主题非分布式/并发，而是通用编程思想
│   └── 核心论点：编程 (Programming) ≠ 编码 (Coding)
├── 算法、抽象与程序
│   ├── 算法 vs 程序：算法更抽象，不应局限于语言
│   ├── 强调思想 > 语言
│   ├── 并发/分布式程序的挑战：执行路径多、调试困难
│   ├── 编写并发程序的正确方法：识别并发部分 -> 找对算法 -> 实现算法
│   └── 引入“抽象视图”/“抽象”概念
├── 如何进行抽象
│   ├── 核心要素：定义程序“做什么”(What) vs “如何做”(How)
│   ├── 语言选择：精确语言 (如 TLA+) vs 非正式语言
│   └── 目标：通过抽象简化问题，优化“What”以简化“How”
├── 抽象实践：计算最大值示例
│   ├── 初始“What”的缺陷：未定义空数组
│   ├── 修正“What”：处理空数组
│   ├── 进一步抽象：
│   │   ├── 推广到任意数字和多重集 (Multiset)
│   │   └── 重新定义“What”：求 ≥ 所有元素的最小值 ($-\infty$ 处理空集)
│   └── 价值：思考“What”可极大简化“How”（编码）
├── 证明正确性：状态、执行与不变量
│   ├── 为何需要证明所有执行路径
│   ├── 引入执行模型：状态序列优于步骤序列
│   ├── 状态定义：包含影响未来的所有信息
│   ├── 简化执行：明确初始/步进/终止，简化状态
│   ├── 不变量 (Invariant)：定义与重要性
│   ├── 最大值示例的不变量：$max(\{x, max(B)\}) = max(A)$
│   ├── 证明不变量：初始为真、步进保持
│   ├── 证明正确性：不变量在终止状态下蕴含目标
│   └── 提及终止性问题 (Termination)
├── 从抽象到实现
│   ├── 实现抽象概念 (如 $-\infty$) 的方法
│   └── 程序“实现”抽象的精确含义 (TLA+ 中有定义)
├── 抽象的现实应用与价值
│   ├── 并发系统案例：AWS 使用 TLA+
│   │   ├── 发现深层设计缺陷
│   │   └── 证明形式化方法的 ROI
│   ├── 非并发系统案例：Virtuoso OS (Rosetta 航天器)
│   │   ├── 使用 TLA+ 进行顶层设计
│   │   └── 结果：架构更清晰，代码量锐减 10 倍
│   ├── 处理不精确需求案例：TLA+ Pretty Printer
│   │   ├── 无法精确定义“最佳”，但仍需抽象
│   │   └── 使用规则作为抽象，便于思考和调试
│   └── 抽象的普遍价值：高层思维、独立于语言、先于编码
├── 如何更好地思考与抽象
│   ├── 强调思考先于编码
│   ├── 写作对澄清思维的作用 (“Writing clarifies thinking”)
│   ├── 抽象能力与数学思维的联系
│   └── 学习途径：数学教育、TLA+ 实践、专门学习抽象思维
├── 总结要点
│   ├── 编程 = 思考 + 编码
│   ├── 思考需写作
│   ├── 抽象思维对非简单程序的益处
│   ├── 状态/不变量模型的重要性
│   └── 勿过度关注语言本身
├── 附录：为什么程序“应该”有 Bug？
│   ├── 现代编程对库的依赖
│   ├── 库普遍缺乏精确规范 (Specification)
│   ├── “Bug”的存在依赖于精确规范
│   ├── 输入/输出规范不足以描述并发交互
│   ├── 需要基于状态序列的抽象描述
│   └── 呼吁为库提供更好的抽象规范
└── 问答环节 (Q&A)
    ├── 问题 1：AI 是否能承担抽象思维？
    ├── 问题 2：如何重建学术界与开源社区的桥梁？
    └── 问题 3：面对业界缺乏严格定义的挫败感？Linux 若严格定义会如何？

Coding isn't Programming - Leslie Lamport 主题演讲

I. 引言：编程的核心在于思考 (Programming is Thinking)

这次演讲的内容恐怕不会是关于分布式计算，当然也不是关于并发，尽管显然你们中有些人期望我谈论这些。因为关于那些话题，我没有什么新东西可讲，我只是厌倦了重复同样的老生常谈。

但我意识到，我从编写并发程序中学到的一些东西，实际上适用于所有的程序。所以我今天要谈的是“编程”（Programming），我认为这是你们都会感兴趣的事情。

II. 算法、抽象与程序 (Algorithms, Abstraction, and Programs)

我之所以在这里，是因为我编写的是并发算法（Algorithms），而不是并发程序（Programs）。算法不是程序，它比程序更高级、更抽象。一个算法可以用多种不同的编程语言来实现。

我们不必，实际上我们也不应该用编程语言来编写算法。因为编程语言很复杂，这是有充分理由的：它们必须能被高效执行，并且必须能处理大型程序。但是算法既不需要被执行，通常也不是很大。

那么我们应该用什么语言呢？不要过分纠结于语言。编程人员、计算机从业者太过于纠结语言了。你应该思考的是思想（Ideas），而不是表达思想的语言。

并发程序是指那些包含多个控制线程的程序，这些线程可以并发执行。而分布式程序是并发程序的一种特殊情况，其线程可以在不同的计算机上执行。所以，分布式只是并发的一个特例。

要写对并发程序非常困难，因为不同线程的动作可以以多种不同的方式交错执行。这意味着可能存在数量巨大的执行路径。面对如此庞大的执行数量，很难考虑到所有可能出错的方式。

调试（Debugging）在这里行不通。你无法确定你已经检查了所有相关的情况，因为情况实在太多了。一个程序可能运行得很好，你可能已经对它进行了彻底的测试，它可能一直运行良好，然后系统中的某个改变，以某种方式改变了线程的相对执行速率，就可能暴露出一个在多年程序执行中从未出现过的 Bug。而且，修复一个 Bug 很有可能引入另一个 Bug。调试是行不通的。

那么如何编写一个并发程序呢？首先，你要弄清楚程序的哪一部分涉及并发。这部分基本上是用于同步线程的，确保它们协同工作，互不干扰等等。这通常只占程序功能的一小部分，但却是非常重要的一部分。

你需要做的是，找到一个能完成这部分功能的正确算法。也许这个算法你可以在教科书里找到，也许它与教科书里的某个算法相似，但你可能需要稍作修改——这种情况相当普遍。也可能它是一个全新的算法。

要得到一个正确的并发算法很难，原因和写对并发程序很难是一样的。但是，算法比程序更简单，所以我们还有一线成功的机会。

一旦你有了一个正确的算法，你就可以去实现（Implement）那个算法了。你可能仍然会有编码错误（Coding errors），但我对编码错误不感兴趣。已经有很多语言和工具被开发出来用于捕捉编码错误，而且程序员们非常擅长编码。但他们在寻找正确算法方面就不那么擅长了。

III. 如何进行抽象 (How to Abstract)

那么，如何找到这些正确的算法呢？需要思考的重要事情是抽象（Abstraction）。记住，算法比程序更抽象。通常，只有当某样东西能在许多应用中都有用时，它才被称为“算法”——否则没人会把它写进算法教科书。

描述程序中并发是如何实现的那个算法，通常只对那个特定的程序有用。所以它通常不被称为算法。相反，我会称其为程序的抽象视图（Abstract View），或者抽象程序（Abstract Program），或者干脆就叫抽象（Abstraction）。

所以，我们如何编写一个并发程序？我们找到程序的抽象视图，它描述了程序如何处理并发。它位于比代码更高的抽象层次。

程序员被教导如何编码，但没有被教导如何抽象。抽象涉及一种新的思维方式：在编码之前思考，在比代码更高的层次上思考。程序员应该为所有程序学习如何做到这一点。

那么，什么是程序呢？我所说的程序，是指任何一段需要你在编码前进行思考的代码。它可能是一个完整的程序，可能是某个类中的一个方法，或者仅仅是程序内部一个复杂的循环。它是任何一段需要你在编码前思考的代码，也是任何一段供那些不想阅读代码的人使用的代码。

如何进行抽象呢？程序是为许多不同目的而编写的，没有一种方法适用于所有程序。但对于大多数程序，你应该写两样东西：

程序做什么（What the program does）。
程序如何做（How the program does it）。

我们应该用什么语言呢？再次强调，不要纠结于语言。如果我们想构建一个工具来检查“如何做”是否蕴含了“做什么”，那么我们需要一种精确的语言。对于确保并发程序做了它应该做的事情来说，精确的语言确实是必要的，因为记住，并发程序真的很难写对。我设计了 TLA+，它是一种用于描述并发算法、并发程序抽象视图的精确语言。但对于大多数程序来说，并不需要它。

IV. 抽象实践：计算最大值示例 (Abstraction Example: Finding the Maximum)

我将给出一个极其简单的例子来说明。编写一个函数，计算一个整数数组 A 中的最大元素。这是一个非常基础的编程测试，过于简单，几乎不需要在编码前进行太多思考。

如果我真的非常较真，我可能会写下：

做什么（What）：返回整数数组 A 中的最大元素。
如何做（How）：依次检查 A[0], A[1] 等，令 x 为找到的最大值，然后返回 x。

这里是用 Rust 编写的代码（顺便说一句，我不懂 Rust，我让一个懂 Rust 的同事写的，他告诉我这是那个“如何做”的 Rust 实现）。

// (示例 Rust 代码，非演讲者直接提供，根据描述推断)
fn find_largest(a: &[i32]) -> Option<i32> {
    if a.is_empty() {
        return None; // 处理空数组
    }
    let mut largest = a[0];
    for &item in a.iter().skip(1) {
        if item > largest {
            largest = item;
        }
    }
    Some(largest)
}

请举手，如果你看到了这个算法中的 Bug？（大约三个人举手）。这不是一个编码 Bug，它是“做什么”（What）中的 Bug。

Bug 在哪里？“What”说的是“返回整数数组 A 中的最大元素”。但是，如果 A 没有任何元素，那么就不存在最大元素。所以这个“What”是不正确的，它无法被实现。

对“What”有一个明显的修复：要么规定 A 不能为空，要么在 A 没有元素时返回某个错误值。然后对“How”进行明显的修复：在 Rust 代码中加入处理空数组的逻辑（如上面红色部分所示）。

但是，我们要运用抽象。让我们看看抽象如何移除编码细节，并帮助我们理解为什么程序做了正确的事情。如果我能简化这样一个极其简单的例子，想象一下当事情变得复杂时，抽象能做什么。当然，我们通常不会在这么小的例子上费心使用抽象，但它能说明抽象是如何工作的。

首先，“返回最大元素”。函数调用和返回是编码细节，不是我们感兴趣的部分。我们感兴趣的是如何找到 A 的最大元素，而不是我们如何返回那个值，或者如何获得 A。

所以我将简化“What”：将 x 设置为数组 A 中的最大元素...等等。为什么只针对整数？让 A 是任意数字数组，我们不必将其特定化为整数，对于任意数字都适用。为什么要用数组？我假设我们只关心元素本身以及找到其中最大的那个，而不是它们的排列方式。所以，与其用数组，不如将其抽象为一个多重集（Multiset）——它是多重集而不是集合（Set），因为它可以包含同一元素的多个副本。

现在，我不喜欢原始“What”中处理空数组的部分，因为它使代码复杂化了，而我希望代码尽可能简单。我们能不能找到一个不同的“What”，它同样好用，但实现起来更简单？

当然，对于这么简单的例子来说，这有点傻，增加的复杂度也就两行代码。但是，当我过去用 C 编程时，我经常会先决定程序应该做什么，然后意识到编码实现会很麻烦。我和其他人一样懒，我会去弄清楚我真正需要程序做什么。结果得到的“What”可能没有包含我想要的所有东西，但包含了所有我需要的东西。这需要时间，我会在思考这个“What”上花相当多的时间，但这在后面编写代码时节省了更多的时间，远超我找到更简单“What”所花费的时间。所以，找到“What”需要额外的工作，额外的思考，但最终能节省大量时间，因为它能在实际例子中产生更简单的东西。

现在，我们想要消除处理空数组的特殊情况。如何做到这一点对大多数程序员来说并不明显。但对我来说很明显，因为我受过数学家的教育。我知道一个空集的最大元素应该等于什么。

方法如下：与其将 x 设置为最大元素，不如将 x 设置为大于或等于 A 中所有元素的最小数字。

如果 A 非空，这两者是等价的。但如果 A 是空的呢？这意味着，如果 A 是空的，我们需要将 x 设置为一个大于或等于 A 中所有元素（也就是空集中的所有元素）的数字。如何为空集做到这一点？

如果我说，我比加州博迪镇（Bodie, California）的所有居民都富有，同时我也比博迪镇的所有居民都贫穷。（听众笑）因为博迪镇根本没人居住。换句话说，博迪镇里没有任何人比我更富有或更贫穷，因为博迪镇里根本没人。这是简单的逻辑，但实际上是数理逻辑。要理性思考，你必须理解简单的逻辑。程序员应该理性思考，所以你们都应该懂简单的逻辑。

因此，如果 A 是空的，我们需要一个大于或等于空集中所有元素的数字。这意味着我们需要一个最小的满足此条件的数字。数学家有时将 $- \infty$ 定义为最小的数字。所以，我们将这个“What”理解为：如果 A 是空的，则 x 被设置为 $- \infty$ 。

现在是“如何做”（How）：让一个新的数组（或多重集）B 等于给定的 A。令 x 等于 $- \infty$ 。当 B 非空时：令 i 是 B 中的任意一个元素。（注意：这是非确定性的，因为根据选择哪个 i，可能有多种执行路径）令 B' 为 B 中移除 i 后的集合。令 B 等于 B'。如果 i 大于 x，则令 x 等于 i。

注意，我使用了编程语言表示法和英语的混合，这通常是我编写非并发程序时使用的方式。我写的大多数程序都是非并发的。

V. 证明正确性：状态、执行与不变量 (Proving Correctness: States, Executions, and Invariants)

但是，我们如何让别人相信这个“如何做”实现了那个“做什么”？我相信大多数程序员只能展示某些执行计算出了正确的 x 值，但不知道如何证明所有可能的执行都产生正确的值——这才是我们想要证明的，以确保这个算法是正确的。因为记住，在我们最初的“What”中，只需要一个特定的 A 值就能暴露 Bug。我们怎么知道不存在某个其他的 A 值会导致这个新算法不工作呢？

要理解如何做到这一点，需要思考执行（Executions）。什么是执行？一个显而易见的答案是：它是一系列步骤，每一步是执行代码的某一部分。

一个通常更好的答案是（我说“通常”是因为没有规则适用于所有程序，但通常来说）：执行是状态（States）的序列。一个步骤（Step）是一对连续的状态。我们稍后会看到为什么这是个更好的答案。这一步描述了部分代码的执行。

为了理解如何用这种方式描述执行，让我们看一个我们简单算法计算 A 最大元素的一个可能执行。假设 A 是包含两个 2 和一个 3 的多重集，可以写成 ${2, 3, 2}$ 。

我们令 B 等于 ${2, 3, 2}$ ，x 等于 $- \infty$ 。一个状态将描述 B 和 x 的值，可能还有其他东西，我们稍后再考虑其他东西。我只展示执行中每个状态下 B 和 x 的值。

它们的初始值是什么？一个显而易见的答案是某个标准初始值，比如叫它 ?。所以我们可以设 B 和 x 都等于 ?。然后我们先执行 let B = A 和 let x = -infinity。一个明显的执行方式是将这个初始化表示为两步：第一步设置 B，第二步设置 x。

但是，为了理解这个抽象程序，我们希望执行尽可能简单。简单、简单、再简单！这意味着让执行包含尽可能少的步骤，只要它仍然是对程序行为足够精确的抽象表示。而这两个初始化步骤本身并没有什么意义。所以，与其将它们视为两个步骤，不如直接让初始状态就拥有 B 和 x 的特定值。为了表明我正在这样做，我将不说 let 语句，而是说这是一个初始（Initially）声明。我们声明这些是 B 和 x 的初始值。这只是伪代码，它可以意味着任何我想要它表达的意思。重要的是我们要理解执行过程，不用担心语法细节，只要我们理解了它的含义就行。

好了，下一个状态是什么？代码本身并不告诉你什么构成一个步骤。是执行对 i 的赋值算一步？还是从 B 中选择元素算一步，然后设置 i 的值算另一步？代码没说。

为了保持抽象的简洁性，我将把评估 while 循环的测试条件以及执行循环体（如果条件为真）合并成一个步骤。如果你仔细想想，这是一个很好的抽象，它足以让我们知道我们是否在做正确的事情，以及我们是如何计算 A 中最大元素的。我不会费心去定义一种让伪代码明确表示这是一步的方式，只要你知道就行。

所以，执行下一步。我们可以让 i 等于 2 或 3。假设这次执行选择让 i 等于 3。那么，执行这一步：B 非空，所以让 i=3。从 B 中移除 3，剩下 ${2, 2}$ 。如果 i > x，则设置 x = i。因为 3 > $- \infty$ ，所以我们设置 x = 3。下一个状态是 B = ${2, 2}$ , x = 3。

接下来的两步都必须选择 2，因为那是 B 中剩下的唯一值。第一步移除一个 2，剩下 B = ${2}$ 。因为 2 不大于 3，x 保持为 3。下一个状态是 B = ${2}$ , x = 3。下一步移除最后一个 2，剩下 B = ${}$ 。同样，2 不大于 3，x 仍为 3。下一个状态是 B = ${}$ , x = 3。

现在，执行下一步，发现 B 是空的。所以它退出循环，不改变 B 或 x。这就是完整的执行过程？

但是最后那个退出循环的步骤没什么意思。所以，我将声明：当 while 循环发现 B 等于空多重集时，执行终止。这就是我对执行的定义。我不知道如何用代码表达这一点，也许可以发明一些方式，但只要你知道这就是它的意思就行。这个执行会在 B 变为空集时立刻停止。这在 TLA+ 中其实很容易表达，但我现在不打算纠结这个。再次强调，不要纠结于语言，理解我们想要的执行集合是什么。

好，什么是状态？为了让“执行”成为思考程序的有用方式，可能的下一个状态必须仅依赖于当前状态，而不能依赖于任何之前的状态。我们可以为描述实际程序的抽象选择这样的状态，因为程序是在计算机上执行的，而计算机下一步做什么仅取决于计算机的当前状态（以及可能的外部输入），而不取决于它过去做了什么。所以我们应该能够编写我们的抽象，使得下一步做什么仅依赖于当前状态。

对于这个例子，状态只需要描述 B 和 x 的值。变量 i 仅用于指示导致当前状态的那一步是如何改变 B 和 x 的，i 在之前状态的值不影响下一个状态是什么。如果我没有去掉最后那个额外的终止步骤，那么状态还需要包含执行是否已经终止的信息。就得在状态中加入额外的东西来说明当 B 为空时，程序（执行）是否已终止。这就是为什么我想要移除那个额外步骤的原因，这样我就不必给状态添加额外的部分了，因为我们希望状态尽可能简单。

现在我们可以回答这个问题了：为什么这个抽象程序是正确的？为什么任何可能的执行都会在终止时得到正确的 x 值？

在执行的任何时刻，未来可能发生什么仅取决于当前状态。因此，在执行的任何时刻，执行终止时 x 可能具有的值也仅取决于当前状态。为什么 x 在终止时必须具有正确的值？这必然依赖于某个对每个状态都为真的东西。

某个对算法（或程序）的每个执行的每个状态都为真的东西，被称为程序（或算法）的不变量（Invariant）。

如果你不了解确保程序做正确事情（例如以正确答案终止）的那个不变量，你就无法理解为什么程序是正确的。

这是我们例子中的一个不变量。我先定义 $m a x (M)$ 对于一个多重集 M 来说，是大于或等于 M 中每个元素的最小数字。所以 $m a x (M)$ 就有这个含义。程序应该在终止时满足 $x = m a x (A)$ ，这就是正确性的含义。

不变量是： $m a x ({x, m a x (B)}) = m a x (A)$ 。这是一个优美简洁的不变量。

为了证明这是一个不变量，我们必须证明它满足两个条件：

它在初始状态下必须为真。
如果它在任何状态下为真，那么它在下一个状态下也必须为真。

如果这两点都成立，那么显然它将在任何执行的所有状态下都为真，因此它是一个不变量。

为了证明不变量蕴含了正确性，我们想证明第三点： 3. 它蕴含了在终止状态下 $x = m a x (A)$ 。

为什么它在初始状态下为真？因为在初始状态下，B = A 且 x = $- \infty$ 。所以不变量条件变成 $m a x ({- \infty, m a x (A)}) = m a x (A)$ 。这是真的，因为 $- \infty$ 和任何数字的最大值就是那个数字本身。

为什么它蕴含了在终止状态下 $x = m a x (A)$ ？在终止状态下，B 等于空多重集 ${}$ 。并且 $max(\{\}) = - \infty $。所以不变量条件意味着 $m a x ({x, - \infty}) = m a x (A)$ 。左边 $m a x ({x, - \infty})$ 等于 x（因为任何数字和 $- \infty$ 的最大值是那个数字本身）。所以条件变为 $x = m a x (A)$ 。

所以第 1 点和第 3 点很简单。但是第 2 点呢？（如果它在任何状态下为真，那么它在下一个状态下也必须为真）。我不知道有多少程序员能弄清楚为什么这个条件成立。我相信你们应该学习如何证明这个条件成立。我现在没时间教你们怎么做，但理解它为什么成立是非常重要的，因为理解为什么某个东西是不变量至关重要。我认为你们应该学习如何做，因为我预计那些做不到的人将是第一批被 AI 取代的程序员。所以去学吧。

终止性（Termination）。我解释了如何证明当抽象程序终止时 x 具有正确的值，但我还没解释如何证明它总是终止。我没有时间讨论终止性。如果我有时间，我们会看到对于某些 A 的值，这个程序实际上不会终止。有人能看出是哪些值的 A 吗？（只有一两个人举手）。好吧，这是给你们的家庭作业：找出对于哪些 A 的值，这个算法不会终止。

VI. 从抽象到实现 (From Abstraction to Implementation)

我们如何实现这个算法？如何实现 $- \infty$ ？假设 A 是一个 32 位整数数组。

方法一：我们可以将 $- \infty$ 实现为最小的 32 位整数。如果这样可以接受的话——也就是说，你不在乎结果是最小可表示负整数还是真正的 $- \infty$ ——那么这很好，它给了我们一个更简单的实现。

方法二：你可以简单地将 $- \infty$ 实现为一个错误值。我之前展示的那个测试 A 是否为空的 Rust 代码，实际上就是在 $- \infty$ 被视为错误值的情况下，实现了这个抽象程序。

但是很少有程序员，事实上很少有计算机科学家，知道一个程序“实现”一个抽象程序或算法到底意味着什么，并能给出精确的定义。我现在没时间做这件事，但这是可以做到的。事实上，TLA+ 给出了一个 TLA+ 抽象实现另一个 TLA+ 抽象的精确定义。你所要做的就是用 TLA+ 表示你的程序，然后你就知道它意味着什么了。我现在没时间解释。

VII. 抽象的现实应用与价值 (Real-World Value of Abstraction)

对于真实的并发程序，“做什么”和“如何做”应该是精确的。工具应该检查“如何做”是否符合“做什么”。这里有一个 TLA+ 在实践中如何工作的例子。

亚马逊网络服务（Amazon Web Services, AWS）的人写了一篇论文。他们是实现亚马逊网络服务的那些人，构建亚马逊云基础架构的人。论文谈论了在 Web 服务中使用形式化方法。所使用的形式化方法就是用 TLA+ 语言来编写他们的抽象。

他们是这样说的：“使用 TLA+ 发现的关键洞见，找到了系统设计中的 Bug，这些 Bug 是我们所知的任何其他技术都无法找到的。” “形式化方法对于主流软件开发来说惊人地可行，并能带来良好的投资回报。” 这些人是务实的商人，编写 TLA+ 规范需要时间，但他们相信花这个时间是值得的，从真金白银的角度来看，因为它避免了 Bug。他们还说：“在亚马逊，形式化方法被常规地应用于复杂现实世界系统的设计中。” 这篇论文是差不多十年前写的了。我相信他们现在仍在使用，几年前他们还在用，但我不知道他们今天具体在做什么，但我推测他们还在用。

论文提到：“TLA+ 能发现系统设计中的 Bug，这些 Bug 是我们所知的任何其他技术都无法找到的。” 这些是根本性的设计缺陷，不仅仅是简单的编码错误。如果在代码编写完成后才发现，修复起来代价极其高昂，因为它需要大量的代码重写。而且通常，这些 Bug 直到代码发布给用户使用后才被发现，如果你是亚马逊，这简直是灾难。亚马逊的工程师在编写任何代码之前就发现了这些缺陷。

抽象仅仅对并发有用吗？处理并发的代码很重要，但这只是代码的一小部分。程序的其余部分呢？

我只知道一个案例，是整个系统从 TLA+ 抽象开始构建的。罗塞塔（Rosetta）是欧盟的一个探测彗星的航天器。它的几个仪器由一个名为 Virtuoso 的实时操作系统控制。Virtuoso 的开发人员决定从头开始编写该系统的新版本，并写了一本关于他们如何做的书。他们用 TLA+ 进行了高层设计。

这是开发团队负责人发给我的一封邮件（我之前不知道他们在做这个，是在他们出版书后我才知道的）。他在邮件中写道：“TLA+ 抽象在帮助我们获得一个更清晰得多的架构方面起了很大作用。” 他说：“我们亲眼见证了多年 C 语言编程所造成的‘洗脑’（我称之为思维僵化而非洗脑）。” 其中一个结果是，新系统的代码量大约是之前系统的十分之一。每个人都知道“第二系统综合症”——第二个系统总是比第一个大得多。但实际上，这里的代码量缩小了 10 倍。

你不可能通过更好的编码就产生少 10 倍的代码。这是通过更清晰的架构实现的，也就是更好的高层设计，更好的抽象。这来自于对抽象的思考，而不是对代码的思考；它不是来自于用编程语言思考。

有时，程序应该做什么无法被精确地表述。这里有一个我在为 TLA+ 编写漂亮打印器（Pretty Printer）时遇到的例子。输入的 TLA+ 代码（用 ASCII 编写），对齐很重要，比如这些 & 符号的对齐是有意义的。

/\ A => B
/\ C => D /\ E => F
   /\ G => H

朴素的输出可能会是这样的（因为漂亮打印不想用等宽字体）：

/\ A => B
/\ C => D /\ E => F
/\ G => H

用户可能希望这两部分对齐，所以正确的输出应该是这样的：

/\ A => B
/\ C => D /\ E => F
           /\ G => H

但另一方面，如果输入是这样的：

/\ A => B
/\ \/ C => D
   \/ E => F

朴素的输出可能是这样的：

/\ A => B
/\ \/ C => D
\/ E => F

这很可能就是正确的输出，因为用户可能不希望这些东西对齐。所以在这种情况下，这是正确的。

所以，不存在对“正确对齐”的精确定义，因为我们无法精确描述某些用户想要什么。那么，如果我们无法精确描述“做什么”，抽象就没用了，对吧？

显然是错的！程序必须做点什么。不知道它确切应该做什么，意味着我们必须抽象地思考它将做什么。不可能指定出“最好”的打印器，因为不存在这样的东西。但程序必须做点什么，而编写“意识流”代码并不能产生一个好程序。

那么我做了什么？我的抽象是什么？我写了六条规则，外加一些定义。这些都出现在代码的注释里。例如，规则说：“一个左注释标记与其覆盖标记进行左注释对齐。” 这对你们来说没什么意义，但像“左注释对齐”这样的术语，是用英语（可能加上公式或其他方式）精确定义的。

为什么我写这个抽象？因为理解和调试六条规则比理解和调试 850 行代码要容易得多。我对这些规则进行了大量的调试，并辅以调试代码来报告哪些规则被使用了。实现这些规则时出现的少量 Bug 都非常容易捕捉。如果我当初只是直接写代码，会花费长得多的时间，并且产生的格式化效果也不会这么好。

这个抽象有什么典型之处？

它位于比代码更高的层次。
我可以用任何语言实现它。
没有任何编写更好代码的方法或工具能帮助我编写这个抽象。
没有任何编写更好代码的方法或工具能让这个抽象变得不必要。
它没有说明如何编写代码。你编写抽象是为了帮助你在思考代码之前思考问题本身。

这个抽象有什么不典型之处？

它相当微妙。可能 95% 的抽象需要少得多的思考，更短、更简单的抽象就足够了。
它是一组规则。一组规则、需求或公理通常是一种不好的抽象，因为很难理解这组规则的后果。所以我不得不对这些规则进行大量的调试。但对于这个问题来说，它是正确的抽象。
正如我所说，没有一种方法对所有程序都是最好的，而这是一个不寻常的程序。

VIII. 如何更好地思考与抽象 (How to Think and Abstract Better)

在编码前思考总是比不思考要好。有人说你不应该在编码前想太多。我猜在某些情况下这是对的，但我告诉你，思考太少是一个比思考太多严重得多、也普遍得多的问题。

如何思考？“写作是大自然让你知道自己思维有多么马虎的方式。”（Writing is Nature's way of letting you know how sloppy your thinking is.）这是一位名叫 Guindon 的漫画家在某幅漫画里写的。我的说法是：“如果你思考而不写作，你只是以为你在思考。”（If you think without writing, you only think you're thinking.）

写作帮助你更好地思考。但思考也帮助你更好地写作。更好的思考帮助你写得更好。这是一个良性循环：你写得越多，你就得思考得越多，你的思考就变得更好；你的思考越好，你一开始就能写得更好。

大多数人必须学习如何写得更好。这意味着写作是为了说服他人。说服自己相信不真实的事情太容易了。你必须学会像别人可能阅读那样去阅读你写的东西。也许让别人读读你写的东西，问他们“你觉得这是什么意思？”，然后你就能看到你写的东西在哪里有歧义。

如何进行抽象思考？抽象是我擅长的。擅长抽象也是我被邀请来这里演讲的原因。我是如何变得擅长抽象的？很大程度上是通过接受数学家的教育。抽象是数学的核心。数学从两只羊和两只山羊抽象出数字“2”。这就是数学的全部意义——抽象。

但我不知道你们应该如何学习才能更擅长抽象。因为在数学中，它就是数学本身。TLA+ 教会了一些用户——我看到使用 TLA+ 的用户，它教会了他们更擅长抽象。但是 TLA+ 对大多数程序员来说可能太难了，我不知道。但也许数学家可以通过将“抽象”本身，而不是数学内容，作为教学的主题来教授抽象。我不知道，试试问问他们。

IX. 总结要点 (Key Takeaways)

需要记住的事情：

编程应该是思考（Thinking）然后是编码（Coding）。
思考需要写作（Writing）。
如果程序很简单，只需要很少的写作。但需要思考才能知道它是否简单，因此也需要写作来知道它是否简单。
对于不简单的程序，在代码层之上的抽象思考可以避免错误，并导致更好、更容易编写的代码。
一个“不简单的程序”可以是从一个完整系统到（程序中）一个复杂循环的任何东西。
没有一种抽象方式对所有程序都是最好的。但是将执行抽象为状态序列通常是一个非常好的方式。所以这是开始对你的程序进行抽象思考的一个好方法。
状态应该包含所有能影响未来可能状态的信息（除了外部输入——你可以把依赖用户输入的程序仅仅看作是做出了一个任意选择，而不用关心它为什么做出这个选择，是它自己决定的还是因为用户的输入，这对于你如何思考程序没有区别）。
在这种方法（抽象）中，程序之所以做正确的事情，是因为它满足一个不变量（Invariant）。理解程序需要理解那个不变量。
记住：不要过分纠结于语言，尤其是编程语言。

X. 附录：为什么程序“应该”有 Bug？ (Addendum: Why Programs "Should" Have Bugs?)

（这部分比我预期的要长，我可以现在停下来回答问题，或者我可以超时一点，跟大家谈谈为什么程序应该有 Bug？想让我超时的请举手？好的。）

为什么程序应该有 Bug？

我从 1957 年开始编程。现在人们编写的程序比那时复杂得多。部分原因是更好的编程语言，但主要原因是因为我们现在有程序库（Libraries），我们的程序可以使用它们。比如 Java，我过去大部分编程用 Java，我不太担心语言本身，而是它附带的所有不同的标准方法。

现在编程最难的部分是弄清楚如何使用这些库程序。因为它们中的许多永远不可能有 Bug。为什么？因为一个程序只有在存在对其“应该做什么”的精确描述时，才能有 Bug。

这个描述的一部分是与语言相关的，这部分通常很简单，并且常常通过程序如何被调用就隐含了，特别是对于强类型语言。但是最有用的程序做的是复杂的事情，你不应该需要阅读代码来理解这些事情。它们应该有一个抽象的、独立于语言的描述。

很少有程序有这样的描述。许多程序根本没有任何描述！我不会费心给你们讲那些关于这使得我使用某些库程序变得多么困难甚至不可能的恐怖故事——它们所谓的文档简直是垃圾。

相反，我会告诉你们一个在提供精确描述方面做得相当不错的组织。那就是 W3C（万维网联盟）。他们编写了 JavaScript 标准。

现在，在验证程序“做什么”是由“如何做”蕴含的方面，已经有很多工作了，始于 Robert Floyd 在 1967 年的一篇论文。但大部分工作都将程序“应该做什么”视为其输入和输出之间的关系——告诉你如果给它这个输入，它会产生什么输出。W3C 标准使用的就是这种观点。

这种观点对于大多数顺序程序（Sequential programs）来说工作得很好，我预计大多数 JavaScript 程序也是顺序的。

但在 2016 年，我制作了一个关于 TLA+ 的视频课程（你可以在网上找到），还配有用于观看的网页。它用一种很酷的方式让你利用视频，比如在正确的地方暂停视频、下载东西等等。观看课程的用户通过网页与一个 JavaScript 程序交互。这是一个并发程序。因为控制视频的代码由一个线程执行，而处理鼠标点击的代码由另一个线程执行。

执行一个库程序可以在不同的时间改变状态的不同部分。这些改变发生的顺序很重要，会对程序产生影响。这无法通过将程序“做什么”视为输入输出关系来描述。这就是为什么你必须将其视为一个执行，即状态的序列。

编写我的 JavaScript 程序最困难的部分是弄清楚如何让那些库程序在所有流行的浏览器（我用了三个）上正确地交互。需要大量的调试才能使用那些 JavaScript 方法。它看起来似乎工作正常，但无法确定它会一直保持正确工作。我们应该能够做得比这更好。

好了，就这些了。

问答环节 (Q&A)

主持人： 感谢您加入我们，帮助我们结束这一周有趣的开源活动。您还愿意回答几个问题吗？太好了。在我们开始之前，也想感谢您加入我们，并成为 SCaLE 大家庭的一员。我们为您准备了一件 T恤，就像我们所有工作人员穿的一样，希望您能自豪地穿上它。看起来前排 Chris 有个问题。

问 (Chris)： 您提到抽象对程序员来说很难学，而且大多数人现在还不知道。如果他们会了会很棒。我在想，我的数学教授过去常把计算机和计算机科学描述为本质上的“抽象的机械化”。这让我想，AI 模型似乎已经生活在一个抽象世界里了，而且我们已经有了可以检查东西的模型验证器和证明器。把抽象思维外包给机器会不会更容易些？

答 (Leslie Lamport)： 我不知道你指的是什么。我从未听说过... 我意思是，我对 AI 一无所知，除了你从报纸上读到的那些。抱歉，我说我对 AI 不了解，除了你可能从《科学新闻》或《纽约时报》上读到的。我不知道你说的 AI 程序的验证器是什么样的。因为 AI 是一个非常严重的问题，如果你试图用 AI 来构建可靠的系统。AI 的整个特点在于它解决了我们不知道如何通过编写程序来解决的问题，它产生的程序我们并不理解。所以我们不知道它们做什么，也不知道如何让这些 AI 程序可靠，比如满足某些精确的条件，像是“不撞到小孩”。这是一个巨大的、悬而未决的问题。如果我现在刚起步，这可能是我会感兴趣的问题，但我已经退休了。

问： Leslie，感谢您一生在计算机科学和编写开源软件（如 LaTeX 和 TLA+）方面的工作。我的问题是：您这一代的计算机科学学者与开源世界紧密相连，甚至在我们称之为“开源”之前就是如此，他们将自己需要的工具和想法实现为开源软件，并在互联网上与大家分享。而您之后的几代学者与开源的关系变得疏远了，尽管两个社区的人数都比多年前多了很多，但之间的桥梁却少了很多。对于我们这些试图在开源社区和学术计算机科学界之间建立桥梁的人，您有什么建议，如何建立更好的桥梁？

答 (Leslie Lamport)： 我不认为... 我想一直以来都有一些... 嗯，我在微软工作了大约 20 多年。微软在允许我们... 他们对于保密非常小心，不让外界知道内部做了什么。但微软，也许是因为它起初对研究的看法与大多数公司非常不同，他们一直将研究的主要目标之一视为提升科学本身。所以发表论文被认为是重要的一部分，一个重要的角色。

我所做的工作，我的名字出现在一些专利上，但总的来说，我所做的事情直到专利过期后才引起工业界的兴趣。基本上是因为我是在抽象层面工作的。所以我认为，应该有空间... 学者们当然应该在足够抽象的层面上工作，使得事情足够面向未来，这样他们就不应该需要去申请那些禁止他们发表工作的基金。但是，你知道，事情已经... 我认为在世界的许多方面，尤其是在这个国家，资本主义已经变得过于强大了。也许在研究领域，这也正在发生。我不知道。就我个人而言，我可以自由地发表我想要的任何东西，因为没人认为它在近期会有那么大的用处。

主持人： 也许还有时间再问一个问题，然后我们就结束 SCaLE。

问： Lamport 博士，谢谢您的演讲。我的问题有点像两部分。您谈到您认为一个问题应该在尝试用代码解决之前被严格定义。根据我的经验，这几乎从未发生过。我很少看到用像 ASN.1 这样的编码语言来定义代码的格式或协议。所以这对您来说一定非常令人沮丧，可能在您职业生涯的很长一段时间里都是如此，看到这么多人做错了，没有很好地定义。您引用了那个操作系统的例子，为太空项目编写的微内核，它首先被非常严格地定义了，他们谈到它效率有多高。我想知道您能否谈谈，处理这种看到人们没有做对的挫败感是什么样的？另外，Linux 大约有 35 年历史了，大约有 4000 万行代码，几乎没有哪部分是先通过严格定义完成的。您能否谈谈，如果像那样定义，您认为它会提高多少效率？所以，如果您能谈谈挫败感和效率方面。

答 (Leslie Lamport)： 你知道，在实际编码方面，我的经验几乎就是... 我做的编码，大概从 1957 年开始编码，所以大概是在 1970 年代早期，我才开始做我认为现在会被认为是计算机科学的事情。所以我当时在做编程，我学到了很多东西。真正的问题在于，很难量化到底获得了什么。事实上，如果你应用方法，如果有人在做软件工程，尝试两种不同的方法，典型的做法是比较方法 A 和方法 B。而我所主张的会被认为是作弊，因为我说的是：不要去做别人让你做的那个问题，那个他们认为他们想要的问题，而是去找出他们真正需要什么。

以及这整个关于敏捷编程的事情... 我不想深入讨论，但它之所以流行，似乎是因为程序员不喜欢和客户交谈，他们宁愿写程序。

所以，你知道，Virtuoso 那个例子，我认为是... 我知道的唯一一个可以指出的例子，真真切切摆在你面前的、效果非常显著的例子。但我不能保证下一次有人尝试时也会发生同样的事情。但我一直发现，我从未发现思考太多是个问题。

但我见过，比如我曾经有一个实习生，为期一年，他非常聪明。他基本上学会了 TLA+，学会了先思考、先描述清楚你想做什么再动手的理念。然后他又获得了另一个实习机会，在另一年。雇佣他的那个人说：“别写那些愚蠢的废话了，直接写代码。”

所以，是的，推销“思考”是很难的。大多数人宁愿打架也不愿思考。幸运的是，我... 最早对 TLA+ 感兴趣的人是硬件工程师。他们对“把事情做对”的概念接受度高得多，因为他们没有那种幻想，认为“哦，程序是如此容易修改，只是写点代码的事”，所以不必担心第一次就做对。你知道，用硅来实现，让你第一次就做对的动力要大得多。

而程序员通常从未意识到，在设计过程后期进行修改会是多么大的工作量。

主持人： 非常感谢您再次加入我们，帮助我们结束 SCaLE 这一周的活动。再次欢迎您加入 SCaLE 大家庭。

[掌声]

要点回顾

I. 引言：编程的核心在于思考 (Programming is Thinking)

本次演讲核心并非分布式计算或并发，而是适用于所有程序的编程思想。
许多并发编程中得到的教训适用于所有类型的程序。
核心论点：编程 (Programming) 不同于编码 (Coding)，编程更侧重于高级别的思考和设计。

II. 算法、抽象与程序 (Algorithms, Abstraction, and Programs)

算法是比程序更高级、更抽象的概念，不应局限于特定编程语言。
计算机从业者过于关注语言，应更关注思想本身。
并发程序（多线程）和分布式程序（多计算机）难以编写正确，因其存在大量可能的执行路径，调试难以覆盖所有情况。
编写并发程序的正确方法：
- 识别处理并发的部分（通常是同步，占代码量小但重要）。
- 为这部分找到一个正确的算法（可能是现有的、修改的或全新的）。
- 然后再实现 (Implement) 这个算法。
- 区分算法层面的错误和编码层面的错误；程序员擅长编码，但未必擅长找到正确算法。
对于非标准或特定程序的“算法”，称之为“程序的抽象视图”（Abstract View）或“抽象”（Abstraction）。
抽象是一种新的思维方式：在编码之前进行思考，在比代码更高的层次上思考。

III. 如何进行抽象 (How to Abstract)

对大多数程序，应编写两部分：
- 程序“做什么”（What）：定义程序的目标和功能。
- 程序“如何做”（How）：描述实现目标的步骤或机制。
语言选择：
- 对于需要工具验证“How”蕴含“What”的场景（尤其并发），需要精确语言（如 TLA+）。
- 对于大多数程序，精确的形式化语言并非必需，可以使用非正式语言（如结合英语和伪代码）。
抽象的目标是简化和清晰化。

IV. 抽象实践：计算最大值示例 (Abstraction Example: Finding the Maximum)

示例：编写函数计算整数数组 A 的最大元素。
初始“What”规范的缺陷：未定义空数组情况，导致无法实现。
通过抽象改进：
- 修正“What”：处理空数组情况（例如返回错误值）。
- 进一步抽象：
  - 不局限于整数，推广到任意数字。
  - 不局限于数组，推广到多重集 (Multiset)。
  - 修改“What”以简化“How”：定义 x 为“大于等于 A 中所有元素的最小数字”。
    - 这在 A 非空时等价于最大值。
    - 当 A 为空时，根据数理逻辑，这个值是 $- \infty$ (负无穷大)。
- 这样可以得到一个更简洁、无需特殊处理空集情况的“How”（算法）。
价值：花时间思考和优化“What”（需求/规范），可以大大简化后续的“How”（实现/编码）。

V. 证明正确性：状态、执行与不变量 (Proving Correctness: States, Executions, and Invariants)

如何确信“How”正确实现了“What”？需要证明对所有可能执行都正确。
将程序执行 (Execution) 视为状态 (State) 的序列通常是更好的方式。
- 状态：包含所有影响未来执行可能性的信息（程序变量等）。
- 步进 (Step)：相邻状态对，代表部分代码的执行。
简化执行模型：定义清晰的初始状态、步进规则和终止条件，使状态尽可能简单。
不变量 (Invariant)：在程序（或算法）的 每一个 可达状态下都为真的属性。
理解程序为何正确，必须理解其关键的不变量。
最大值示例的不变量： $m a x ({x, m a x (B)}) = m a x (A)$ (其中 $B$ 是剩余待处理元素的集合， $m a x (M)$ 定义为大于等于 $M$ 中所有元素的最小值)。
证明不变量：
- 初始状态为真。
- 如果在某状态为真，则在下一步状态也为真。
证明正确性：证明不变量在终止状态下蕴含了程序的目标（例如 $x = m a x (A)$ ）。
终止性 (Termination)：证明程序总会停止也很重要（示例算法对某些输入不会终止，这是一个思考题）。
学习理解和证明不变量是程序员应具备的关键能力。

VI. 从抽象到实现 (From Abstraction to Implementation)

实现抽象概念（如 −∞）的方法：
- 使用特定值（如最小可表示整数）。
- 使用专门的错误值/标记。
“程序 P 实现了抽象 A”具有精确的含义，尽管这里未详细展开（TLA+ 中有定义）。

VII. 抽象的现实应用与价值 (Real-World Value of Abstraction)

并发系统 (Amazon Web Services - AWS)：
- 使用 TLA+ 进行系统设计，发现了其他技术无法发现的深层设计缺陷。
- 形式化方法对于主流软件开发是可行的，并能带来良好投资回报 (ROI)。
- 在设计阶段修复设计缺陷远比在编码后修复成本低。
非并发系统 (Virtuoso OS for Rosetta spacecraft)：
- 使用 TLA+ 进行整个实时操作系统的顶层设计。
- 结果：架构更清晰，代码量相比前一版本减少了约 10 倍。
- 这证明了抽象思维带来的好处远超编码技巧改进。
处理不精确需求 (TLA+ Pretty Printer)：
- 当“What”（例如“最佳格式化”）无法精确定义时，抽象仍然极其有用。
- Lamport 为其 Pretty Printer 定义了一套规则（作为抽象）。
- 这有助于他思考、理解和调试这套规则，而不是直接编写难以管理的“意识流”代码。
- 结果是更好的、更易于维护的程序。
抽象的特点：
- 高于代码层面。
- 独立于具体实现语言。
- 帮助在编码前思考问题本身。
- 大多数抽象并不复杂，简单的抽象往往就足够。

VIII. 如何更好地思考与抽象 (How to Think and Abstract Better)

编程应是思考在前，编码在后。
思考需要书写：书写能暴露思维的不严谨之处。("Writing is Nature's way of letting you know how sloppy your thinking is.")
写作与思考相互促进，形成良性循环。
学习抽象：
- 数学教育是培养抽象能力的重要途径（数学本身就是关于抽象的）。
- TLA+ 的使用也帮助了一些用户提升抽象思维能力。
- 或许可以请数学家专门教授“抽象”这一思维方式。

IX. 总结要点 (Key Takeaways)

编程 = 思考 + 编码。
思考需要书写。
对于非简单程序，代码层之上的抽象思维能避免错误、简化代码、提升质量。
将执行视为状态序列，并寻找不变量，是理解和验证程序的有力方法。
不要过度沉迷于（编程）语言本身，应关注更高层次的思想和设计。

X. 附录：为什么程序“应该”有 Bug？ (Addendum: Why Programs "Should" Have Bugs?)

现代编程严重依赖库 (Libraries)。
使用库的最大困难在于其通常缺乏精确的规范 (Specification)。
程序只有相对于其“应该做什么”的精确描述，才能被判定存在“Bug”。
许多库没有（或只有模糊的）描述，导致无法明确判断其行为是否“正确”。
传统基于输入/输出关系的规范，不足以描述并发交互中时序依赖的行为。
需要基于状态序列的抽象描述来精确定义并发组件的交互行为。
缺乏规范使得依赖库的程序难以保证可靠性，尤其是在跨平台或库版本更新时。
结论：程序需要精确的规范才能“拥有” Bug，呼吁为库和组件提供更好的抽象规范。