重新设计数据密集型应用|定理|正确性|算法|设计数据密集型应用

《设计数据密集型应用》（DDIA）第二版终于出了。

这本书不用我多介绍了——过去九年里，它是分布式系统领域当之无愧的圣经，也是我翻译过的最有价值的一本书。第一版中文翻译在 GitHub 上攒了两万多颗星，说明大家是真的需要这样一本书。

第二版的变化不小。Martin 把整个存储层的假设从本地磁盘换成了对象存储，补上了这些年云原生架构的演进，也更新了不少案例和观点。 https://ddia.vonng.com —— 说实话，这次主力是 AI，我做的是校对和润色。但效果已经足够流畅通顺，完全不影响阅读。需要的朋友可以直接取用。

巧的是，就在昨天，Martin 和第二版的合著者 Chris Riccomini 一起上了 Antithesis 的 Bug Bash 播客，聊了差不多一个半小时。话题很杂也很有意思：DDIA 第二版改了什么、为什么现在所有数据库都在往 S3 上搬、CAP 定理为什么早该扔进垃圾桶、形式化验证到底有没有用，以及 AI 写代码到底行不行。

我把视频扒了下来，转录成文字稿，翻译成了中文——这一整套流程全是 AI 干的，我基本没怎么动手。这大概也算是 AI 时代的内容生产方式了：从语音转文字到翻译到排版，几分钟搞定一万多字，质量还说得过去。

最后，我也就播客里的几个核心观点聊了聊自己的看法——特别是关于对象存储取代本地磁盘、 CAP 定理的历史遗留问题、以及软件测试的残酷现实。不一定对，但保证说的是真话，供各位参考。

YouTube 链接： https://www.youtube.com/watch?v=UHdPnubbzBI

Bug Bash 播客：《设计数据密集型应用》第二版幕后故事

嘉宾：Martin Kleppmann、Chris Riccomini 主持人：David Win

欢迎收听 Bug Bash 播客，在这里我们聊一切与软件正确性和可靠性相关的话题。我是主持人 David Win。距离《设计数据密集型应用》成为分布式系统标准教材已经过去了 9 年。今天，Martin Kleppmann 和 Chris Riccomini 来到节目中，为大家揭开即将出版的第二版的幕后故事。毕竟，本地磁盘的时代正在让位于云原生对象存储，我们将探讨为什么现代数据库正在围绕 S3 进行彻底重构。接下来，我们还会重新审视 CAP 定理，以及为什么也许是时候用“离线可用性”的概念来取代它了。我们还会进入一场出人意料的实用性 AI 讨论——探索大语言模型为什么在创造性设计方面可能表现糟糕，但在验证复杂系统迁移时却是完美的测试预言机。这期节目你一定不想错过。

在开始今天的节目之前，快速说一句：如果你想在现实中结识同样关心软件正确性和可靠性的人，可以考虑参加 Bug Bash 大会，时间是 4 月 23 日至 24 日，地点在华盛顿特区。所有详情请访问 bugbash.antithesis.com。

一本经典的诞生

David： 好的，欢迎大家收听 Bug Bash 播客。今天我们有一对非常令人激动的嘉宾——Martin 和 Chris，他们是全世界（至少是我的世界里）每个人最喜欢的那本书——《设计数据密集型应用》第二版的合著者。也就是那本我希望自己刚开始写分布式系统时就能拥有的书，但那时候没有，所以我只能用最笨的方式把所有坑都踩了一遍。欢迎 Martin，欢迎 Chris。

Martin： 谢谢。

Chris： 嗨，Will。很高兴来到这里。

David： 我觉得我们可以聊的话题太多了，但我首先想问的是——我知道刚才我有点在你们面前夸张了一下—— 但我觉得说《设计数据密集型应用》已经成为分布式系统实践者的圣经并不为过。它就是那本书。每当我看到有人在问怎么学习这个既棘手又复杂的学科时，它总是第一个被推荐的。而且我认为这是有充分理由的，这本书写得真的非常非常好，而且非常全面。我很好奇，这是你当初的意图吗？你是本来就打算把它写得这么大部头的，还是这一切是偶然发生的？如果是后者，你觉得原因是什么？

Martin： 关于第一版的问题我来说吧。确实没有打算把它写得这么大。最初的目标是 400 页，后来变成了 600 页。我真的只是想写一本我自己希望当初入门时就有的书。我发现每次在网上查资料时，要么碰到的是那种充满学术术语、极难理解的深度研究论文，要么就是试图让你买产品的空洞营销软文，根本没说清楚实质内容。所以我想要找到这两个极端之间的平衡。

David： 这本书的反响有什么让你意外的吗？你看起来是个非常低调的人，我猜你应该没预料到它会变得这么受欢迎。有没有哪些章节的反响比你预期的好或差？

Martin： 总体来说，我当时觉得分布式系统是一个非常小众的领域——谁在乎分布式系统呢？这是很专业的东西。我当时想，大多数只是使用数据库的人根本不需要了解这么深入的细节，看看数据库手册就够了。我主要针对的是那些需要为特定应用选择数据库系统的人，因为可选的实在太多了。我当时觉得这会是一小群高级架构师之类的人。完全没想到它会变成一个如此主流的东西。

David： 我觉得这本书之所以如此成功，我个人也非常喜欢的一点是——它实际上不仅仅是一本关于分布式系统的书。虽然它是以分布式系统为框架来写的，但它实际上传达了一些关于设计任何类型系统的深刻智慧，甚至不限于软件系统。它在某种程度上是一本通过分布式系统这个镜头来表达的通用工程智慧合集。我觉得这正是你成功融合不同抽象层次的方式之一。我不知道还有什么别的书能做到这一点。

Martin： 是的，我真的很想让它有实感，所以放了很多案例研究和与真实场景的关联。你知道，当你听到那些有趣的故事，比如海底光缆因为鲨鱼咬断而中断——你就觉得“这必须写进去”。当然，这些故事最终都被纳入到我们试图阐述的一般性原则中，所以它不仅仅是轶事集，而是真正在从这些案例中提炼和归纳。但我觉得这些小花絮让内容更有真实感，让读者相信这确实是真实系统运作的方式，因为里面包含了这些来之不易的经验。我花了很多时间翻阅各种生产事故的事后分析报告，看看能不能从中提取出有趣的教训，融入到叙述中。

为什么需要第二版

David： 那你们为什么决定需要出第二版？你们最期待第二版中的什么内容？行业发生了哪些变化，书的内容又有哪些变化？

Martin： 其实第二版的必要性已经很明显了，因为第一版正在变得过时。它已经 9 年了。而且最初几章是在出版前几年就开始写的，所以那些章节大概已经有 12 年了，这期间事情不可避免地会发生变化。我当时确实尽量聚焦于一般性原则，而非某个特定软件的最新版本，以便它能有一定的持久性。但尽管如此，事物还是在变化。

比如一个重大变化是：第一版基本上假设分布式系统中的一个节点就是一台带有本地磁盘的机器。如果它要存储数据，就写入本地磁盘；如果要复制数据，就通过网络发送给另一台机器。但现在我们有了云原生系统，你写入的可能不是本地磁盘，而是对象存储，而对象存储本身就是一个分布式系统——我们在服务之上层叠服务。这是一个根本性的设计变化，深入到了人们构建分布式系统和数据系统的基础层面，我们必须在书中反映出来。

从本地磁盘到对象存储

David： 你们觉得这个变化为什么会发生？这确实是一个巨大的范式转变。以前大家的假设是“显然你会有一块超快的 SSD，然后优化你的存储引擎来利用它”。而现在大家觉得“显然你会有超高吞吐量的分解式对象存储，一切都依赖于它”。每个现代数据库都在这样构建。那你们觉得是什么关键因素促成了这个转变？Chris，我觉得你在这个领域有特别的见解。

Chris： 是的，这主要来自我的个人经验。云系统对我来说最大的吸引力始终是——我可以付钱让别人替我值班。本质上这是一个 运维问题。如果我可以花钱不用担心复制、网络分区、节点通信中断、凌晨三点被叫醒、数据损坏这些事——这些东西真的一点都不好玩，纯粹是痛苦。无论是计算端还是持久化端都是如此。能把这些甩给第三方、有人负责真的很好。

但我确实觉得这在某种程度上是一种幻觉，因为现在你的云系统出了问题，你得去弄清楚——谁改了这个存储桶的访问控制？谁做了这个部署？为什么系统在降级？原来是有个“吵闹的邻居”之类的问题。所以它并不是一个完美的解决方案。但我觉得大概 15 年前大家的想法是“这好太多了，我只需要调一个接口就行”。

David： 你觉得如果 S3 没有添加强一致性支持，这个转变还会以同样的速度和方式发生吗？

Chris： TurboPuffer 的创始人 Simon Eskildsen 有一个非常好的演讲，详细梳理了导致像 TurboPuffer 这样的系统以这种方式构建的关键时间线。他指出的一个重点是，S3 实际上很晚才获得强一致性支持——大概是 2020 年之后。所以我觉得，是的，即便在 S3 获得强一致性之前，这个转变就已经发生了。当然，Google Cloud Storage 很早就有了强一致性。在我看来，即使没有 S3，只要有了按需获取机器的能力、Kubernetes、EBS 这些基础设施，转变也会发生。

Martin： 我想补充一点，拥有强一致性以及能够做原子的比较并交换（Compare-and-Swap）操作，确实能让构建在对象存储之上的分布式系统变得简单得多。因为你本质上可以把共识外包给对象存储。以前人们需要使用 ZooKeeper 或 etcd 来把共识外包给另一个系统，而现在把它集成到对象存储中是一个很大的简化。

Chris： 没错，真的很棒。我们前几年开始做一个项目，基本上就是一个构建在对象存储之上的键值存储，灵感来自 TurboPuffer 和 WarpStream 这些云原生数据库。最近我们发现，其实可以把它拆解成独立的组件——一个自动做栅栏（fencing）的事务对象（因为有了 Compare-and-Swap，在对象上做栅栏简直是小事一桩）、一个分布式队列（TurboPuffer 最近也发了相关文章）、一个预写日志（类似 WAL3 和 Chroma 的做法）。 Martin 说得完全正确：一旦 S3 和 GCS 有了前置条件机制，你基本上就能非常轻松地构建所有这些原语，然后以各种很好的方式组合它们。

David： 是的，我们 Antithesis 实际上构建了自己的分析数据库引擎—— 因为市面上没有分析数据库支持一种时间会分叉的数据模型（我还以为每个人都生活在这样的世界里呢）。但真正的关键技术认知是：你不再需要自己写存储引擎了。这一点极大地降低了做这类事情的门槛。

Chris： 百分之百同意。现在你可以看到一个数据库技术栈：底层是持久化层，往上一层是像 DataFusion 或 DuckDB 这样的查询引擎，再加上 Parquet、Lance、Nimble 这些优秀的文件格式。你现在完全可以把这些组件叠加起来做一个分析数据库，效果还相当出色。Polar Signals 最近也做了类似的事情。

合著者的故事

David： 能跟我们讲讲合著者的故事吗？Martin 你说过这本书已经存在大约十年了。Chris，当时你是在 WePay 吗？

Chris： 其实当时我在 LinkedIn，就坐在 Martin 旁边，直到他去休假。

Martin： Chris 当时在 LinkedIn 做 Samza 这个流处理器。我是通过之前创业公司被收购进入 LinkedIn 的。后来我们团队被解散了，我需要找新团队。我听说 Kafka 团队在做很有意思的事情，就联系了 Jay，问他能不能加入。然后他把我介绍给了 Samza 团队，我就开始和 Chris 一起工作了。

Chris： 对，大概是 2012 或 2013 年。那时候你刚开始写书的前几章。我记得你去休假后，给我发了一封邮件，附件是一个包含前几章的 PDF。我看到后就觉得“这太棒了”。那时候内容还很厚重。看着它逐渐成形、出版，并获得如此好的反响，真的很酷。

Martin： LinkedIn 很慷慨地给了我 50%的时间来写书，所以我一半时间做软件工程师和 Chris 一起工作，另一半时间写书。后来我发现同时做这两件事真的很难——我们当时在把 Samza 部署到生产环境，总有各种生产问题需要处理，很难从那种状态切换到一个多年写作项目上来。所以后来我干脆请了假，自掏腰包全职写书。然后不知不觉就滑入了学术界——在大学找到了一份可以做有趣研究的工作，同时完成了这本书。

到了写第二版的时候，我一开始是自己写的，但后来意识到我已经落后于当前的行业实践了。毕竟我已经退缩到学术界的象牙塔里了。虽然对 2014 年左右的技术还算了解，但完全错过了之后发生的事情。不过我一直在看 Chris 写的博客和通讯，从中获得了不少有用的洞见。后来突然灵光一闪——我应该让 Chris 作为合著者加入。于是我给 Chris 发了封邮件说“你有兴趣吗？”他说“有”。

创业、大公司与学术界

David： 你们两个都经历过创业，也都在大型企业里当过螺丝钉，Martin 你还待过学术界。能不能给我们一些犀利的比较和对比，这些不同的生活方式和职业路径各有什么特点？

Chris： 我最犀利的观点是：公司规模其实没那么重要。在 Google 工作和在 JP Morgan 工作，即使都是大公司，体验也完全不同。我发现自己越来越关注的是：这家公司是不是以技术和工程为驱动的？它的世界观是否与我的兼容？我在 JP Morgan 最痛苦的时候就是文化上与他们根本不同——他们是银行，技术对他们来说只是工具，这可以理解。但技术对我来说是一种热情。

我有一个之前在 WePay 的同事后来去了 ClickHouse，她跟我喝咖啡时说：“如果你真的对数据库充满热情，你就应该去一家数据库公司工作。” 这话听起来简单得令人震惊，但又出人意料地不显而易见。所以我的观点是：不要太在意公司大小，要关注你的价值观和世界观是否与公司的领导层和方向兼容。

Martin： LinkedIn 是我待过的唯一一家大公司，所以我没什么比较基准。我觉得他们做得不错，但我不太适合大公司的风格。我有很多自己想做的事情，更喜欢自由地探索和试错，而不是遵循预设的 OKR 之类的框架。创业适合我，因为你就是在疯狂地尝试各种事情。学术界也适合我，因为研究非常自由开放。两者的区别主要是时间尺度——在创业公司你要在几周到几个月内交付；在学术界我可以用几年甚至几十年的尺度来思考问题。我现在很珍视这种自由——可以做自己认为重要的事情，不需要它现在就具备商业可行性。但我也尽量把创业思维带入研究中，保持对“做出真正有用的东西”的关注——这一点在学术界有时会被遗忘。

CRDT、端到端加密与本地优先协作

David： 我记得你刚进入学术界时，我们聊过，你说在研究用 CRDT 和类似的数据结构来实现隐私保护的协作工具。这个项目现在还在进行吗？进展如何？学到了什么？

Martin： 基本上还在继续。我开始做这个已经大约 10 年了，这就是我说的“以十年为尺度”的含义。有一些非常难的问题确实需要很长时间来解决。

David： 这家公司绝对不会因为你花了很长时间而批评你——我们已经干了八年了。

Martin： 我最初的目标是做一个类似 Google Docs 但具有端到端加密、去中心化的东西，这样我们就不需要那么依赖 Google 的服务器了。然后我开始在 CRDT 上做大量工作来实现去中心化协作。但比如端到端加密这部分，直到最近才开始成型。就在过去一年左右，我在 Ink & Switch 的合作者们构建了一个叫 KeyHive 的库，它在我们的 Automerge CRDT 库之上添加了端到端加密和基于密码学身份系统的去中心化访问控制。这是一个漫长的过程，而且远未完成——软件还没有正式发布，我们确实需要做一些形式化证明来验证它的正确性。要真正投入实践可能还需要几年时间。但这基本上就是我这些年一直在持续推进的事情——一个小项目接一个小项目，逐步提高数据结构的效率，让它们能做以前做不到的事情。

形式化证明与模型检查

David： 你提到了形式化证明，这对我们来说总是很有趣的话题。作为来自工业界的人，我注意到形式化证明在学术界占有重要地位，但我很少看到它们被用在日常的工业软件项目中——尤其是在项目已经上线、正在被积极扩展、维护和性能优化的阶段。即使以前做过证明，我也很少看到有人回去维护它。Chris，你们在 Slate DB 中使用了 FSB，对吧？

Chris： 是的，这是我们尝试过的工具套件中的一部分。我们最初使用 Fizzbee（FSB）来定义清单管理协议。让我先解释一下背景：Slate DB 就是我之前提到的构建在对象存储之上的键值存储。你可以把它想象成 RocksDB——一个单节点的键值存储，可以进行 get、put、delete、scan 操作——但它把所有数据持久化在对象存储上，可以完全不依赖本地磁盘运行。底层使用了一种叫日志结构合并树（LSM Tree）的存储策略。简单来说就是：所有写操作都追加到日志中，然后定期读取日志进行“压缩”——也就是去除重复的键，只保留最新版本。这既是一个极大的简化，也基本上就是事实。

David： 在这个场景下，FSB 是什么？你们怎么使用它？

Chris： Fizzbee 是一个形式化证明系统，也有一些基于模型的测试方面。它的要点是：你用一种小型语言定义你认为系统应该有的行为，定义预期结果，然后它会遍历所有不同的状态组合来验证你的不变量是否成立。比如，如果我向 Slate DB 写入一个键，然后调用 get 读取这个键，无论发生什么，我都应该 100%能拿到值。底层 Slate DB 做了很多事情——写预写日志、压缩数据等等。 FSB 会模拟那次写入操作，运行代码中所有可能的执行路径变体，然后在每个路径上检查：如果我在这个流程中的任何地方调用 get，是否总能拿回值。

不过有一点很重要：FSB 和大多数这类系统（TLA+ 等）实际上并不直接关联到你的代码。你是在 FSB 的语言中定义你认为代码会如何行为。所以它非常适合测试设计，但要测试实际实现就更困难。 FSB 的作者 JP 最近添加了一些基于模型的测试功能，提供了 Rust、Python 等语言的钩子，可以插入你的实际代码。但总体来说，设计和实现之间一直存在这道鸿沟。

这也回应了你之前的问题——为什么系统上线后就很少看到有人用这些工具。系统上线后，它在不断变化，有很多其他测试方式，有用户提交的 bug 报告，有新功能开发。这些工具就被搁置了，因为使用成本不低。大多数这类语言本质上非常数学化。我们选择 FSB 的一个原因是它使用 Starlark 语言——一种简化版的 Python，对开发者来说比其他工具更容易上手。

Martin： 我来补充几句。正如 Chris 所说，验证规范和验证实现是有区别的。我也认为大部分价值其实来自验证规范——用计算机作为工具来检验我们自己的思维，看看当考虑到那些我们人类可能没想到的奇怪边界情况时，我们对系统行为的假设是否站得住脚。一旦规范通过了验证，我觉得大部分价值就已经获得了。

当然，翻译成实现时可能会引入 bug，但为了形式化验证实际实现所需的额外工作量，往往与收益不成比例。对实现做一些基于属性的测试（Property-based Testing）是很有价值的，那算是比较容易摘到的果子。但如果你想真正使用证明助手来证明代码的定理，那工作量就太大了。

我对大语言模型持谨慎乐观态度——未来它们可能会擅长写形式化证明，到时候我们就可以把这些工作外包给 AI 代理。而且即使它产生幻觉也没关系，因为证明检查器只有在证明真正严谨的情况下才会接受。这似乎是 LLM 一个非常好的应用场景。但我自己还没真正尝试过。

我用 Isabelle 证明助手做过一些形式化验证工作。 Isabelle 不像模型检查器那样只能在有限状态空间内测试，它可以在无限状态空间上进行推理，真正证明某个属性在所有可能情况下都成立。但写这些 Isabelle 证明的过程极其耗时。不过，在我们试图设计一个非常精妙的算法、不做证明就完全不知道它对不对的情况下，这是非常有价值的。

实际上，写证明的过程本身才是帮助我们理解算法为何正确（或不正确）的关键。最后得到一个证明产物只是一个副产品。写证明不是因为我们想要最终那个证明，而是因为我们想在头脑中获得那种理解。我越来越看重证明助手这一点。虽然它极其耗时，但它极大地磨砺了我自己的思维——被迫一步步写出那个“愚蠢的机器”愿意接受的证明。因为在写证明的过程中，我无数次碰到那种“这显然是对的”的地方，花了半个小时试图证明它，然后发现——不，有反例。所以写证明这个过程让我在结构化思考方面变得更好了，即使我不再用证明工具了。

David： 这对我来说非常有道理——对很多复杂的认知任务来说，有一种强迫自己逐步严谨思考的方式，会让你的思维变得更好、更锋利。但这就引出一个有趣的对比：如果 LLM 能替我们写证明，但很多价值就在于写的过程和那种挣扎，那如果我能按个按钮、去喝杯咖啡、回来就看到 Isabelle 证明摆在那里——我们还能获得那些好处吗？

Martin： 这是一个很好的问题。我不确定，可能得试试才知道。目前写证明时很多时间是花在非常令人沮丧的事情上——比如琢磨“到底该用什么归纳假设才能证明这个引理，然后才能推导出那个引理”。就是在一些很小的引理上反复磨——比如我只是想证明列表追加操作的结合律——“这明明很显然，为什么这么难？” 如果 AI 能帮我去掉这些苦力活，让我们专注于证明的高层步骤，我觉得这本身就是巨大的收益——既能降低挫败感和时间成本，又能让更多人不用读完博士、不用花几年学习那些晦涩的证明策略就能写这些证明。所以我觉得自动化更多证明过程大概率是净收益。

半形式化方法

David： 去年 Bug Bash 大会上有一位演讲者叫 Ankush Desai，当时在 AWS，现在在 Snowflake，他是形式化方法语言 P 的开发者。 P 专门针对分布式系统推理做了优化。他做了一个非常精彩的演讲。他说了一句话，可能比你的观点更极端——他大意是说：“我从形式化方法中获得的 90%的价值，是在运行模型检查器之前就获得了。” 关键价值在于，它强迫你坐下来真正思考你的系统到底在做什么——如果没有这个过程，你很容易就跳过这一步。

我们在 Antithesis 内部确实也用了一些形式化方法——这可能会让一些人吃惊，因为他们以为我们是反形式化方法的。其实不是。我们在所有安全关键的部分大量使用基于证明的技术。

我们做的一件事是吸取了 Ankush 的建议：我们有一种“半形式化证明”——不是机器可检查的，但人类可检查。它有一些定义和术语无法被完全还原为纯逻辑描述，但它仍然具有证明的整体语义结构——引理、蕴含、量化等等。这是一个很好的平衡：你可以进行形式化推理风格的思考，捕捉到你否则不会发现的错误，但避免了那种与检查器没完没了地争论的痛苦。而且它允许在某些术语无法以计算机满意的方式定义的领域中使用。我不知道这会不会流行起来，但我们一直管它叫“半形式化方法”。

Chris： 我听说有人管它叫“Smart Casual”——从“formal”降一个档次。

David： 有句话我很喜欢——有人说过“写作是大自然展示你思维有多模糊的方式”。然后 Leslie Lamport 在此基础上说：“数学是大自然展示你的文字有多模糊的方式。” 再进一步，证明助手是大自然展示你的数学有多模糊的方式。

Chris： 这整个话题让我觉得它和写作本身有着平行关系。你一旦试图把什么东西写成书、写成博客、写成设计文档，你马上就开始碰撞你实际的心智模型，发现其中的错误和空白。所以这个对话完全可以推广到任何以写作为基础的活动。

AI 在第二版写作中的应用

David： 那你们在第二版中使用了 AI 吗？

Martin： 没有用在实际内容上，但 Chris 用它取得了一些不错的效果。

Chris： O'Reilly（我们的出版商）在 Safari 在线学习平台上提供每章课后测验题。他们需要我们为每章提供测验问题。我通过提示工程成功让 LLM 生成了所有测验题，效果出奇地好。 Martin 后来指出，其实这不该让人意外——大语言模型那种概率性的、带有“幻觉”的回答方式，恰好适合生成似是而非的错误选项。所以如果你去做 O'Reilly 的在线测验，你用的就是经过我们大量审查和调整的 LLM 生成的题目。 Martin 对我那个 PR 的修改意见有几百行之长，所以很难说 LLM 在哪里结束、Martin 和我在哪里开始。

另外有一个章节总结，我实在写不动了，就让 LLM 来写。它给了我一个初稿，然后我改写了不少——因为它总是到处用破折号，每段都用相同的开头。

但我觉得 AI 对我帮助最大的地方是：我写完一段东西后，会问它“我漏了什么？我的空白在哪里？有什么不正确的？” 它就像一个浏览器内置的小助手、检查员和编辑。我会参考它的建议，自己琢磨“我是不是确实漏了这个？该不该加上？”

AI、测试与创造性

David： 你的 O'Reilly 测验题案例完美地印证了我的一个更广泛的论点： AI 最擅长满足大型组织那些打勾式的形式化要求——那种“我一个字就能告诉你，但你非要让我填张表”的场景。这个例子特别好，因为多选题需要每道题有一个正确答案和三个错误答案，需要有人想出听起来合理但实际上不正确的说法。我个人觉得这很难做到，但 LLM 恰好非常擅长。

说到另一个话题——我们对用 LLM 测试软件显然很感兴趣。我们发现如今经过大量 RLHF 的模型，实际上已经很难生成真正疯狂、不可思议的东西了——即使你要求它这样做。高温度采样越来越难以产生有趣的结果。这让我有点沮丧，因为即便抛开软件测试不谈，我真正想用 AI 做的就是生成大量疯狂的想法，然后用它们来启发我的大脑。但现在经济激励和随机梯度下降的工作方式让它们在这方面表现不佳。

Chris： 有意思。我个人觉得 LLM 在单元测试领域最有帮助——正向用例、负向用例、快乐路径、这个能不能跑通。在这些方面它非常出色。但在设计方面——当我说“我有这个想法，告诉我权衡和替代方案”——它表现不太好。我觉得这是同一个根本原因：它只能做到跟互联网上讨论的平均水平一样有创造力，所以你总是得到那些显而易见的、别人都讨论过的东西。这确实令人失望。

David： 这里其实有一些比较深刻的东西。比如说强化学习训练一个代理下棋——你优化的目标是赢棋。但我真正想要的是优化出最多样、最有趣的棋局。那它的损失函数是什么？你不能简单地最大化策略的熵，因为随机下棋不会产生有趣的棋局，只会产生无聊的棋局。你真正想做的是最大化模型输出通过某个可能不可微的系统后的输出熵——我觉得没有人知道怎么做到这一点。而这恰恰是测试所需要的。

Chris： 我觉得可以看看 AlphaGo 的自我对弈——它并没有改变目标（目标还是赢围棋），但从训练在互联网语料库转向更多的自我博弈而非人类 RLHF，可能是一条发现人类想不到的创意的路径。 AlphaGo 那局棋的第 137 手震惊了所有人。但我也认同，我不知道怎么在代码领域做到这一点——代码的“赢围棋”等价物是什么？也许是某种基于测试的东西，但没人真正想清楚了。

什么是好的软件

David： 我觉得这里面有一个不可约减的部分——作为工程师成长的过程中，“它能跑了”和“测试通过了”只是通往“好”的起点。测试通过是可检验的、有明确二元答案的部分。但我们还追求很多其他东西——可理解性、对生产环境可靠性和可调试性的某种直觉、能被未来没有参与构建的工程师理解和接手的能力。这些都是模糊的、人类的东西，很难写出好的损失函数。

Chris： 你知道吗，我之前那本书里有一条建议是：你得在一个地方待够久，承受自己犯的错的后果。如果你每两年换一次工作，你永远学不到该学的教训——别人在替你学。

重新审视 CAP 定理

David： Martin，我记得第一次见你是在 2013 或 2014 年的 Strange Loop 大会上。你在前一晚的非正式会议上做了一个演讲，面对一屋子人，讲的是 CAP 定理为什么不是一个有用的分布式系统思考框架。当时房间里挤满了人，我认识的几个人都觉得这个演讲非常精彩。我觉得这个观点如今已经相当主流了，但在 2013 或 2014 年说这些简直就是异端邪说。所以我很好奇——为什么你能看到这一点，而那么多其他非常聪明的人却看不到？当时的社会条件到底是什么，让这个洞见那么难被人接受？

Martin： 这确实是一个非常好的问题。确实感觉有些异端。我记得我考虑过把它作为 Strange Loop 主会场的演讲提交，后来决定——算了，太有争议了，还是放在不录像的晚间活动上讲吧，那里大家都喝了点酒，更适合这种尖锐话题。但现在回过头看，我觉得这其实很明显。如果你读了那篇试图形式化 CAP 定理的实际论文，里面基本上什么实质内容都没有。

Chris： 我能问一下吗，你还记得有什么替代框架吗？我当时的职业阶段完全沉浸在 CAP 定理中，那是我们讨论一切的框架。我当时并不知道有什么替代方案来质疑这个范式。

David： 我觉得核心洞见是——Martin 和我们当时的老板、现在的联合创始人 Dave Sharer 都看到了—— Brewer 提出的 CAP 猜想是一个关于系统设计者可能关心的事物（一致性、可用性等）的合理猜想。但 MIT 的 Lynch 等人在形式化 CAP 定理时，把这些词重新定义成了任何系统设计者都不会在乎的含义。一旦术语以这种方式定义，这个定理就变得完全平凡了——“当然这是对的，但我从中没有学到任何有趣或新的东西”。然而，2010 年代初期构建分布式系统的每个人都认为这是有史以来最重要的发现。

Martin： 我觉得那些真正构建分布式数据库的人其实完全明白怎么回事，他们没什么误解。问题更多在于——那是 NoSQL 时代。 NoSQL 试图挑战关系数据库的教条，告诉人们其实你不一定什么都需要可串行化。很多人想构建“不一致”的数据库，所以他们需要一个理由来证明这是好事而不是坏事。我觉得这是一个营销问题。比如 Basho 做 Riak，他们需要说服人们这是合理的设计权衡，我的印象是很多 CAP 定理的鼓吹来自 Basho（他们做了很多优秀的工作，包括 CRDT 的早期工作）。营销压力迫使人们简化信息，CAP 定理恰好是一个好传播的营销信息，于是就被反复重复，很多没有仔细思考过的人也跟着传播，成了一种不假思索的“常识”。

Chris： 我在 Google Cloud Spanner 发布时就在 Google Cloud，稍微参与了一些。他们真的把 Eric Brewer 请来，说“写一篇博客说你的 CAP 猜想是错的，我们现在需要这个。”所以共识确实完全翻转了。

Kyle Kingsbury（Jepsen 项目的作者）一直在尝试把 CAP 中“可用性”的概念重新定义为“全面可用性”（Total Availability）。我觉得这是一个合理的重新表述，因为它清楚地展示了形式化定义中可用性概念的绝对主义有多荒谬。

Martin： 我跟 Kyle 讨论过用什么术语更好。我个人偏好“离线可用性”或“断连操作”。如果你想到运行在移动设备上的软件，这完全说得通——我手机上的日历应用，我希望无论有没有网络连接都能修改日历事件。这就是一个复制数据库，我想要 CAP 定理意义上的可用性——在与其他副本完全断开的情况下仍能修改数据库状态。所以在这个场景下它完美契合。至于在数据中心的副本之间，这就更有争议了。所以我更喜欢“离线可用性”这个术语，因为它聚焦于手持设备的使用场景。

David： 这很有道理。我整个职业生涯基本上都避开了客户端开发，所以这不是我第一时间会想到的使用场景。

Martin： 而这恰好是我离开工业界后一直在做的事——关于客户端协作软件。所有有趣的工作都在客户端进行，服务器只是通信管道。这是一种令人耳目一新的视角——这是小数据，不是大数据，我喜欢这样。

Chris： 说到 CAP 和 Spanner，2018 年有一篇 Eric Brewer 写的白皮书叫《Spanner, TrueTime, 和 CAP 定理》，里面有 Google 的实际可用性数据。 50%的可用性错误实际上是用户操作错误，只有 7%是网络错误。我当时看到就想：“我们是不是关注错了方向？”

David： 看到这种比例，你得记住——之所以 7%这么低，是因为已经有大量努力把网络错误降下去了。就像人们不再在婴儿期死亡了，所以每个人都死于心脏病——经过巨大的努力才达到“每个人都死于心脏病”的状态。 Google 的生产网络投入了数千年的人力来让它变得异常可靠。

教学方法与课程设计

David： 我们兜了一圈回到最开始——你写了这本书，在做第二版，你在教年轻的计算机科学学生关于分布式系统的知识。你的课程大致跟着书的大纲走吗？你怎么教学生思考这些权衡？你还讲 CAP 吗？会讲 Daniel Abadi 提出的那个替代框架吗？好像叫 PACELC？

Martin： 我教本科生的分布式系统课程实际上比书理论性强得多。我时不时考虑过要不要把它变成另一本书，但写一本书的创伤已经够了。课程讲义可以免费获取，YouTube 上也有录像。

这门课理论性更强是因为受众不同。剑桥计算机科学课程有大量理论基础。我们系的理念是：实际的软件工程技能人们会在工作中学到。我们的计算机科学课程不是行业岗位的职业培训，而是教人们计算机科学的真正基础。这意味着我可以使用数学符号而且知道学生能看懂。

我在课程中更深入地讲算法。我最喜欢的部分是带学生逐行过一遍 Raft 算法的完整伪代码实现——这基本上要用一整个小时甚至更长时间。我尽力让他们真正去思考所有奇怪的边界情况，然后以算法化的方式来思考它们。

我未来想在课程中加入模型检查，基本理念是：看看这些算法有多精妙——如果你不至少做模型检查，更不用说证明，你完全不知道它们到底对不对。

这门课非常聚焦于分布式系统本身，而书其实更偏数据库方向——分布式系统部分是为数据管理服务的，但它以数据库为主线。所以它们其实差别很大。此外，我还教一门实用密码学课程，那又是一个完全不同的话题了。

测试工具的选择：形式化方法 vs DST vs 属性测试

Chris： 我一直在想的一个问题是——你之前提到有些人认为 Antithesis 是反形式化方法的——但在我看来，形式化方法和确定性模拟测试（DST）以及各种实际验证工具是互补的。作为用户，我缺少的是最佳实践指南：我想确保我的软件端到端能正常工作，现在的建议就是“写系统测试、写单元测试、写集成测试”。但从设计阶段一直到部署，似乎没有一个完整的故事把形式化方法、DST 和属性测试串起来。你们有这样的指导原则吗？

David： 好吧，这可能不是公司官方声明。我有点愤世嫉俗。我觉得我们所有人试图做的事——写出正确工作的软件——太难了，我们需要一切能得到的帮助。如果你真的认真对待这件事，你可能会想办法使用所有这些工具，因为我们知道写完美正确的软件是可证明不可能的。

但说实话，挑战不在于让形式化方法的人采用 DST，或让 DST 的人采用形式化方法。挑战在于让 99.99999%的世界去测试他们的软件——因为大多数人根本不在意质量，或者他们在意但没有能力去实现它。所以当我得知一个潜在客户在使用形式化方法时，我内心会小小庆祝一下——一方面因为他们可能在为客户写好软件，另一方面因为他们更容易被说服采用 Antithesis，因为他们已经展示了对质量的某种程度的关心。

我们选择以测试为核心创业而不是形式化方法，也有一点点愤世嫉俗的成分。形式化方法对那些从第一天就决定要写出真正优秀软件的人来说非常好用。但我觉得绝大多数人不会这样做。他们没有时间做任何这些事，他们不在意，即使他们在意，他们的老板也不在意。所以尽管 Antithesis 今天可能还有些使用门槛，但我们长期的优化方向就是让它尽可能容易地在事后作为创可贴贴上去—— 当你发现自己已经陷入困境、不知道该怎么办、需要帮助的时候。

属性测试之所以比较容易被采纳，是因为它更容易解释，更容易让人觉得“这不过就是一种高级的单元测试”，更容易拿给你的老板看、说服他你在做正经事。

我觉得形式化方法和基于证明的技术在安全关键领域是绝对不可或缺的。在对抗性环境中，你不是要找到大部分 bug，你需要找到所有 bug——因为这完全是不对称的：如果对手发现一个 bug，你就完了。只有基于证明的技术才能给你这种置信度。但在非对抗性环境中，测试通常能给你更好的投入产出比。

Chris： 我想追问的就是：对于我这个实践者来说，什么时候该拿起 DST 工具？什么时候该拿起形式化方法工具？什么时候该用混沌测试？我觉得现在缺乏这方面的好指导。

David： 对我来说基本上就是——场景是对抗性的吗？如果是，你真的需要形式化方法。是否高度不对称？如果你的对手能投入比你多几千甚至几十万倍的算力，那更形式化的方法可能是正确选择。但我更想传达的是——我们四个人在这里讨论的这些关切，和市场上绝大多数人的关切相去甚远。绝大多数人根本不测试他们的软件。

Martin： 我觉得很多人就是在做基本的 CRUD 应用，他们的需求不复杂、不精妙。如果他们使用一个支持可串行化事务的数据库，大部分情况下就没什么问题。但是那些构建数据库系统的人，他们确实需要深入思考各种关键的边界情况。

David： 我得稍微反驳一下。我觉得即使是 CRUD 应用有时也会出奇地微妙。而且在纯 CRUD 应用和数据库之间有大量的中间地带——世界上有各种各样的系统，我们在测试它们方面做得都不好。看看所有的电脑游戏——为了让游戏在发布日不至于满是致命 bug，投入了多少心血和泪水，又损失了多少休假日？即使投入了那么多精力，结果还是很差。复杂软件制品因为世界的某些根本性原因而极其难以做对。

开发生命周期中测试工具的时机

David： Chris 提到了应该在什么时候使用这些不同工具的问题。很多正确性工具在开发生命周期的特定阶段最有效。我们花了很多时间讨论形式化方法在写规范时最有效——但问题是，那恰恰是你作为企业或个人最不愿意全力投入的时候，因为你还不确定有没有人会喜欢它、它能不能创造你想要的价值。有太多合理的压力要求尽快部署到生产环境、看看感觉怎样、是否真的解决了问题。甚至对业余项目来说——一旦它勉强能用了，我还会不会对这个项目感兴趣，还是已经失去了热情？

所以需要大量前期投入的东西，人们会理性地回避——除非他们非常确定这会是他们真心希望正确运行的关键软件。

Chris： 这正是我在 Slate DB 上的体验。早期就是赶紧把东西做出来。做完之后我跑了 DST，很兴奋地发现了三个 bug——结果我们已经知道这三个 bug 了，因为用户已经报告过。所以虽然工具能检测到是很好的，但如果能在用户使用之前就知道就更好了。不过话又说回来——当时没人在用它，那为什么要测试呢？这是一个先有鸡还是先有蛋的问题。

Martin 你做研究时，目标本身就是搞清楚怎么正确地做这些事，这是核心目标，跟采用率或 GitHub 星数无关。所以在很早期就大量投资于严格的正确性是合理的。

Martin： 是的，这是我作为研究者的奢侈。我不需要在意它是不是一个商业上可行的产品。如果我觉得某件事值得写论文，那就值得花时间去形式化它。但对于大多数构建实际系统的人来说，激励机制完全不同。不过工业界可能也有类似的项目——比如在 Google 内部如果你要重新架构 Spanner 并承接 V1 的所有流量，我假设你会花时间在切流量之前确保它是对的。

Chris： 那边有一个重写 Spanner 存储引擎的项目，那是一个非常长期的项目——因为在 Spanner 的规模下，极其罕见的事件每天都在发生。而且你已经知道这个系统会被使用——这是既定事实。所以你已经知道它会以各种“对抗性”方式被使用。

我从 DST 的业余尝试中学到的另一个教训是：我采用了端到端的方法——测试整个数据库的公共 API。但回过头来看，我觉得更好的做法是对子组件单独做 DST——比如只测压缩器，或只测对象持久化部分。在完整 DST 和完整设计证明之间的某个位置，分解成组件可能能更早地获得更多价值。但当时我不知道该怎么做，也没有找到太多指导，找到的大多是 TigerBeetle 那些很酷的博客文章。我觉得在帮助那些想做这些事的人更有效地去做方面，还有很多工作要做。

AI 作为测试预言机

David： 我能跟你们分享一个今天早上想到的疯狂想法吗？

属性测试和 DST 最令人头疼的事情之一就是：我的属性应该是什么？我的系统到底应该做什么？这正是 Ankush 在他的演讲中提到的——从形式化方法中获得的最大价值就是被迫去思考这个问题，但大多数人不想思考。

一种非常有用的属性——如果你在做大规模的重构或迁移——就是“新系统的行为和旧系统完全一样”。这是一个极其强大的测试预言机。

回到我们关于 AI 的讨论：我注意到，无论是我自己使用 AI 编程，还是和其他更认真使用它的人交流， AI 通常非常擅长一次性生成一个程序，但在对程序进行增量修改或处理大型复杂代码库时表现惊人地差。

所以我认为——我不确定我是否喜欢这个世界，但我觉得我们可能正在朝这个方向走——基本上所有软件都变成“只写”的：你让 AI 为你生成一个程序，当你想做改变时，你直接删掉它，让 AI 按照修改后的提示重新生成一个新程序。在这种世界中，DST 能够比较两个系统、验证它们是否行为一致的能力就变成了一种超级大的优势。

Martin： 这真的很有趣。用测试预言机来比较确实是一个非常有价值的原则。我们在形式化验证工作中就在使用它——比如在 Isabelle 中定义一个算法，然后从中提取可执行的 Haskell 代码。这段 Haskell 代码我不会放到生产中——它太慢了。但我们可以用它作为测试预言机，对照手写的 Rust 实现来验证。然后做一些属性测试来检查两者行为是否一致。

David： 那个 Rust 实现甚至不需要是手写的。我发现 LLM 在用新语言重写代码方面表现出色。你可以把 Haskell 给它，让它重写成 Rust，然后验证两者是否做同样的事情。

Chris： 对，我最近就做了这样的事——有一个不再维护的 Java 混沌测试代理工具，我就让 LLM 用 Rust 重写，效果好得惊人。所以这条从证明到 Haskell 再到 Rust、全程无需人工干预、但有一条可验证面包屑路径的方式真的很有趣。我之前没想到这个。

David： 有趣的是，到目前为止在属性测试领域，“在测试中写一个完整的替代实现”一直被视为反模式。但也许当我们把编写软件的成本大幅降低之后，这个权衡计算就会发生根本性的变化。

结语

David： 好的，这是一次精彩的讨论。这里是我们推荐你们的书的环节——《设计数据密集型应用》第二版预计二月底出版。

Chris： 我应该提一下，Safari 在线学习平台上已经有早期版本了，如果你有访问权限，可以去看看。

David： 好的，我现在就去排队拿一本。我记得我拿到过第一版的早期访问版，这次我想要第二版的纸质书。非常感谢你们两位，这次对话非常精彩。谢谢你们的参与。

Martin： 谢谢。

Chris： 很开心。拜拜。

老冯评论一、“本地磁盘让位于云原生对象存储”——对了一半

Martin 和 Chris 的判断在他们的语境下完全成立：如果你今天从零开始设计一个分析型数据库或日志系统，围绕 S3 来构建存储层确实是合理的默认选择。 TurboPuffer、WarpStream、ClickHouse Cloud 都在这么做，Neon 用对象存储做了 PostgreSQL 的存算分离，趋势是存在的，逻辑也说得通：对象存储把持久化、复制、容错这些脏活累活外包给了基础设施层，数据库开发者可以专注于上层逻辑，开发门槛确实大幅降低了。

但我有三个补充。

第一，这个趋势有明确的负载类型边界。本地 NVMe SSD 的延迟是微秒级，S3 是几十毫秒级，差三到四个数量级。对 OLAP 和日志型负载来说这不是问题，但对需要亚毫秒响应的 OLTP 场景，S3 就是不行，物理上不行。播客里举的所有例子基本都是分析型或日志型的，这不是巧合。 Neon 虽然基于对象存储，但本质上在热路径上还是靠本地缓存 —— 存储层的名字变了，物理现实没变。所以更准确的说法是：对象存储正在成为分析型数据库的默认持久层，以及 OLTP 数据库的补充架构选项——而不是“本地磁盘让位于对象存储”这种大一统叙事。

第二，运维成本和经济成本是两回事。Chris 说的“花钱让别人替我值班”是实话，但省的是运维人力，不是总成本。S3 的 API 调用费、跨区流量费加起来不便宜。 WarpStream 被 Confluent 收购前自己也承认过这一点。对于十几人的硅谷团队，用钱换运维省心是理性选择；但对于成本敏感的场景，这笔账未必算得过来。而这个叙事最大的受益者显然是云厂商——“一切都跑在 S3 上”翻译成大白话就是“一切都跑在 AWS 的账单上”。

第三，中国的基础设施现实不一样。对象存储作为备份和冷数据层算是标配，但要把它当成数据库的主存储层，从一致性语义到性能特征到定价模型，都还有差距。本土云的对象存储和 S3，本土和硅谷的人力成本差距都是重要的变量。加上大量企业仍在自建机房、信创要求用国产硬件，“把数据库建在对象存储上”在很多场景下前提条件并不充分。

总结：这是一个真实且重要的趋势，但它的适用范围比播客里呈现的要窄。 Martin 看到了架构层面的优雅，Chris 看到了运维层面的便利，但从全球视角、从不同负载类型和成本结构来看，这离“范式转移”还有距离。理解这个趋势背后的物理和经济现实，比追随叙事本身更重要。

二、CAP 定理——该批判，但别矫枉过正

Martin 对 CAP 定理的批判我基本认同。CAP 在数学上是正确的，但它被当成了工程设计框架来用——而它根本不配。 Lynch 的形式化把“可用性”定义成了“每一个非故障节点都必须响应每一个请求”——这是一个全称量词，现实中没有人的 SLA 是这样写的。你的 SLA 写的是 99.99% 的请求在 200ms 内响应，不是“所有请求都必须响应”。所以 CAP 定理告诉你的是：在一个极端化的数学模型里你不能同时拥有两个极端化的性质。对工程决策的指导意义极为有限。

David 说的“营销驱动”解释很到位：NoSQL 运动需要学术背书来证明“弱一致性是合理的”，CAP 就被当了遮羞布。 Martin 提出的“离线可用性”重新表述也很好——它把讨论从一个抽象定理拉回到具体的工程问题：你的应用断网时能不能继续工作？这才是有意义的设计问题。

这在中国尤其严重。国内的技术布道和面试八股文到今天还在让人背“CP 系统有哪些、AP 系统有哪些”。这种二分法让人以为分布式系统的设计空间就只有一条窄窄的光谱，而实际上那是一个高维的、连续的、充满权衡的复杂地形。正确的教法应该是先用 CAP 建立基本直觉，然后立刻解构它，引入更精细的模型——而不是把它当成终极真理背下来。

如果你想真正理解分布式系统在故障下的行为，我的建议是去看 Jepsen 的测试报告。 Kyle Kingsbury 对各种数据库的实际测试结果，比背一百遍“CAP 不可能三角”有用得多——不是因为理论不重要，而是因为理论必须落到实证上才有意义。

三、测试与形式化方法——残酷的现实

这段讨论里有趣的是 David 那句话：“正在挑战不在于让形式化方法的人采用 DST，或让 DST 的人采用形式化方法。挑战在于让 99.99% 的世界去测试他们的软件。”

播客里四个人在精细地讨论 Fizzbee、Isabelle、DST 的适用边界，这些讨论当然有价值——对于已经认真对待质量的团队来说，知道什么时候用形式化方法、什么时候用 DST、什么时候用属性测试，确实是一个重要的问题。但残酷的现实是，这些细糠离绝大多数开发者的世界太远了。我见过太多生产环境的 PostgreSQL 部署连基本的备份恢复都没测过，failover 演练都没做过，然后某天主库挂了才发现备库三个月前就停了。在这种现实面前，讨论 Isabelle 证明助手的使用体验多少有点奢侈。相比之下，真正的难题是如何让最广大群体的用户，在真实场景中验证你软件的正确性。

说实话，我觉得 PostgreSQL 和 Pigsty 在某种意义上都是这么做的：，这些问题可能官方自己都没测出来，但因为它的用户基数太大了，很快就被全球用户在实际使用中测了出来。 Pigsty 同理，它也有很多 bug 是用户在用了之后测出来直接反馈给我的。它的质量也是在这几年持续的实际生产使用反馈中通过不断修复来提升的。这比让你自己假想一些测试场景与用例要重要得多 —— 让真实世界来测试你的软件，本身就是一种核心能力。

Chris 说他对 Slate DB 做了 DST，找到了三个 bug，但全是用户已经报过的。他自己也反思说做得太晚了，应该更早地对子组件做 DST 而不是等系统完整后才做端到端测试。这恰好说明了一个实操层面的问题：这些高级测试工具的主要障碍不是技术难度，而是时机和动机 —— 在项目早期你不确定它能不能活下来，不想投入；等到它活下来了、用户在用了，你又忙着修 bug 加功能，有时候测试问题的速度，还不如用户替你众测来得快。这个鸡生蛋蛋生鸡的困境，大概是软件工程里最诚实也最无解的问题之一。

References

[1]: https://ddia.vonng.com
[2]: https://www.youtube.com/watch?v=UHdPnubbzBI