重新設(shè)計數(shù)據(jù)密集型應(yīng)用

《設(shè)計數(shù)據(jù)密集型應(yīng)用》（DDIA）第二版終于出了。

這本書不用我多介紹了——過去九年里，它是分布式系統(tǒng)領(lǐng)域當之無愧的圣經(jīng)，也是我翻譯過的最有價值的一本書。 第一版中文翻譯在 GitHub 上攢了兩萬多顆星，說明大家是真的需要這樣一本書。

第二版的變化不小。Martin 把整個存儲層的假設(shè)從本地磁盤換成了對象存儲，補上了這些年云原生架構(gòu)的演進，也更新了不少案例和觀點。 https://ddia.vonng.com —— 說實話，這次主力是 AI，我做的是校對和潤色。 但效果已經(jīng)足夠流暢通順，完全不影響閱讀。需要的朋友可以直接取用。

巧的是，就在昨天，Martin 和第二版的合著者 Chris Riccomini 一起上了 Antithesis 的 Bug Bash 播客，聊了差不多一個半小時。 話題很雜也很有意思：DDIA 第二版改了什么、為什么現(xiàn)在所有數(shù)據(jù)庫都在往 S3 上搬、CAP 定理為什么早該扔進垃圾桶、形式化驗證到底有沒有用， 以及 AI 寫代碼到底行不行。

我把視頻扒了下來，轉(zhuǎn)錄成文字稿，翻譯成了中文——這一整套流程全是 AI 干的，我基本沒怎么動手。 這大概也算是 AI 時代的內(nèi)容生產(chǎn)方式了：從語音轉(zhuǎn)文字到翻譯到排版，幾分鐘搞定一萬多字，質(zhì)量還說得過去。

最后，我也就播客里的幾個核心觀點聊了聊自己的看法——特別是關(guān)于對象存儲取代本地磁盤、 CAP 定理的歷史遺留問題、以及軟件測試的殘酷現(xiàn)實。不一定對，但保證說的是真話，供各位參考。

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

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

歡迎收聽 Bug Bash 播客，在這里我們聊一切與軟件正確性和可靠性相關(guān)的話題。我是主持人 David Win。 距離《設(shè)計數(shù)據(jù)密集型應(yīng)用》成為分布式系統(tǒng)標準教材已經(jīng)過去了 9 年。 今天，Martin Kleppmann 和 Chris Riccomini 來到節(jié)目中，為大家揭開即將出版的第二版的幕后故事。 畢竟，本地磁盤的時代正在讓位于云原生對象存儲，我們將探討為什么現(xiàn)代數(shù)據(jù)庫正在圍繞 S3 進行徹底重構(gòu)。 接下來，我們還會重新審視 CAP 定理，以及為什么也許是時候用“離線可用性”的概念來取代它了。 我們還會進入一場出人意料的實用性 AI 討論——探索大語言模型為什么在創(chuàng)造性設(shè)計方面可能表現(xiàn)糟糕， 但在驗證復(fù)雜系統(tǒng)遷移時卻是完美的測試預(yù)言機。 這期節(jié)目你一定不想錯過。

在開始今天的節(jié)目之前，快速說一句：如果你想在現(xiàn)實中結(jié)識同樣關(guān)心軟件正確性和可靠性的人，可以考慮參加 Bug Bash 大會， 時間是 4 月 23 日至 24 日，地點在華盛頓特區(qū)。 所有詳情請訪問 bugbash.antithesis.com。

一本經(jīng)典的誕生

David： 好的，歡迎大家收聽 Bug Bash 播客。 今天我們有一對非常令人激動的嘉賓——Martin 和 Chris， 他們是全世界（至少是我的世界里）每個人最喜歡的那本書——《設(shè)計數(shù)據(jù)密集型應(yīng)用》第二版的合著者。 也就是那本我希望自己剛開始寫分布式系統(tǒng)時就能擁有的書，但那時候沒有，所以我只能用最笨的方式把所有坑都踩了一遍。 歡迎 Martin，歡迎 Chris。

Martin： 謝謝。

Chris： 嗨，Will。很高興來到這里。

David： 我覺得我們可以聊的話題太多了， 但我首先想問的是——我知道剛才我有點在你們面前夸張了一下—— 但我覺得說《設(shè)計數(shù)據(jù)密集型應(yīng)用》已經(jīng)成為分布式系統(tǒng)實踐者的圣經(jīng)并不為過。 它就是那本書。 每當我看到有人在問怎么學習這個既棘手又復(fù)雜的學科時，它總是第一個被推薦的。 而且我認為這是有充分理由的，這本書寫得真的非常非常好，而且非常全面。我很好奇，這是你當初的意圖嗎？ 你是本來就打算把它寫得這么大部頭的，還是這一切是偶然發(fā)生的？如果是后者，你覺得原因是什么？

Martin： 關(guān)于第一版的問題我來說吧。確實沒有打算把它寫得這么大。最初的目標是 400 頁，后來變成了 600 頁。 我真的只是想寫一本我自己希望當初入門時就有的書。 我發(fā)現(xiàn)每次在網(wǎng)上查資料時，要么碰到的是那種充滿學術(shù)術(shù)語、極難理解的深度研究論文，要么就是試圖讓你買產(chǎn)品的空洞營銷軟文， 根本沒說清楚實質(zhì)內(nèi)容。 所以我想要找到這兩個極端之間的平衡。

David： 這本書的反響有什么讓你意外的嗎？你看起來是個非常低調(diào)的人，我猜你應(yīng)該沒預(yù)料到它會變得這么受歡迎。 有沒有哪些章節(jié)的反響比你預(yù)期的好或差？

Martin： 總體來說，我當時覺得分布式系統(tǒng)是一個非常小眾的領(lǐng)域——誰在乎分布式系統(tǒng)呢？這是很專業(yè)的東西。 我當時想，大多數(shù)只是使用數(shù)據(jù)庫的人根本不需要了解這么深入的細節(jié)，看看數(shù)據(jù)庫手冊就夠了。 我主要針對的是那些需要為特定應(yīng)用選擇數(shù)據(jù)庫系統(tǒng)的人，因為可選的實在太多了。 我當時覺得這會是一小群高級架構(gòu)師之類的人。完全沒想到它會變成一個如此主流的東西。

David： 我覺得這本書之所以如此成功，我個人也非常喜歡的一點是——它實際上不僅僅是一本關(guān)于分布式系統(tǒng)的書。 雖然它是以分布式系統(tǒng)為框架來寫的，但它實際上傳達了一些關(guān)于設(shè)計任何類型系統(tǒng)的深刻智慧，甚至不限于軟件系統(tǒng)。 它在某種程度上是一本通過分布式系統(tǒng)這個鏡頭來表達的通用工程智慧合集。 我覺得這正是你成功融合不同抽象層次的方式之一。我不知道還有什么別的書能做到這一點。

Martin： 是的，我真的很想讓它有實感，所以放了很多案例研究和與真實場景的關(guān)聯(lián)。 你知道，當你聽到那些有趣的故事，比如海底光纜因為鯊魚咬斷而中斷——你就覺得“這必須寫進去”。 當然，這些故事最終都被納入到我們試圖闡述的一般性原則中，所以它不僅僅是軼事集，而是真正在從這些案例中提煉和歸納。 但我覺得這些小花絮讓內(nèi)容更有真實感，讓讀者相信這確實是真實系統(tǒng)運作的方式，因為里面包含了這些來之不易的經(jīng)驗。 我花了很多時間翻閱各種生產(chǎn)事故的事后分析報告，看看能不能從中提取出有趣的教訓，融入到敘述中。

為什么需要第二版

David： 那你們?yōu)槭裁礇Q定需要出第二版？你們最期待第二版中的什么內(nèi)容？行業(yè)發(fā)生了哪些變化，書的內(nèi)容又有哪些變化？

Martin： 其實第二版的必要性已經(jīng)很明顯了，因為第一版正在變得過時。它已經(jīng) 9 年了。 而且最初幾章是在出版前幾年就開始寫的，所以那些章節(jié)大概已經(jīng)有 12 年了，這期間事情不可避免地會發(fā)生變化。 我當時確實盡量聚焦于一般性原則，而非某個特定軟件的最新版本，以便它能有一定的持久性。但盡管如此，事物還是在變化。

比如一個重大變化是：第一版基本上假設(shè)分布式系統(tǒng)中的一個節(jié)點就是一臺帶有本地磁盤的機器。 如果它要存儲數(shù)據(jù)，就寫入本地磁盤；如果要復(fù)制數(shù)據(jù)，就通過網(wǎng)絡(luò)發(fā)送給另一臺機器。 但現(xiàn)在我們有了云原生系統(tǒng)，你寫入的可能不是本地磁盤，而是對象存儲， 而對象存儲本身就是一個分布式系統(tǒng)——我們在服務(wù)之上層疊服務(wù)。 這是一個根本性的設(shè)計變化，深入到了人們構(gòu)建分布式系統(tǒng)和數(shù)據(jù)系統(tǒng)的基礎(chǔ)層面，我們必須在書中反映出來。

從本地磁盤到對象存儲

David： 你們覺得這個變化為什么會發(fā)生？這確實是一個巨大的范式轉(zhuǎn)變。 以前大家的假設(shè)是“顯然你會有一塊超快的 SSD，然后優(yōu)化你的存儲引擎來利用它”。 而現(xiàn)在大家覺得“顯然你會有超高吞吐量的分解式對象存儲，一切都依賴于它”。每個現(xiàn)代數(shù)據(jù)庫都在這樣構(gòu)建。 那你們覺得是什么關(guān)鍵因素促成了這個轉(zhuǎn)變？Chris，我覺得你在這個領(lǐng)域有特別的見解。

Chris： 是的，這主要來自我的個人經(jīng)驗。云系統(tǒng)對我來說最大的吸引力始終是——我可以付錢讓別人替我值班。本質(zhì)上這是一個 運維問題。 如果我可以花錢不用擔心復(fù)制、網(wǎng)絡(luò)分區(qū)、節(jié)點通信中斷、凌晨三點被叫醒、數(shù)據(jù)損壞這些事——這些東西真的一點都不好玩，純粹是痛苦。 無論是計算端還是持久化端都是如此。能把這些甩給第三方、有人負責真的很好。

但我確實覺得這在某種程度上是一種幻覺，因為現(xiàn)在你的云系統(tǒng)出了問題，你得去弄清楚——誰改了這個存儲桶的訪問控制？ 誰做了這個部署？為什么系統(tǒng)在降級？原來是有個“吵鬧的鄰居”之類的問題。 所以它并不是一個完美的解決方案。但我覺得大概 15 年前大家的想法是“這好太多了，我只需要調(diào)一個接口就行”。

David： 你覺得如果 S3 沒有添加強一致性支持，這個轉(zhuǎn)變還會以同樣的速度和方式發(fā)生嗎？

Chris： TurboPuffer 的創(chuàng)始人 Simon Eskildsen 有一個非常好的演講，詳細梳理了導(dǎo)致像 TurboPuffer 這樣的系統(tǒng)以這種方式構(gòu)建的關(guān)鍵時間線。 他指出的一個重點是，S3 實際上很晚才獲得強一致性支持——大概是 2020 年之后。 所以我覺得，是的，即便在 S3 獲得強一致性之前，這個轉(zhuǎn)變就已經(jīng)發(fā)生了。 當然，Google Cloud Storage 很早就有了強一致性。 在我看來，即使沒有 S3，只要有了按需獲取機器的能力、Kubernetes、EBS 這些基礎(chǔ)設(shè)施，轉(zhuǎn)變也會發(fā)生。

Martin： 我想補充一點，擁有強一致性以及能夠做原子的比較并交換（Compare-and-Swap）操作， 確實能讓構(gòu)建在對象存儲之上的分布式系統(tǒng)變得簡單得多。 因為你本質(zhì)上可以把共識外包給對象存儲。 以前人們需要使用 ZooKeeper 或 etcd 來把共識外包給另一個系統(tǒng)，而現(xiàn)在把它集成到對象存儲中是一個很大的簡化。

Chris： 沒錯，真的很棒。 我們前幾年開始做一個項目，基本上就是一個構(gòu)建在對象存儲之上的鍵值存儲，靈感來自 TurboPuffer 和 WarpStream 這些云原生數(shù)據(jù)庫。 最近我們發(fā)現(xiàn)，其實可以把它拆解成獨立的組件——一個自動做柵欄（fencing）的事務(wù)對象（因為有了 Compare-and-Swap， 在對象上做柵欄簡直是小事一樁）、 一個分布式隊列（TurboPuffer 最近也發(fā)了相關(guān)文章）、一個預(yù)寫日志（類似 WAL3 和 Chroma 的做法）。 Martin 說得完全正確：一旦 S3 和 GCS 有了前置條件機制，你基本上就能非常輕松地構(gòu)建所有這些原語，然后以各種很好的方式組合它們。

David： 是的， 我們 Antithesis 實際上構(gòu)建了自己的分析數(shù)據(jù)庫引擎—— 因為市面上沒有分析數(shù)據(jù)庫支持一種時間會分叉的數(shù)據(jù)模型（我還以為每個人都生活在這樣的世界里呢）。 但真正的關(guān)鍵技術(shù)認知是：你不再需要自己寫存儲引擎了。這一點極大地降低了做這類事情的門檻。

Chris： 百分之百同意。 現(xiàn)在你可以看到一個數(shù)據(jù)庫技術(shù)棧：底層是持久化層，往上一層是像 DataFusion 或 DuckDB 這樣的查詢引擎， 再加上 Parquet、Lance、Nimble 這些優(yōu)秀的文件格式。 你現(xiàn)在完全可以把這些組件疊加起來做一個分析數(shù)據(jù)庫，效果還相當出色。Polar Signals 最近也做了類似的事情。

合著者的故事

David： 能跟我們講講合著者的故事嗎？Martin 你說過這本書已經(jīng)存在大約十年了。Chris，當時你是在 WePay 嗎？

Chris： 其實當時我在 LinkedIn，就坐在 Martin 旁邊，直到他去休假。

Martin： Chris 當時在 LinkedIn 做 Samza 這個流處理器。我是通過之前創(chuàng)業(yè)公司被收購進入 LinkedIn 的。 后來我們團隊被解散了，我需要找新團隊。 我聽說 Kafka 團隊在做很有意思的事情，就聯(lián)系了 Jay，問他能不能加入。然后他把我介紹給了 Samza 團隊，我就開始和 Chris 一起工作了。

Chris： 對，大概是 2012 或 2013 年。那時候你剛開始寫書的前幾章。 我記得你去休假后，給我發(fā)了一封郵件，附件是一個包含前幾章的 PDF。我看到后就覺得“這太棒了”。那時候內(nèi)容還很厚重。 看著它逐漸成形、出版，并獲得如此好的反響，真的很酷。

Martin： LinkedIn 很慷慨地給了我 50%的時間來寫書，所以我一半時間做軟件工程師和 Chris 一起工作，另一半時間寫書。 后來我發(fā)現(xiàn)同時做這兩件事真的很難——我們當時在把 Samza 部署到生產(chǎn)環(huán)境，總有各種生產(chǎn)問題需要處理， 很難從那種狀態(tài)切換到一個多年寫作項目上來。 所以后來我干脆請了假，自掏腰包全職寫書。 然后不知不覺就滑入了學術(shù)界——在大學找到了一份可以做有趣研究的工作，同時完成了這本書。

到了寫第二版的時候，我一開始是自己寫的，但后來意識到我已經(jīng)落后于當前的行業(yè)實踐了。畢竟我已經(jīng)退縮到學術(shù)界的象牙塔里了。 雖然對 2014 年左右的技術(shù)還算了解，但完全錯過了之后發(fā)生的事情。 不過我一直在看 Chris 寫的博客和通訊，從中獲得了不少有用的洞見。后來突然靈光一閃——我應(yīng)該讓 Chris 作為合著者加入。 于是我給 Chris 發(fā)了封郵件說“你有興趣嗎？”他說“有”。

創(chuàng)業(yè)、大公司與學術(shù)界

David： 你們兩個都經(jīng)歷過創(chuàng)業(yè)，也都在大型企業(yè)里當過螺絲釘，Martin 你還待過學術(shù)界。 能不能給我們一些犀利的比較和對比，這些不同的生活方式和職業(yè)路徑各有什么特點？

Chris： 我最犀利的觀點是：公司規(guī)模其實沒那么重要。在 Google 工作和在 JP Morgan 工作，即使都是大公司，體驗也完全不同。 我發(fā)現(xiàn)自己越來越關(guān)注的是：這家公司是不是以技術(shù)和工程為驅(qū)動的？它的世界觀是否與我的兼容？ 我在 JP Morgan 最痛苦的時候就是文化上與他們根本不同——他們是銀行，技術(shù)對他們來說只是工具，這可以理解。 但技術(shù)對我來說是一種熱情。

我有一個之前在 WePay 的同事后來去了 ClickHouse，她跟我喝咖啡時說：“如果你真的對數(shù)據(jù)庫充滿熱情， 你就應(yīng)該去一家數(shù)據(jù)庫公司工作。” 這話聽起來簡單得令人震驚，但又出人意料地不顯而易見。 所以我的觀點是：不要太在意公司大小，要關(guān)注你的價值觀和世界觀是否與公司的領(lǐng)導(dǎo)層和方向兼容。

Martin： LinkedIn 是我待過的唯一一家大公司，所以我沒什么比較基準。我覺得他們做得不錯，但我不太適合大公司的風格。 我有很多自己想做的事情，更喜歡自由地探索和試錯，而不是遵循預(yù)設(shè)的 OKR 之類的框架。 創(chuàng)業(yè)適合我，因為你就是在瘋狂地嘗試各種事情。學術(shù)界也適合我，因為研究非常自由開放。 兩者的區(qū)別主要是時間尺度——在創(chuàng)業(yè)公司你要在幾周到幾個月內(nèi)交付；在學術(shù)界我可以用幾年甚至幾十年的尺度來思考問題。 我現(xiàn)在很珍視這種自由——可以做自己認為重要的事情，不需要它現(xiàn)在就具備商業(yè)可行性。 但我也盡量把創(chuàng)業(yè)思維帶入研究中，保持對“做出真正有用的東西”的關(guān)注——這一點在學術(shù)界有時會被遺忘。

CRDT、端到端加密與本地優(yōu)先協(xié)作

David： 我記得你剛進入學術(shù)界時，我們聊過，你說在研究用 CRDT 和類似的數(shù)據(jù)結(jié)構(gòu)來實現(xiàn)隱私保護的協(xié)作工具。 這個項目現(xiàn)在還在進行嗎？進展如何？學到了什么？

Martin： 基本上還在繼續(xù)。我開始做這個已經(jīng)大約 10 年了，這就是我說的“以十年為尺度”的含義。 有一些非常難的問題確實需要很長時間來解決。

David： 這家公司絕對不會因為你花了很長時間而批評你——我們已經(jīng)干了八年了。

Martin： 我最初的目標是做一個類似 Google Docs 但具有端到端加密、去中心化的東西，這樣我們就不需要那么依賴 Google 的服務(wù)器了。 然后我開始在 CRDT 上做大量工作來實現(xiàn)去中心化協(xié)作。但比如端到端加密這部分，直到最近才開始成型。 就在過去一年左右，我在 Ink & Switch 的合作者們構(gòu)建了一個叫 KeyHive 的庫， 它在我們的 Automerge CRDT 庫之上添加了端到端加密和基于密碼學身份系統(tǒng)的去中心化訪問控制。 這是一個漫長的過程，而且遠未完成——軟件還沒有正式發(fā)布，我們確實需要做一些形式化證明來驗證它的正確性。 要真正投入實踐可能還需要幾年時間。 但這基本上就是我這些年一直在持續(xù)推進的事情——一個小項目接一個小項目，逐步提高數(shù)據(jù)結(jié)構(gòu)的效率， 讓它們能做以前做不到的事情。

形式化證明與模型檢查

David： 你提到了形式化證明，這對我們來說總是很有趣的話題。 作為來自工業(yè)界的人，我注意到形式化證明在學術(shù)界占有重要地位， 但我很少看到它們被用在日常的工業(yè)軟件項目中——尤其是在項目已經(jīng)上線、正在被積極擴展、維護和性能優(yōu)化的階段。 即使以前做過證明，我也很少看到有人回去維護它。Chris，你們在 Slate DB 中使用了 FSB，對吧？

Chris： 是的，這是我們嘗試過的工具套件中的一部分。我們最初使用 Fizzbee（FSB）來定義清單管理協(xié)議。 讓我先解釋一下背景：Slate DB 就是我之前提到的構(gòu)建在對象存儲之上的鍵值存儲。 你可以把它想象成 RocksDB——一個單節(jié)點的鍵值存儲，可以進行 get、put、delete、scan 操作——但它把所有數(shù)據(jù)持久化在對象存儲上， 可以完全不依賴本地磁盤運行。 底層使用了一種叫日志結(jié)構(gòu)合并樹（LSM Tree）的存儲策略。 簡單來說就是：所有寫操作都追加到日志中，然后定期讀取日志進行“壓縮”——也就是去除重復(fù)的鍵，只保留最新版本。 這既是一個極大的簡化，也基本上就是事實。

David： 在這個場景下，F(xiàn)SB 是什么？你們怎么使用它？

Chris： Fizzbee 是一個形式化證明系統(tǒng)，也有一些基于模型的測試方面。 它的要點是：你用一種小型語言定義你認為系統(tǒng)應(yīng)該有的行為，定義預(yù)期結(jié)果， 然后它會遍歷所有不同的狀態(tài)組合來驗證你的不變量是否成立。 比如，如果我向 Slate DB 寫入一個鍵，然后調(diào)用 get 讀取這個鍵，無論發(fā)生什么，我都應(yīng)該 100%能拿到值。 底層 Slate DB 做了很多事情——寫預(yù)寫日志、壓縮數(shù)據(jù)等等。 FSB 會模擬那次寫入操作，運行代碼中所有可能的執(zhí)行路徑變體，然后在每個路徑上檢查：如果我在這個流程中的任何地方調(diào)用 get， 是否總能拿回值。

不過有一點很重要：FSB 和大多數(shù)這類系統(tǒng)（TLA+ 等）實際上并不直接關(guān)聯(lián)到你的代碼。你是在 FSB 的語言中定義你認為代碼會如何行為。 所以它非常適合測試設(shè)計，但要測試實際實現(xiàn)就更困難。 FSB 的作者 JP 最近添加了一些基于模型的測試功能，提供了 Rust、Python 等語言的鉤子，可以插入你的實際代碼。 但總體來說，設(shè)計和實現(xiàn)之間一直存在這道鴻溝。

這也回應(yīng)了你之前的問題——為什么系統(tǒng)上線后就很少看到有人用這些工具。 系統(tǒng)上線后，它在不斷變化，有很多其他測試方式，有用戶提交的 bug 報告，有新功能開發(fā)。這些工具就被擱置了，因為使用成本不低。 大多數(shù)這類語言本質(zhì)上非常數(shù)學化。 我們選擇 FSB 的一個原因是它使用 Starlark 語言——一種簡化版的 Python，對開發(fā)者來說比其他工具更容易上手。

Martin： 我來補充幾句。正如 Chris 所說，驗證規(guī)范和驗證實現(xiàn)是有區(qū)別的。 我也認為大部分價值其實來自驗證規(guī)范——用計算機作為工具來檢驗我們自己的思維， 看看當考慮到那些我們?nèi)祟惪赡軟]想到的奇怪邊界情況時，我們對系統(tǒng)行為的假設(shè)是否站得住腳。 一旦規(guī)范通過了驗證，我覺得大部分價值就已經(jīng)獲得了。

當然，翻譯成實現(xiàn)時可能會引入 bug，但為了形式化驗證實際實現(xiàn)所需的額外工作量，往往與收益不成比例。 對實現(xiàn)做一些基于屬性的測試（Property-based Testing）是很有價值的，那算是比較容易摘到的果子。 但如果你想真正使用證明助手來證明代碼的定理，那工作量就太大了。

我對大語言模型持謹慎樂觀態(tài)度——未來它們可能會擅長寫形式化證明，到時候我們就可以把這些工作外包給 AI 代理。 而且即使它產(chǎn)生幻覺也沒關(guān)系，因為證明檢查器只有在證明真正嚴謹?shù)那闆r下才會接受。 這似乎是 LLM 一個非常好的應(yīng)用場景。但我自己還沒真正嘗試過。

我用 Isabelle 證明助手做過一些形式化驗證工作。 Isabelle 不像模型檢查器那樣只能在有限狀態(tài)空間內(nèi)測試，它可以在無限狀態(tài)空間上進行推理， 真正證明某個屬性在所有可能情況下都成立。 但寫這些 Isabelle 證明的過程極其耗時。 不過，在我們試圖設(shè)計一個非常精妙的算法、不做證明就完全不知道它對不對的情況下，這是非常有價值的。

實際上，寫證明的過程本身才是幫助我們理解算法為何正確（或不正確）的關(guān)鍵。最后得到一個證明產(chǎn)物只是一個副產(chǎn)品。 寫證明不是因為我們想要最終那個證明，而是因為我們想在頭腦中獲得那種理解。 我越來越看重證明助手這一點。 雖然它極其耗時，但它極大地磨礪了我自己的思維——被迫一步步寫出那個“愚蠢的機器”愿意接受的證明。 因為在寫證明的過程中，我無數(shù)次碰到那種“這顯然是對的”的地方，花了半個小時試圖證明它，然后發(fā)現(xiàn)——不，有反例。 所以寫證明這個過程讓我在結(jié)構(gòu)化思考方面變得更好了，即使我不再用證明工具了。

David： 這對我來說非常有道理——對很多復(fù)雜的認知任務(wù)來說，有一種強迫自己逐步嚴謹思考的方式， 會讓你的思維變得更好、更鋒利。 但這就引出一個有趣的對比：如果 LLM 能替我們寫證明，但很多價值就在于寫的過程和那種掙扎， 那如果我能按個按鈕、去喝杯咖啡、回來就看到 Isabelle 證明擺在那里——我們還能獲得那些好處嗎？

Martin： 這是一個很好的問題。我不確定，可能得試試才知道。 目前寫證明時很多時間是花在非常令人沮喪的事情上——比如琢磨“到底該用什么歸納假設(shè)才能證明這個引理， 然后才能推導(dǎo)出那個引理”。 就是在一些很小的引理上反復(fù)磨——比如我只是想證明列表追加操作的結(jié)合律——“這明明很顯然，為什么這么難？” 如果 AI 能幫我去掉這些苦力活，讓我們專注于證明的高層步驟，我覺得這本身就是巨大的收益——既能降低挫敗感和時間成本， 又能讓更多人不用讀完博士、不用花幾年學習那些晦澀的證明策略就能寫這些證明。 所以我覺得自動化更多證明過程大概率是凈收益。

半形式化方法

David： 去年 Bug Bash 大會上有一位演講者叫 Ankush Desai，當時在 AWS，現(xiàn)在在 Snowflake，他是形式化方法語言 P 的開發(fā)者。 P 專門針對分布式系統(tǒng)推理做了優(yōu)化。他做了一個非常精彩的演講。 他說了一句話，可能比你的觀點更極端——他大意是說：“我從形式化方法中獲得的 90%的價值，是在運行模型檢查器之前就獲得了。” 關(guān)鍵價值在于，它強迫你坐下來真正思考你的系統(tǒng)到底在做什么——如果沒有這個過程，你很容易就跳過這一步。

我們在 Antithesis 內(nèi)部確實也用了一些形式化方法——這可能會讓一些人吃驚，因為他們以為我們是反形式化方法的。其實不是。 我們在所有安全關(guān)鍵的部分大量使用基于證明的技術(shù)。

我們做的一件事是吸取了 Ankush 的建議：我們有一種“半形式化證明”——不是機器可檢查的，但人類可檢查。 它有一些定義和術(shù)語無法被完全還原為純邏輯描述，但它仍然具有證明的整體語義結(jié)構(gòu)——引理、蘊含、量化等等。 這是一個很好的平衡：你可以進行形式化推理風格的思考，捕捉到你否則不會發(fā)現(xiàn)的錯誤， 但避免了那種與檢查器沒完沒了地爭論的痛苦。 而且它允許在某些術(shù)語無法以計算機滿意的方式定義的領(lǐng)域中使用。 我不知道這會不會流行起來，但我們一直管它叫“半形式化方法”。

Chris： 我聽說有人管它叫“Smart Casual”——從“formal”降一個檔次。

David： 有句話我很喜歡——有人說過“寫作是大自然展示你思維有多模糊的方式”。 然后 Leslie Lamport 在此基礎(chǔ)上說：“數(shù)學是大自然展示你的文字有多模糊的方式。” 再進一步，證明助手是大自然展示你的數(shù)學有多模糊的方式。

Chris： 這整個話題讓我覺得它和寫作本身有著平行關(guān)系。 你一旦試圖把什么東西寫成書、寫成博客、寫成設(shè)計文檔，你馬上就開始碰撞你實際的心智模型，發(fā)現(xiàn)其中的錯誤和空白。 所以這個對話完全可以推廣到任何以寫作為基礎(chǔ)的活動。

AI 在第二版寫作中的應(yīng)用

David： 那你們在第二版中使用了 AI 嗎？

Martin： 沒有用在實際內(nèi)容上，但 Chris 用它取得了一些不錯的效果。

Chris： O'Reilly（我們的出版商）在 Safari 在線學習平臺上提供每章課后測驗題。他們需要我們?yōu)槊空绿峁y驗問題。 我通過提示工程成功讓 LLM 生成了所有測驗題，效果出奇地好。 Martin 后來指出，其實這不該讓人意外——大語言模型那種概率性的、帶有“幻覺”的回答方式，恰好適合生成似是而非的錯誤選項。 所以如果你去做 O'Reilly 的在線測驗，你用的就是經(jīng)過我們大量審查和調(diào)整的 LLM 生成的題目。 Martin 對我那個 PR 的修改意見有幾百行之長，所以很難說 LLM 在哪里結(jié)束、Martin 和我在哪里開始。

另外有一個章節(jié)總結(jié)，我實在寫不動了，就讓 LLM 來寫。 它給了我一個初稿，然后我改寫了不少——因為它總是到處用破折號，每段都用相同的開頭。

但我覺得 AI 對我?guī)椭畲蟮牡胤绞牵何覍懲暌欢螙|西后，會問它“我漏了什么？我的空白在哪里？有什么不正確的？” 它就像一個瀏覽器內(nèi)置的小助手、檢查員和編輯。 我會參考它的建議，自己琢磨“我是不是確實漏了這個？該不該加上？”

AI、測試與創(chuàng)造性

David： 你的 O'Reilly 測驗題案例完美地印證了我的一個更廣泛的論點： AI 最擅長滿足大型組織那些打勾式的形式化要求——那種“我一個字就能告訴你，但你非要讓我填張表”的場景。 這個例子特別好，因為多選題需要每道題有一個正確答案和三個錯誤答案，需要有人想出聽起來合理但實際上不正確的說法。 我個人覺得這很難做到，但 LLM 恰好非常擅長。

說到另一個話題——我們對用 LLM 測試軟件顯然很感興趣。 我們發(fā)現(xiàn)如今經(jīng)過大量 RLHF 的模型，實際上已經(jīng)很難生成真正瘋狂、不可思議的東西了——即使你要求它這樣做。 高溫度采樣越來越難以產(chǎn)生有趣的結(jié)果。 這讓我有點沮喪，因為即便拋開軟件測試不談，我真正想用 AI 做的就是生成大量瘋狂的想法，然后用它們來啟發(fā)我的大腦。 但現(xiàn)在經(jīng)濟激勵和隨機梯度下降的工作方式讓它們在這方面表現(xiàn)不佳。

Chris： 有意思。我個人覺得 LLM 在單元測試領(lǐng)域最有幫助——正向用例、負向用例、快樂路徑、這個能不能跑通。 在這些方面它非常出色。 但在設(shè)計方面——當我說“我有這個想法，告訴我權(quán)衡和替代方案”——它表現(xiàn)不太好。 我覺得這是同一個根本原因：它只能做到跟互聯(lián)網(wǎng)上討論的平均水平一樣有創(chuàng)造力， 所以你總是得到那些顯而易見的、別人都討論過的東西。 這確實令人失望。

David： 這里其實有一些比較深刻的東西。比如說強化學習訓練一個代理下棋——你優(yōu)化的目標是贏棋。 但我真正想要的是優(yōu)化出最多樣、最有趣的棋局。那它的損失函數(shù)是什么？ 你不能簡單地最大化策略的熵，因為隨機下棋不會產(chǎn)生有趣的棋局，只會產(chǎn)生無聊的棋局。 你真正想做的是最大化模型輸出通過某個可能不可微的系統(tǒng)后的輸出熵——我覺得沒有人知道怎么做到這一點。 而這恰恰是測試所需要的。

Chris： 我覺得可以看看 AlphaGo 的自我對弈——它并沒有改變目標（目標還是贏圍棋）， 但從訓練在互聯(lián)網(wǎng)語料庫轉(zhuǎn)向更多的自我博弈而非人類 RLHF，可能是一條發(fā)現(xiàn)人類想不到的創(chuàng)意的路徑。 AlphaGo 那局棋的第 137 手震驚了所有人。但我也認同，我不知道怎么在代碼領(lǐng)域做到這一點——代碼的“贏圍棋”等價物是什么？ 也許是某種基于測試的東西，但沒人真正想清楚了。

什么是好的軟件

David： 我覺得這里面有一個不可約減的部分——作為工程師成長的過程中，“它能跑了”和“測試通過了”只是通往“好”的起點。 測試通過是可檢驗的、有明確二元答案的部分。 但我們還追求很多其他東西——可理解性、對生產(chǎn)環(huán)境可靠性和可調(diào)試性的某種直覺、 能被未來沒有參與構(gòu)建的工程師理解和接手的能力。 這些都是模糊的、人類的東西，很難寫出好的損失函數(shù)。

Chris： 你知道嗎，我之前那本書里有一條建議是：你得在一個地方待夠久，承受自己犯的錯的后果。 如果你每兩年換一次工作，你永遠學不到該學的教訓——別人在替你學。

重新審視 CAP 定理

David： Martin，我記得第一次見你是在 2013 或 2014 年的 Strange Loop 大會上。 你在前一晚的非正式會議上做了一個演講，面對一屋子人，講的是 CAP 定理為什么不是一個有用的分布式系統(tǒng)思考框架。 當時房間里擠滿了人，我認識的幾個人都覺得這個演講非常精彩。 我覺得這個觀點如今已經(jīng)相當主流了，但在 2013 或 2014 年說這些簡直就是異端邪說。 所以我很好奇——為什么你能看到這一點，而那么多其他非常聰明的人卻看不到？ 當時的社會條件到底是什么，讓這個洞見那么難被人接受？

Martin： 這確實是一個非常好的問題。確實感覺有些異端。 我記得我考慮過把它作為 Strange Loop 主會場的演講提交，后來決定——算了，太有爭議了，還是放在不錄像的晚間活動上講吧， 那里大家都喝了點酒，更適合這種尖銳話題。 但現(xiàn)在回過頭看，我覺得這其實很明顯。如果你讀了那篇試圖形式化 CAP 定理的實際論文，里面基本上什么實質(zhì)內(nèi)容都沒有。

Chris： 我能問一下嗎，你還記得有什么替代框架嗎？我當時的職業(yè)階段完全沉浸在 CAP 定理中，那是我們討論一切的框架。 我當時并不知道有什么替代方案來質(zhì)疑這個范式。

David： 我覺得核心洞見是——Martin 和我們當時的老板、 現(xiàn)在的聯(lián)合創(chuàng)始人 Dave Sharer 都看到了—— Brewer 提出的 CAP 猜想是一個關(guān)于系統(tǒng)設(shè)計者可能關(guān)心的事物（一致性、可用性等）的合理猜想。 但 MIT 的 Lynch 等人在形式化 CAP 定理時，把這些詞重新定義成了任何系統(tǒng)設(shè)計者都不會在乎的含義。 一旦術(shù)語以這種方式定義，這個定理就變得完全平凡了——“當然這是對的，但我從中沒有學到任何有趣或新的東西”。 然而，2010 年代初期構(gòu)建分布式系統(tǒng)的每個人都認為這是有史以來最重要的發(fā)現(xiàn)。

Martin： 我覺得那些真正構(gòu)建分布式數(shù)據(jù)庫的人其實完全明白怎么回事，他們沒什么誤解。問題更多在于——那是 NoSQL 時代。 NoSQL 試圖挑戰(zhàn)關(guān)系數(shù)據(jù)庫的教條，告訴人們其實你不一定什么都需要可串行化。 很多人想構(gòu)建“不一致”的數(shù)據(jù)庫，所以他們需要一個理由來證明這是好事而不是壞事。我覺得這是一個營銷問題。 比如 Basho 做 Riak，他們需要說服人們這是合理的設(shè)計權(quán)衡，我的印象是很多 CAP 定理的鼓吹來自 Basho（他們做了很多優(yōu)秀的工作， 包括 CRDT 的早期工作）。 營銷壓力迫使人們簡化信息，CAP 定理恰好是一個好傳播的營銷信息，于是就被反復(fù)重復(fù)，很多沒有仔細思考過的人也跟著傳播， 成了一種不假思索的“常識”。

Chris： 我在 Google Cloud Spanner 發(fā)布時就在 Google Cloud，稍微參與了一些。 他們真的把 Eric Brewer 請來，說“寫一篇博客說你的 CAP 猜想是錯的，我們現(xiàn)在需要這個。”所以共識確實完全翻轉(zhuǎn)了。

Kyle Kingsbury（Jepsen 項目的作者）一直在嘗試把 CAP 中“可用性”的概念重新定義為“全面可用性”（Total Availability）。 我覺得這是一個合理的重新表述，因為它清楚地展示了形式化定義中可用性概念的絕對主義有多荒謬。

Martin： 我跟 Kyle 討論過用什么術(shù)語更好。我個人偏好“離線可用性”或“斷連操作”。 如果你想到運行在移動設(shè)備上的軟件，這完全說得通——我手機上的日歷應(yīng)用，我希望無論有沒有網(wǎng)絡(luò)連接都能修改日歷事件。 這就是一個復(fù)制數(shù)據(jù)庫，我想要 CAP 定理意義上的可用性——在與其他副本完全斷開的情況下仍能修改數(shù)據(jù)庫狀態(tài)。 所以在這個場景下它完美契合。至于在數(shù)據(jù)中心的副本之間，這就更有爭議了。 所以我更喜歡“離線可用性”這個術(shù)語，因為它聚焦于手持設(shè)備的使用場景。

David： 這很有道理。我整個職業(yè)生涯基本上都避開了客戶端開發(fā)，所以這不是我第一時間會想到的使用場景。

Martin： 而這恰好是我離開工業(yè)界后一直在做的事——關(guān)于客戶端協(xié)作軟件。所有有趣的工作都在客戶端進行，服務(wù)器只是通信管道。 這是一種令人耳目一新的視角——這是小數(shù)據(jù)，不是大數(shù)據(jù)，我喜歡這樣。

Chris： 說到 CAP 和 Spanner，2018 年有一篇 Eric Brewer 寫的白皮書叫《Spanner, TrueTime, 和 CAP 定理》， 里面有 Google 的實際可用性數(shù)據(jù)。 50%的可用性錯誤實際上是用戶操作錯誤，只有 7%是網(wǎng)絡(luò)錯誤。我當時看到就想：“我們是不是關(guān)注錯了方向？”

David： 看到這種比例，你得記住——之所以 7%這么低，是因為已經(jīng)有大量努力把網(wǎng)絡(luò)錯誤降下去了。 就像人們不再在嬰兒期死亡了，所以每個人都死于心臟病——經(jīng)過巨大的努力才達到“每個人都死于心臟病”的狀態(tài)。 Google 的生產(chǎn)網(wǎng)絡(luò)投入了數(shù)千年的人力來讓它變得異常可靠。

教學方法與課程設(shè)計

David： 我們兜了一圈回到最開始——你寫了這本書，在做第二版，你在教年輕的計算機科學學生關(guān)于分布式系統(tǒng)的知識。 你的課程大致跟著書的大綱走嗎？你怎么教學生思考這些權(quán)衡？你還講 CAP 嗎？ 會講 Daniel Abadi 提出的那個替代框架嗎？好像叫 PACELC？

Martin： 我教本科生的分布式系統(tǒng)課程實際上比書理論性強得多。 我時不時考慮過要不要把它變成另一本書，但寫一本書的創(chuàng)傷已經(jīng)夠了。課程講義可以免費獲取，YouTube 上也有錄像。

這門課理論性更強是因為受眾不同。劍橋計算機科學課程有大量理論基礎(chǔ)。我們系的理念是：實際的軟件工程技能人們會在工作中學到。 我們的計算機科學課程不是行業(yè)崗位的職業(yè)培訓，而是教人們計算機科學的真正基礎(chǔ)。 這意味著我可以使用數(shù)學符號而且知道學生能看懂。

我在課程中更深入地講算法。 我最喜歡的部分是帶學生逐行過一遍 Raft 算法的完整偽代碼實現(xiàn)——這基本上要用一整個小時甚至更長時間。 我盡力讓他們真正去思考所有奇怪的邊界情況，然后以算法化的方式來思考它們。

我未來想在課程中加入模型檢查，基本理念是：看看這些算法有多精妙——如果你不至少做模型檢查，更不用說證明， 你完全不知道它們到底對不對。

這門課非常聚焦于分布式系統(tǒng)本身，而書其實更偏數(shù)據(jù)庫方向——分布式系統(tǒng)部分是為數(shù)據(jù)管理服務(wù)的，但它以數(shù)據(jù)庫為主線。 所以它們其實差別很大。此外，我還教一門實用密碼學課程，那又是一個完全不同的話題了。

測試工具的選擇：形式化方法 vs DST vs 屬性測試

Chris： 我一直在想的一個問題是——你之前提到有些人認為 Antithesis 是反形式化方法的——但在我看來， 形式化方法和確定性模擬測試（DST）以及各種實際驗證工具是互補的。 作為用戶，我缺少的是最佳實踐指南：我想確保我的軟件端到端能正常工作， 現(xiàn)在的建議就是“寫系統(tǒng)測試、寫單元測試、寫集成測試”。 但從設(shè)計階段一直到部署，似乎沒有一個完整的故事把形式化方法、DST 和屬性測試串起來。你們有這樣的指導(dǎo)原則嗎？

David： 好吧，這可能不是公司官方聲明。我有點憤世嫉俗。 我覺得我們所有人試圖做的事——寫出正確工作的軟件——太難了，我們需要一切能得到的幫助。 如果你真的認真對待這件事，你可能會想辦法使用所有這些工具，因為我們知道寫完美正確的軟件是可證明不可能的。

但說實話，挑戰(zhàn)不在于讓形式化方法的人采用 DST，或讓 DST 的人采用形式化方法。 挑戰(zhàn)在于讓 99.99999%的世界去測試他們的軟件——因為大多數(shù)人根本不在意質(zhì)量，或者他們在意但沒有能力去實現(xiàn)它。 所以當我得知一個潛在客戶在使用形式化方法時，我內(nèi)心會小小慶祝一下——一方面因為他們可能在為客戶寫好軟件， 另一方面因為他們更容易被說服采用 Antithesis，因為他們已經(jīng)展示了對質(zhì)量的某種程度的關(guān)心。

我們選擇以測試為核心創(chuàng)業(yè)而不是形式化方法，也有一點點憤世嫉俗的成分。 形式化方法對那些從第一天就決定要寫出真正優(yōu)秀軟件的人來說非常好用。但我覺得絕大多數(shù)人不會這樣做。 他們沒有時間做任何這些事，他們不在意，即使他們在意，他們的老板也不在意。 所以盡管 Antithesis 今天可能還有些使用門檻， 但我們長期的優(yōu)化方向就是讓它盡可能容易地在事后作為創(chuàng)可貼貼上去—— 當你發(fā)現(xiàn)自己已經(jīng)陷入困境、不知道該怎么辦、需要幫助的時候。

屬性測試之所以比較容易被采納，是因為它更容易解釋，更容易讓人覺得“這不過就是一種高級的單元測試”， 更容易拿給你的老板看、說服他你在做正經(jīng)事。

我覺得形式化方法和基于證明的技術(shù)在安全關(guān)鍵領(lǐng)域是絕對不可或缺的。 在對抗性環(huán)境中，你不是要找到大部分 bug，你需要找到所有 bug——因為這完全是不對稱的：如果對手發(fā)現(xiàn)一個 bug，你就完了。 只有基于證明的技術(shù)才能給你這種置信度。但在非對抗性環(huán)境中，測試通常能給你更好的投入產(chǎn)出比。

Chris： 我想追問的就是：對于我這個實踐者來說，什么時候該拿起 DST 工具？什么時候該拿起形式化方法工具？ 什么時候該用混沌測試？我覺得現(xiàn)在缺乏這方面的好指導(dǎo)。

David： 對我來說基本上就是——場景是對抗性的嗎？如果是，你真的需要形式化方法。是否高度不對稱？ 如果你的對手能投入比你多幾千甚至幾十萬倍的算力，那更形式化的方法可能是正確選擇。 但我更想傳達的是——我們四個人在這里討論的這些關(guān)切，和市場上絕大多數(shù)人的關(guān)切相去甚遠。絕大多數(shù)人根本不測試他們的軟件。

Martin： 我覺得很多人就是在做基本的 CRUD 應(yīng)用，他們的需求不復(fù)雜、不精妙。 如果他們使用一個支持可串行化事務(wù)的數(shù)據(jù)庫，大部分情況下就沒什么問題。 但是那些構(gòu)建數(shù)據(jù)庫系統(tǒng)的人，他們確實需要深入思考各種關(guān)鍵的邊界情況。

David： 我得稍微反駁一下。我覺得即使是 CRUD 應(yīng)用有時也會出奇地微妙。 而且在純 CRUD 應(yīng)用和數(shù)據(jù)庫之間有大量的中間地帶——世界上有各種各樣的系統(tǒng)，我們在測試它們方面做得都不好。 看看所有的電腦游戲——為了讓游戲在發(fā)布日不至于滿是致命 bug，投入了多少心血和淚水，又損失了多少休假日？ 即使投入了那么多精力，結(jié)果還是很差。復(fù)雜軟件制品因為世界的某些根本性原因而極其難以做對。

開發(fā)生命周期中測試工具的時機

David： Chris 提到了應(yīng)該在什么時候使用這些不同工具的問題。很多正確性工具在開發(fā)生命周期的特定階段最有效。 我們花了很多時間討論形式化方法在寫規(guī)范時最有效——但問題是，那恰恰是你作為企業(yè)或個人最不愿意全力投入的時候， 因為你還不確定有沒有人會喜歡它、它能不能創(chuàng)造你想要的價值。 有太多合理的壓力要求盡快部署到生產(chǎn)環(huán)境、看看感覺怎樣、是否真的解決了問題。 甚至對業(yè)余項目來說——一旦它勉強能用了，我還會不會對這個項目感興趣，還是已經(jīng)失去了熱情？

所以需要大量前期投入的東西，人們會理性地回避——除非他們非常確定這會是他們真心希望正確運行的關(guān)鍵軟件。

Chris： 這正是我在 Slate DB 上的體驗。早期就是趕緊把東西做出來。 做完之后我跑了 DST，很興奮地發(fā)現(xiàn)了三個 bug——結(jié)果我們已經(jīng)知道這三個 bug 了，因為用戶已經(jīng)報告過。 所以雖然工具能檢測到是很好的，但如果能在用戶使用之前就知道就更好了。不過話又說回來——當時沒人在用它，那為什么要測試呢？ 這是一個先有雞還是先有蛋的問題。

Martin 你做研究時，目標本身就是搞清楚怎么正確地做這些事，這是核心目標，跟采用率或 GitHub 星數(shù)無關(guān)。 所以在很早期就大量投資于嚴格的正確性是合理的。

Martin： 是的，這是我作為研究者的奢侈。我不需要在意它是不是一個商業(yè)上可行的產(chǎn)品。 如果我覺得某件事值得寫論文，那就值得花時間去形式化它。 但對于大多數(shù)構(gòu)建實際系統(tǒng)的人來說，激勵機制完全不同。 不過工業(yè)界可能也有類似的項目——比如在 Google 內(nèi)部如果你要重新架構(gòu) Spanner 并承接 V1 的所有流量， 我假設(shè)你會花時間在切流量之前確保它是對的。

Chris： 那邊有一個重寫 Spanner 存儲引擎的項目，那是一個非常長期的項目——因為在 Spanner 的規(guī)模下， 極其罕見的事件每天都在發(fā)生。 而且你已經(jīng)知道這個系統(tǒng)會被使用——這是既定事實。所以你已經(jīng)知道它會以各種“對抗性”方式被使用。

我從 DST 的業(yè)余嘗試中學到的另一個教訓是：我采用了端到端的方法——測試整個數(shù)據(jù)庫的公共 API。 但回過頭來看，我覺得更好的做法是對子組件單獨做 DST——比如只測壓縮器，或只測對象持久化部分。 在完整 DST 和完整設(shè)計證明之間的某個位置，分解成組件可能能更早地獲得更多價值。 但當時我不知道該怎么做，也沒有找到太多指導(dǎo)，找到的大多是 TigerBeetle 那些很酷的博客文章。 我覺得在幫助那些想做這些事的人更有效地去做方面，還有很多工作要做。

AI 作為測試預(yù)言機

David： 我能跟你們分享一個今天早上想到的瘋狂想法嗎？

屬性測試和 DST 最令人頭疼的事情之一就是：我的屬性應(yīng)該是什么？我的系統(tǒng)到底應(yīng)該做什么？ 這正是 Ankush 在他的演講中提到的——從形式化方法中獲得的最大價值就是被迫去思考這個問題，但大多數(shù)人不想思考。

一種非常有用的屬性——如果你在做大規(guī)模的重構(gòu)或遷移——就是“新系統(tǒng)的行為和舊系統(tǒng)完全一樣”。 這是一個極其強大的測試預(yù)言機。

回到我們關(guān)于 AI 的討論：我注意到，無論是我自己使用 AI 編程，還是和其他更認真使用它的人交流， AI 通常非常擅長一次性生成一個程序，但在對程序進行增量修改或處理大型復(fù)雜代碼庫時表現(xiàn)驚人地差。

所以我認為——我不確定我是否喜歡這個世界，但我覺得我們可能正在朝這個方向走——基本上所有軟件都變成“只寫”的： 你讓 AI 為你生成一個程序，當你想做改變時，你直接刪掉它，讓 AI 按照修改后的提示重新生成一個新程序。 在這種世界中，DST 能夠比較兩個系統(tǒng)、驗證它們是否行為一致的能力就變成了一種超級大的優(yōu)勢。

Martin： 這真的很有趣。用測試預(yù)言機來比較確實是一個非常有價值的原則。 我們在形式化驗證工作中就在使用它——比如在 Isabelle 中定義一個算法，然后從中提取可執(zhí)行的 Haskell 代碼。 這段 Haskell 代碼我不會放到生產(chǎn)中——它太慢了。 但我們可以用它作為測試預(yù)言機，對照手寫的 Rust 實現(xiàn)來驗證。然后做一些屬性測試來檢查兩者行為是否一致。

David： 那個 Rust 實現(xiàn)甚至不需要是手寫的。我發(fā)現(xiàn) LLM 在用新語言重寫代碼方面表現(xiàn)出色。 你可以把 Haskell 給它，讓它重寫成 Rust，然后驗證兩者是否做同樣的事情。

Chris： 對，我最近就做了這樣的事——有一個不再維護的 Java 混沌測試代理工具，我就讓 LLM 用 Rust 重寫，效果好得驚人。 所以這條從證明到 Haskell 再到 Rust、全程無需人工干預(yù)、但有一條可驗證面包屑路徑的方式真的很有趣。我之前沒想到這個。

David： 有趣的是，到目前為止在屬性測試領(lǐng)域，“在測試中寫一個完整的替代實現(xiàn)”一直被視為反模式。 但也許當我們把編寫軟件的成本大幅降低之后，這個權(quán)衡計算就會發(fā)生根本性的變化。

結(jié)語

David： 好的，這是一次精彩的討論。這里是我們推薦你們的書的環(huán)節(jié)——《設(shè)計數(shù)據(jù)密集型應(yīng)用》第二版預(yù)計二月底出版。

Chris： 我應(yīng)該提一下，Safari 在線學習平臺上已經(jīng)有早期版本了，如果你有訪問權(quán)限，可以去看看。

David： 好的，我現(xiàn)在就去排隊拿一本。我記得我拿到過第一版的早期訪問版，這次我想要第二版的紙質(zhì)書。 非常感謝你們兩位，這次對話非常精彩。謝謝你們的參與。

Martin： 謝謝。

Chris： 很開心。拜拜。

老馮評論 一、“本地磁盤讓位于云原生對象存儲”——對了一半

Martin 和 Chris 的判斷在他們的語境下完全成立：如果你今天從零開始設(shè)計一個分析型數(shù)據(jù)庫或日志系統(tǒng)，圍繞 S3 來構(gòu)建存儲層確實是合理的默認選擇。 TurboPuffer、WarpStream、ClickHouse Cloud 都在這么做，Neon 用對象存儲做了 PostgreSQL 的存算分離， 趨勢是存在的，邏輯也說得通：對象存儲把持久化、復(fù)制、容錯這些臟活累活外包給了基礎(chǔ)設(shè)施層，數(shù)據(jù)庫開發(fā)者可以專注于上層邏輯，開發(fā)門檻確實大幅降低了。

但我有三個補充。

第一，這個趨勢有明確的負載類型邊界。本地 NVMe SSD 的延遲是微秒級，S3 是幾十毫秒級，差三到四個數(shù)量級。 對 OLAP 和日志型負載來說這不是問題，但對需要亞毫秒響應(yīng)的 OLTP 場景，S3 就是不行，物理上不行。播客里舉的所有例子基本都是分析型或日志型的，這不是巧合。 Neon 雖然基于對象存儲，但本質(zhì)上在熱路徑上還是靠本地緩存 —— 存儲層的名字變了，物理現(xiàn)實沒變。 所以更準確的說法是：對象存儲正在成為分析型數(shù)據(jù)庫的默認持久層，以及 OLTP 數(shù)據(jù)庫的補充架構(gòu)選項——而不是“本地磁盤讓位于對象存儲”這種大一統(tǒng)敘事。

第二，運維成本和經(jīng)濟成本是兩回事。Chris 說的“花錢讓別人替我值班”是實話，但省的是運維人力，不是總成本。S3 的 API 調(diào)用費、跨區(qū)流量費加起來不便宜。 WarpStream 被 Confluent 收購前自己也承認過這一點。對于十幾人的硅谷團隊，用錢換運維省心是理性選擇；但對于成本敏感的場景，這筆賬未必算得過來。 而這個敘事最大的受益者顯然是云廠商——“一切都跑在 S3 上”翻譯成大白話就是“一切都跑在 AWS 的賬單上”。

第三，中國的基礎(chǔ)設(shè)施現(xiàn)實不一樣。 對象存儲作為備份和冷數(shù)據(jù)層算是標配，但要把它當成數(shù)據(jù)庫的主存儲層，從一致性語義到性能特征到定價模型，都還有差距。 本土云的對象存儲和 S3，本土和硅谷的人力成本差距都是重要的變量。加上大量企業(yè)仍在自建機房、信創(chuàng)要求用國產(chǎn)硬件，“把數(shù)據(jù)庫建在對象存儲上”在很多場景下前提條件并不充分。

總結(jié)：這是一個真實且重要的趨勢，但它的適用范圍比播客里呈現(xiàn)的要窄。 Martin 看到了架構(gòu)層面的優(yōu)雅，Chris 看到了運維層面的便利，但從全球視角、從不同負載類型和成本結(jié)構(gòu)來看，這離“范式轉(zhuǎn)移”還有距離。理解這個趨勢背后的物理和經(jīng)濟現(xiàn)實，比追隨敘事本身更重要。

二、CAP 定理——該批判，但別矯枉過正

Martin 對 CAP 定理的批判我基本認同。CAP 在數(shù)學上是正確的，但它被當成了工程設(shè)計框架來用——而它根本不配。 Lynch 的形式化把“可用性”定義成了“每一個非故障節(jié)點都必須響應(yīng)每一個請求”——這是一個全稱量詞，現(xiàn)實中沒有人的 SLA 是這樣寫的。 你的 SLA 寫的是 99.99% 的請求在 200ms 內(nèi)響應(yīng)，不是“所有請求都必須響應(yīng)”。所以 CAP 定理告訴你的是：在一個極端化的數(shù)學模型里你不能同時擁有兩個極端化的性質(zhì)。 對工程決策的指導(dǎo)意義極為有限。

David 說的“營銷驅(qū)動”解釋很到位：NoSQL 運動需要學術(shù)背書來證明“弱一致性是合理的”，CAP 就被當了遮羞布。 Martin 提出的“離線可用性”重新表述也很好——它把討論從一個抽象定理拉回到具體的工程問題：你的應(yīng)用斷網(wǎng)時能不能繼續(xù)工作？這才是有意義的設(shè)計問題。

這在中國尤其嚴重。國內(nèi)的技術(shù)布道和面試八股文到今天還在讓人背“CP 系統(tǒng)有哪些、AP 系統(tǒng)有哪些”。 這種二分法讓人以為分布式系統(tǒng)的設(shè)計空間就只有一條窄窄的光譜，而實際上那是一個高維的、連續(xù)的、充滿權(quán)衡的復(fù)雜地形。 正確的教法應(yīng)該是先用 CAP 建立基本直覺，然后立刻解構(gòu)它，引入更精細的模型——而不是把它當成終極真理背下來。

如果你想真正理解分布式系統(tǒng)在故障下的行為，我的建議是去看 Jepsen 的測試報告。 Kyle Kingsbury 對各種數(shù)據(jù)庫的實際測試結(jié)果，比背一百遍“CAP 不可能三角”有用得多——不是因為理論不重要，而是因為理論必須落到實證上才有意義。

三、測試與形式化方法——殘酷的現(xiàn)實

這段討論里有趣的是 David 那句話：“正在挑戰(zhàn)不在于讓形式化方法的人采用 DST，或讓 DST 的人采用形式化方法。挑戰(zhàn)在于讓 99.99% 的世界去測試他們的軟件。”

播客里四個人在精細地討論 Fizzbee、Isabelle、DST 的適用邊界，這些討論當然有價值——對于已經(jīng)認真對待質(zhì)量的團隊來說，知道什么時候用形式化方法、什么時候用 DST、什么時候用屬性測試，確實是一個重要的問題。 但殘酷的現(xiàn)實是，這些細糠離絕大多數(shù)開發(fā)者的世界太遠了。我見過太多生產(chǎn)環(huán)境的 PostgreSQL 部署連基本的備份恢復(fù)都沒測過，failover 演練都沒做過，然后某天主庫掛了才發(fā)現(xiàn)備庫三個月前就停了。 在這種現(xiàn)實面前，討論 Isabelle 證明助手的使用體驗多少有點奢侈。相比之下，真正的難題是如何讓最廣大群體的用戶，在真實場景中驗證你軟件的正確性。

說實話，我覺得 PostgreSQL 和 Pigsty 在某種意義上都是這么做的：，這些問題可能官方自己都沒測出來，但因為它的用戶基數(shù)太大了，很快就被全球用戶在實際使用中測了出來。 Pigsty 同理，它也有很多 bug 是用戶在用了之后測出來直接反饋給我的。它的質(zhì)量也是在這幾年持續(xù)的實際生產(chǎn)使用反饋中通過不斷修復(fù)來提升的。這比讓你自己假想一些測試場景與用例要重要得多 —— 讓真實世界來測試你的軟件，本身就是一種核心能力。

Chris 說他對 Slate DB 做了 DST，找到了三個 bug，但全是用戶已經(jīng)報過的。他自己也反思說做得太晚了，應(yīng)該更早地對子組件做 DST 而不是等系統(tǒng)完整后才做端到端測試。 這恰好說明了一個實操層面的問題：這些高級測試工具的主要障礙不是技術(shù)難度，而是時機和動機 —— 在項目早期你不確定它能不能活下來，不想投入； 等到它活下來了、用戶在用了，你又忙著修 bug 加功能，有時候測試問題的速度，還不如用戶替你眾測來得快。 這個雞生蛋蛋生雞的困境，大概是軟件工程里最誠實也最無解的問題之一。

References

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