工程哲学：Leslie Lamport，先思考再写代码

核心要点

• 先思考再写代码，并把思考写下来。 规约是软件中相当于建筑师蓝图的东西——“不思考则保证我们会”犯错。
• 时间并非全局，真正实在的是因果。 没有可信赖的共享时钟时，您不再追问事件何时发生，而是追问什么导致了什么。
• 先发生关系与逻辑时钟把因果形式化。 兰伯特的偏序关系，以及实现它的每进程计数器，是向量时钟与现代冲突消解的种子。
• 先精确定义正确性，再证明它。 安全性与活性、Paxos共识、拜占庭容错以及TLA+规约语言，全都源自把分布式计算当作数学而非民间传说来对待。

原则

“分布式系统是这样一种系统：一台您甚至不知道其存在的计算机发生故障，就能让您自己的计算机无法使用。” – 莱斯利·兰伯特¹

1987年他把这句话发到自己实验室的一块公告板上，它成了分布式计算中被引用最多的句子，因为它点出了直觉拒绝相信的那件事。¹您以为自己在自己的计算机上运行一个程序。其实不然。您是在一群机器上运行它，而这些机器的存在您从未一一清点过，它们的时钟互相不一致，其中任何一台都可能恰恰在最要紧的那一刻发生故障。您能装进脑子里的系统，与真正运行的系统，是两个不同的系统，而二者之间的鸿沟正是每一个分布式缺陷栖身之处。

兰伯特毕生的工作，就是拒绝用乐观把那道鸿沟糊弄过去。他的信念是：并发系统与分布式系统过于微妙，无法靠直觉推理，所以在动笔写下一行代码之前，要在纸上用数学来推理它们。“思考并不能保证我们不犯错，”他在2013年对《连线》说，“但不思考就保证我们一定会犯错。”²这思考必须写下来，因为写作正是草率思维暴露原形的地方：”要思考，您就得写。如果不写就思考，那您只是以为自己在思考罢了。”³建筑师在砌第一块砖之前先画蓝图；软件中与之对应的就是规约，而兰伯特用职业生涯的后半段反复主张：我们的系统之所以崩溃，正是因为我们跳过了这一步。⁴

更深一层的动作关乎时间本身。在物理世界里，没有一个全局时钟可供您信赖来为跨机器的事件排序——所以您必须停止追问某事何时发生，转而开始追问什么导致了什么。一次分布式计算真正的结构是因果，而非墙上的钟。⁵兰伯特所建造的几乎一切都源于认真对待这一个事实，而这也正是流淌在证据之门之下的同一信念：您不能擅自假定那个您希望成真的顺序；您必须把它确立起来。

背景

莱斯利·兰伯特于1941年2月7日出生在纽约市。⁶他1960年在麻省理工学院取得数学学士学位，随后在1972年于布兰迪斯大学取得数学博士学位，博士论文研究偏微分方程中的奇点。⁶他并非以计算机科学家的身份受训。他受训成为数学家，而且从未停止像数学家那样行事。他职业生涯的决定性特征，就是把数学的标准——精确的定义、明示的假设、用证明而非测试——带进了一个大多靠感觉编程的领域。

这些工作发生在四个机构。20世纪70年代，他在马萨诸塞计算机协会做了关于事件排序的奠基性思考。在SRI国际(1977—1985)，他做出了拜占庭将军的工作。在数字设备公司的系统研究中心(1985年起，历经康柏收购直到2001年)，他写出了Paxos，并开始了规约方面的工作。从2001年直到2025年初退休，他在微软研究院。⁶贯穿这一切，方法始终如一：找一个人人都当作民间传说来对待的分布式或并发计算问题，把它精确定义到足以陈述成一条定理，然后证明这条定理。

工作

时间、时钟与先发生关系

《分布式系统中的时间、时钟与事件排序》于1978年发表在《Communications of the ACM》上，是整个计算机科学中被引用最多的论文之一——它因分布式计算最具影响力的工作而在2000年获得了迪杰斯特拉奖。⁵⁶它的洞见看似不起眼。在分布式系统中，没有共享的、可信赖的时钟，所以您无法靠比较时间戳来为两个事件排序。您能知道的，是一个事件是否可能导致另一个事件：事件A先发生于事件B，前提是A与B在同一进程上且A在前，或者A是某条消息的发送而B是它的接收。把这些链接起来，就得到了先发生关系——被形式化的因果。⁵

那个关键而又违反直觉的推论是：先发生关系只是一个偏序，而非全序。位于不同进程、彼此之间没有任何消息链相连的两个事件，是真正并发的：关于哪个在先并不存在事实，任何假装并非如此的系统都是在臆造一个并不存在的顺序。⁵兰伯特随后给出了如今普遍被称为兰伯特时钟的算法：每个进程保有一个计数器，在每次事件时递增它，并在每条发出的消息上盖上这个值；接收方把自己的计数器推进到”自身值与消息时间戳中较大者再加一”。⁷这条简单的规则产生出与因果一致的时间戳，而它正是向量时钟、版本向量以及现代分布式数据库整套冲突消解机制的种子。

这篇论文超越其算法本身的意义，在于它改变了所问的问题。在兰伯特之前，”这件事在几点发生？”被认为在分布式系统中是可以回答的。在兰伯特之后，诚实的回答是：”问错了——该问是什么导致了它。”正是这一重新表述，使他被誉为把分布式计算从一门手艺变成了一门科学。

Paxos、共识与复制状态机

如果没有全局时钟，机器又会发生故障，那么一群计算机究竟如何对任何事情达成一致——哪笔事务提交了，谁持有锁，日志中下一条条目是什么？这个问题就是共识问题，而兰伯特的答案就是Paxos，自那以后几乎每一个容错系统的核心都有它的身影。他把它与复制状态机方法配对：如果每个副本从相同状态出发，并以相同顺序施加相同的命令序列，它们就会保持完全一致——于是把分布式系统保持一致这整个问题，归约为就命令的顺序达成一致，而这恰恰正是Paxos所提供的。⁶

Paxos如何发表的这段故事，是该领域最著名的警世传说。兰伯特把它写成《兼职议会》，把算法包装成一座虚构的古希腊岛屿——名为Paxos——上的立法程序，连立法者都顶着把同事姓名作伪希腊音译而成的名字。⁸这个玩笑是一场灾难。审稿人以为他不是认真的；论文被以无足轻重为由退稿；听过他演讲的人记住了那套印第安纳·琼斯式的设定，却没记住算法。⁸它就这样多年未能发表。《Communications of the ACM》的编辑最终于1998年把它发表在《ACM Transactions on Computer Systems》上——却仍裹在那则寓言里。⁸当整个领域继续无视它时，兰伯特终于投降，于2001年写下《Paxos Made Simple》，剥掉那层希腊外衣，露出他始终坚称底下藏着的那个确实简单的算法。⁸他得出的教训不是”人们很蠢”。而是：即便一个正确而重要的想法，只要您把思考遮蔽起来，它也会失败——表达是工作的一部分，而非工作之外的事。

拜占庭将军问题

1982年，兰伯特与罗伯特·肖斯塔克、马歇尔·皮斯一道发表了《拜占庭将军问题》，为该领域赋予了描述最难一类故障的语言。⁶与拜占庭式的部件相比，崩溃的部件算是容易对付的——拜占庭式部件不会停下，而是会撒谎，向不同的同伴发送各异且互相矛盾的信息，无论这是出于缺陷、损坏还是恶意。论文的设定是：一支军队的若干师，各由一位将军统领，必须通过信使就唯一一套方案——进攻还是撤退——达成一致，而其中某个数量未知的将军是叛徒，正积极阻挠达成一致。兰伯特证明了一个系统在仍能达成一致的前提下能容忍多少叛徒的精确阈值，把”万一某个节点撒谎呢？”从一桩模糊的忧虑变成了一条带有明确界限的定理。

那条定理是每一个必须在部分参与者怀有敌意时仍能持续运转的系统的思想根源——也正因如此，几十年后，拜占庭这个词才会处在区块链共识的中心。兰伯特并非要去使加密货币成为可能；他是要去精确定义：当”故障”包括背叛时，容错究竟意味着什么。

TLA+与规约(以及，没错，LaTeX)

贯穿兰伯特职业生涯的主线，是”必须先规约再编码”这一信念，而TLA+就是这一信念被打造成的工具。时序行为逻辑(Temporal Logic of Actions)是一种语言，用来为一个系统应当做什么写下精确的数学描述——它的各种状态、状态之间的步骤，以及它必须始终满足(安全性：坏事永不发生)和最终达成(活性：好事终将发生)的性质，这两个概念都由他形式化。⁶您写出规约，模型检查器便会遍历状态空间，去找出那个会破坏您不变式的微妙交错——那个您靠测试永远不会发现的缺陷，因为它只在三台机器以您从未设想过的顺序做三件事时才会出现。他的论证就是建筑师的蓝图：您在浇筑混凝土之前先把建筑画出来，而软件规约就是同一张蓝图，用数学写就，因为数学是我们拥有的最精确的语言。⁴

还有一座更安静的丰碑。20世纪80年代初，兰伯特在唐纳德·克努特的TeX之上构建，写出了LaTeX——这套宏系统成了科学家与数学家排版文档的默认方式，也是一整代论文与学位论文呈现出如今模样的原因。⁶这是一件典型的兰伯特式产物：他需要精确地写下自己的工作，于是就造出了让所有人都能这么做的工具。催生TLA+的那种本能——一套强制精确的记号——与催生LaTeX的本能如出一辙。

方法

这套方法，是一个被坚持不懈地应用了五十年的想法：思考即工作，而思考必须在代码之前写下来。

按因果推理，而非按时间。 没有可信赖的全局时钟，所以不要按事件何时发生来排序，而要按什么导致什么来排序。先发生关系，而非墙上的钟，才是真正的结构——而接受两个事件是真正并发的，比臆造一个顺序更诚实。⁵

先规约，再编码。 对于任何没有既定解法的事情，先停下来思考，而这思考独立于编码。把蓝图——也就是规约——用数学写出来，因为在散文含糊之处，数学是简单而精确的。⁴“不思考则保证我们会”犯错。²

靠写作来检验您是否真在思考。 写作是检验一个念头是否真实的试金石。”如果不写就思考，那您只是以为自己在思考罢了。”³一个您写不下来的规约，是一个您尚未真正拥有的想法。

精确地定义那种故障。 “万一某个节点撒谎呢？”在您把它陈述为拜占庭将军并证明容错界限之前，都只是民间传说。精确的定义把忧虑变成定理。⁶

表达是正确性的一部分。 Paxos正确了好几年，却没人能用，因为那则希腊寓言把想法埋没了。一个没人能理解的正确结果，作为工程尚未真正完成。⁸

影响之链

谁塑造了他

数学本身。 兰伯特受的训练是数学博士，而非计算机科学，而他贡献的整个形态，就是把数学的标准——定义、公理、证明——引入一个此前一直靠直觉编程的领域。⁶(奠基性影响)

20世纪70年代真实系统中的容错问题。 SRI在飞机可靠性系统上的工作，以及机器在协议中途发生故障这一现实中的恐怖，给了他一些具体问题——拜占庭故障、共识——它们要求那种他天生擅长给予的形式化处理。⁶(直接影响)

艾兹格·迪杰斯特拉。 认为正确性靠证明而非测试来确立、认为并发程序必须被形式地推理，这一信念在成为兰伯特的之前，先是迪杰斯特拉的。兰伯特凭其时钟论文所获之奖，正以迪杰斯特拉之名命名。(直接影响)

他塑造了谁

每一个分布式数据库、云平台与区块链。 逻辑时钟支撑着分布式存储中的冲突消解；Paxos(及其后裔Raft)是谷歌Chubby与Spanner、ZooKeeper、etcd以及基本上每一朵云的协调层的共识内核。拜占庭将军这一结果，是比特币以及自那以后每一个容错共识协议之下的理论地基。

工业界的形式化方法。 亚马逊云服务以使用TLA+著称，在交付S3、DynamoDB及其他核心服务之前先对它们进行规约与检查——在设计中、而非在生产中找出微妙的缺陷。兰伯特的蓝图论证，从异端走向了实践。

这个领域的词汇。 先发生、安全性与活性、复制状态机、顺序一致性、拜占庭故障——这些与其说是兰伯特对分布式系统语言的贡献，不如说它们在很大程度上就是那套语言。

贯穿其中的主线

艾兹格·迪杰斯特拉主张，您要在运行程序之前先推理它的正确——测试只能显示缺陷的存在，永远无法显示其不存在——而兰伯特是其直接的继承者，把”先证明、后执行”从顺序程序带进了远为艰难的并发世界，在那里，那个您无法测试的缺陷是常态而非例外。芭芭拉·利斯科夫以数据抽象与可替换性，把对程序行为的形式推理变成了一个可用的原语；兰伯特则把对系统随时间之行为的形式推理立为标准，所规约的不是一个对象保证什么，而是整个并发系统必须始终以及最终做什么。还有唐纳德·克努特，他为算法分析带来了数学上的严谨，并近乎顺带地造出了TeX，好让那些工作能被精确地落到纸上——这与兰伯特几乎严丝合缝地押韵，后者出于同一理由在它之上构建了LaTeX，并把规约本身变成一种数学行为。三位数学家，都拒绝让”看起来能用”算作”知道”。(系列之桥)

我从中得到什么

我所铭记的教训是：思考即工作，而思考在被写下来之前并不真实。兰伯特的蓝图论证之所以令人不安，是因为它是对的：一个系统在生产中崩溃的原因，几乎从来不是代码打错了——而是没有人规约过系统在并发与故障之下究竟应当做什么，于是根本就没有一份陈述可供拿来核对代码。这门规矩，是先于实现写出规约，用一种精确到足以让其内部矛盾显形的语言来写。这与质量是唯一的变量是同一个标准：问题从来不是”这个能通过顺利路径吗？”而是”我有没有精确地陈述出什么必须始终为真——并证明设计遵守了它？”这也正是我为何如此倚重先写PRD再写代码；一份PRD就是一份穿着工装的兰伯特规约。

在我如今所构建的世界里——智能体、工具循环、多智能体系统——兰伯特的教训正是几乎人人都跳过、并为之付出代价的那一条。一个智能体系统就是一个分布式系统：彼此独立的进程，没有全局时钟，乱序到达甚至根本不到达的消息，以及悄无声息地故障、或更糟地撒谎的组件。缺陷从来不在提示词里；它们在顺序里——两个智能体基于陈旧状态行动，一次工具调用的结果在那个需要它的决定之后才到，编排器假装为之排好了序的一对”并发”事件。兰伯特的规矩，是停止信赖墙上时钟那套直觉，明确地就因果与故障进行推理，并在把任何东西接线连起来之前，先写下什么必须始终为真。先规约再构建、对一个系统进行推理而非戳弄它的这一信念——正是从1978年那篇关于时钟的论文一路贯穿到2026年某个代理框架的主线，也正是我为何把一个系统的性能与正确性当作您设计时就植入的属性、而绝非寄望事后再调试找回来的原因。

常见问题

莱斯利·兰伯特的工程哲学是什么？

兰伯特的信念是：并发系统与分布式系统过于微妙，无法靠直觉推理，所以您必须在纸上用数学来思考，然后才写代码——就像建筑师在砌第一块砖之前先画蓝图。软件蓝图就是规约，用数学写就，因为数学是可用的最精确的语言。⁴在这之下，还有一种对待时间的立场：在分布式系统中，没有可信赖的全局时钟，所以一次计算真正的结构是因果——什么导致了什么——而非事情何时发生。⁵“思考并不能保证我们不犯错，”他说，”但不思考就保证我们一定会犯错。”²

什么是兰伯特时钟与先发生关系？

先发生关系是兰伯特对分布式系统中因果的形式化：事件A先发生于事件B，前提是它们在同一进程上且A在前，或者A发送一条消息而B接收它，或者通过把这些链接起来。⁵它只是一个偏序——位于不同进程、彼此之间没有消息相连的两个事件，是真正并发的，没有任何正确的系统能宣称其中之一在先。⁵兰伯特时钟用每进程一个计数器来实现它：每次事件都递增它，每条发出的消息都盖上这个值，接收时把自己的计数器推进到”自身值与消息时间戳中较大者再加一”。⁷其结果是一组与因果一致的时间戳——这正是向量时钟与现代分布式冲突消解的基础。

什么是Paxos与拜占庭将军问题？

Paxos是兰伯特用于共识的算法——让一群不可靠、可能发生故障的机器就单一一个值达成一致，比如复制日志中的下一条命令——它支撑着几乎每一个现代分布式系统的协调层。众所周知，他最初把它发表成一则关于虚构希腊议会的寓言(《兼职议会》，《ACM TOCS》1998)；这个玩笑把想法遮蔽得太厉害，以至于他最终在2001年把它重写成《Paxos Made Simple》。⁸拜占庭将军问题(兰伯特、肖斯塔克与皮斯，1982)定义了最难的那种故障模式——不只是崩溃、而是会撒谎、发送相互矛盾信息的组件——把它设定为一群将军试图就方案达成一致，而其中的叛徒却在破坏达成一致，并证明了一个系统能容忍多少叛徒。⁶它是区块链共识的理论根源。

莱斯利·兰伯特为何获得图灵奖？

ACM授予兰伯特2013年A.M.图灵奖，”以表彰其对分布式与并发系统理论及实践的根本性贡献，尤其是因果与逻辑时钟、安全性与活性、复制状态机以及顺序一致性等概念的发明”。⁶这则颁奖词概括了他工作的广度：他用精确的定义与证明，把分布式计算从民间传说变成了一门科学，赋予了这个领域它的大部分词汇，创造了TLA+规约语言，让”先规约再编码”成为一门可行的规矩，并且——在克努特的TeX之上构建——写出了LaTeX，这套排版系统成了科学与数学领域的标准。⁶

来源