工程哲學：Leslie Lamport，先思考再寫程式

重點摘要

• 先思考再寫程式，並且把思考寫下來。 規格之於軟體，正如建築師的藍圖之於建築——「不思考則保證我們必然」犯錯。
• 時間並非全域共享；真正存在的是因果關係。 既然沒有值得信賴的共享時鐘，就不該再問事件「何時」發生，而要問「什麼導致了什麼」。
• happened-before 關係與邏輯時鐘讓因果變得形式化。 Lamport 的偏序關係——以及實作它的每個行程內部計數器——正是向量時鐘與現代衝突解決機制的源頭。
• 先精確定義何謂正確，再加以證明。 安全性與活躍性、Paxos 共識、拜占庭容錯，以及 TLA+ 規格語言，全都源自把分散式運算當成數學、而非當成口耳相傳的經驗法則。

核心原則

「所謂分散式系統，就是一台你根本不知道其存在的電腦發生故障時，竟能讓你自己的電腦無法使用。」——Leslie Lamport¹

1987 年，他把這句話寄到實驗室的一個佈告欄上，而它之所以成為分散式運算裡最常被引用的一句話，是因為它道破了直覺拒絕相信的事實。¹您以為自己是在自己的電腦上跑一支程式。並不是。您是把它跑在一群機器上——這群機器的存在您未曾一一列舉、它們的時鐘彼此不一致，而且任何一台都可能恰好在最關鍵的那一瞬間故障。您腦中所能掌握的系統，與實際運行的系統，是兩個不同的系統；而每一個分散式錯誤，都活在兩者之間的落差裡。

Lamport 一生的事業，就是拒絕用樂觀主義去粉飾那道落差。他堅信並行與分散式系統過於微妙，無法靠直覺推理，因此必須在動筆寫下任何一行程式之前，先用數學在紙上推理。「思考並不保證我們不會犯錯，」他在 2013 年告訴《Wired》，「但不思考則保證我們必然犯錯。」²而這份思考必須寫下來，因為書寫正是讓草率思考無所遁形之處：「要思考，就必須書寫。如果你不寫而光是想，那你只是以為自己在思考。」³建築師在砌下第一塊磚之前會先畫好藍圖；軟體世界裡對應的就是規格。Lamport 後半段的職業生涯，都在主張我們的系統之所以崩壞，正是因為我們省略了這一步。⁴

更深一層的轉向，關乎時間本身。在物理世界裡，並不存在一個你能信賴、足以為跨機器事件排序的全域時鐘——因此你必須不再追問某件事「何時」發生，轉而追問「什麼導致了什麼」。一場分散式運算真正的結構是因果關係，而非掛在牆上的時鐘。⁵Lamport 所建立的幾乎一切，都源自認真看待這一個事實；這也正是貫穿證據門檻底下的同一份信念：你不能直接假定自己希望成立的順序；你必須把它確立出來。

背景脈絡

Leslie Lamport 於 1941 年 2 月 7 日生於紐約市。⁶他在 1960 年取得 MIT 數學學士學位，接著於 Brandeis 取得碩士，並在 1972 年取得數學博士，博士論文研究的是偏微分方程中的奇異點。⁶他並非科班出身的電腦科學家。他受的是數學家的訓練，而且從未停止以數學家的方式行事。他職業生涯最鮮明的特徵，就是把數學的標準——精確的定義、明確陳述的假設、用證明而非測試——帶進一個當時大多靠感覺寫程式的領域。

這些工作橫跨四個機構。1970 年代在 Massachusetts Computer Associates，他完成了關於事件排序的奠基性思考。在 SRI International（1977–1985），他做出了拜占庭將軍的研究。在 Digital Equipment Corporation 的 Systems Research Center（1985 年起，歷經 Compaq 併購一直到 2001 年），他寫出了 Paxos，並開始了規格化的工作。從 2001 年到 2025 年初退休為止，他任職於 Microsoft Research。⁶貫穿這一切的方法始終如一：在分散式或並行運算中找出一個眾人都當成口耳相傳經驗法則的問題，把它定義得精確到足以陳述一條定理，然後證明這條定理。

主要成就

時間、時鐘，與 happened-before 關係

〈Time, Clocks, and the Ordering of Events in a Distributed System〉於 1978 年刊登於《Communications of the ACM》，是整個電腦科學中被引用次數最多的論文之一——它在 2000 年榮獲 Dijkstra 獎，表彰分散式運算領域最具影響力的成果。⁵⁶它的洞見看似微不足道。在分散式系統中，並不存在一個共享、可信賴的時鐘，所以你無法靠比較時間戳來為兩個事件排序。你能知道的，是某個事件是否可能導致了另一個事件：若事件 A 與 B 位於同一行程且 A 在前，或者 A 是某訊息的發送、B 是該訊息的接收，則事件 A happened-before 事件 B。把這些串接起來，就得到了 happened-before 關係——讓因果變得形式化。⁵

關鍵而又違反直覺的後果是：happened-before 只是一種偏序，而非全序。位於不同行程、彼此之間沒有任何訊息鏈相連的兩個事件，是真正並行的：關於哪一個先發生，根本不存在客觀事實可言；任何佯裝有此事實的系統，都是在憑空捏造一個並不存在的順序。⁵接著 Lamport 給出了如今普遍被稱為 Lamport 時鐘的演算法：每個行程維護一個計數器，在每次事件時遞增它，並為每則發出的訊息蓋上這個時間戳；接收方則把自己的計數器推進到「自身值」與「訊息時間戳」兩者中較大者再加一。⁷這條簡單的規則所產生的時間戳與因果一致，而它正是向量時鐘、版本向量，以及現代分散式資料庫整套衝突解決機制的源頭。

這篇論文之所以超越其演算法本身而具有重大意義，是因為它改變了所提的問題。在 Lamport 之前，「這件事發生在什麼時間？」被認為是分散式系統中可以回答的問題。在 Lamport 之後，誠實的答案是「問錯了——該問是什麼導致了它」。正是這次的重新框定，讓他被認為是把分散式運算從一門手藝變成一門科學的人。

Paxos、共識，與複製狀態機

若沒有全域時鐘，而機器又會故障，那麼一群電腦究竟要如何對任何事情達成一致——哪一筆交易完成了提交、誰持有那把鎖、日誌裡的下一筆條目是什麼？這個問題就是共識問題，而 Lamport 的答案是 Paxos，這個演算法是此後幾乎每一個容錯系統的核心。他將它與複製狀態機的做法搭配在一起：只要每個副本都從相同的狀態出發，並以相同順序套用相同的指令序列，它們就會保持一致——於是整個維持分散式系統一致性的問題，便化約為對指令順序達成一致，而這恰恰正是 Paxos 所提供的。⁶

Paxos 如何發表的故事，是這個領域裡最著名的警世寓言。Lamport 把它寫成〈The Part-Time Parliament〉，將演算法包裝成一座虛構古希臘小島（名為 Paxos）的立法程序，連島上立法者的名字都用偽希臘文音譯自他同事們的姓名。⁸這個玩笑釀成了大災難。審稿人以為他不是認真的；論文被當成無足輕重而遭退稿；聽過他演講的人記得的是那套印第安納瓊斯式的場景，卻不記得那個演算法。⁸它就這樣未發表地擱置了好幾年。《Communications of the ACM》的編輯最終在 1998 年將它刊登於《ACM Transactions on Computer Systems》——仍然裹著那層寓言的外衣。⁸當這個領域繼續對它視而不見，Lamport 終於投降，在 2001 年寫了〈Paxos Made Simple〉，剝除希臘外衣，揭露他堅稱底下其實是個確實簡單的演算法。⁸他從中得出的教訓並不是「大家很笨」，而是：即使是一個正確、重要的想法，只要你把背後的思考遮蔽起來，它也會失敗——表達是工作的一部分，而非與工作分離的另一回事。

拜占庭將軍問題

1982 年，Lamport 與 Robert Shostak、Marshall Pease 一同發表了〈The Byzantine Generals Problem〉，為這個領域提供了描述最棘手那類故障的語言。⁶相較於拜占庭式的元件，當機的元件算是好對付的——拜占庭式的元件不會停下，而是會說謊，向不同的對等節點發送彼此不同、互相矛盾的資訊，無論是出於程式錯誤、資料損壞，還是惡意。論文的設定是：一支軍隊的數個師，各由一名將軍率領，必須透過信使對單一作戰計畫達成一致——進攻或撤退——而其中某個未知的將軍子集是叛徒，正積極阻撓達成一致。Lamport 證明了一個系統最多能容忍多少叛徒、卻仍能達成一致的精確門檻，把「萬一某個節點說謊怎麼辦？」從一種模糊的隱憂，變成了一條附帶明確上界的定理。

那條定理是每一個必須在部分參與者具有敵意時仍能持續運作的系統，其智識上的根源——也正因如此，數十年後，拜占庭一詞才會坐落於區塊鏈共識的核心位置。Lamport 並非為了催生加密貨幣而著手；他著手是為了精確定義：當「故障」包含了背叛，容錯究竟意味著什麼。

TLA+ 與規格化（沒錯，還有 LaTeX）

貫穿 Lamport 職業生涯的主軸，是「必須先規格化、再寫程式」的信念，而 TLA+ 正是把這份信念內建成工具。Temporal Logic of Actions（行動的時序邏輯）是一種語言，用來寫下對一個系統應當如何運作的精確數學描述——它的各種狀態、狀態之間的步驟，以及它必須始終滿足的性質（安全性：永遠不會發生壞事）與最終必須達成的性質（活躍性：好事終究會發生），這兩個概念都是由他形式化的。⁶你寫下規格，接著由模型檢查器探索整個狀態空間，找出那個會破壞你不變式的微妙交錯次序——那個你靠測試永遠找不到的錯誤，因為它只在三台機器以你從未想像過的順序做了三件事時才會現身。他的論證正是建築師的藍圖：你在灌下混凝土之前先把建築畫出來，而軟體規格就是同一張藍圖，用數學寫成，因為數學是我們所擁有最精確的語言。⁴

此外還有一座更安靜的紀念碑。1980 年代初，Lamport 在 Donald Knuth 的 TeX 之上，寫出了 LaTeX——這套巨集系統後來成為科學家與數學家排版文件的預設方式，也是整整一代論文與學位論文長成那副模樣的原因。⁶這是一件典型的 Lamport 式作品：他需要精確地寫下自己的工作，於是打造了讓所有人都能做到這件事的工具。催生出 TLA+ 的那股本能——一套迫使人精確的記號法——正是催生出 LaTeX 的同一股本能。

工作方法

這套方法是同一個想法、被毫不鬆懈地施行了五十年：思考本身就是工作，而思考必須在寫程式之前先寫下來。

以因果而非時間來推理。 沒有任何全域時鐘值得你信賴，因此不要再依事件何時發生來排序，而要依什麼導致了什麼來排序。真正的結構是 happened-before 關係，而非牆上的時鐘——而且承認兩個事件確實是並行的，比憑空捏造一個順序要來得誠實。⁵

先規格化，再寫程式。 對於任何尚無既定解法的事物，先停下來思考，而思考獨立於寫程式之外。把藍圖——也就是規格——用數學寫出來，因為散文含糊之處，數學簡潔而精確。⁴「不思考則保證我們必然」犯錯。²

透過書寫來查驗自己是否真的在思考。 書寫是檢驗一個念頭是否真實存在的試金石。「如果你不寫而光是想，那你只是以為自己在思考。」³一個你寫不下來的規格，就是一個你其實還沒真正擁有的想法。

精確定義那個故障。 「萬一某個節點說謊怎麼辦？」在你把它陳述為拜占庭將軍問題、並證明出容忍上界之前，都只是口耳相傳的經驗法則。精確的定義能把隱憂變成定理。⁶

表達是正確性的一部分。 Paxos 在任何人能使用它之前，已經正確了好幾年，因為那則希臘寓言把想法給埋葬了。一個沒有人能理解的正確結果，還沒有完成它的工程化。⁸

影響鏈

誰形塑了他

數學本身。 Lamport 受的是數學博士訓練，而非電腦科學；他整個貢獻的形貌，就是把數學的標準——定義、公理、證明——引進一個一直靠直覺寫程式的領域。⁶（奠基性影響）

1970 年代真實系統的容錯問題。 SRI 在航空可靠系統上的工作，以及機器在協定執行到一半時故障的實務噩夢，給了他具體的問題——拜占庭故障、共識——這些問題正需要他天生就擅長提供的形式化處理。⁶（直接影響）

Edsger Dijkstra。 「正確性是靠證明而非測試來確立」、以及「並行程式必須以形式化方式推理」這份信念，在屬於 Lamport 之前先屬於 Dijkstra。Lamport 因其時鐘論文所獲得的那個獎，正是以 Dijkstra 之名命名的。（直接影響）

他形塑了誰

每一個分散式資料庫、雲端平台，與區塊鏈。 邏輯時鐘支撐著分散式儲存中的衝突解決；Paxos（及其後裔 Raft）是 Google 的 Chubby 與 Spanner、ZooKeeper、etcd，以及幾乎每一朵雲協調層的共識核心。拜占庭將軍的結果，則是 Bitcoin 以及此後每一個容錯共識協定底下的理論地基。

業界的形式化方法。 Amazon Web Services 眾所周知地使用 TLA+ 來規格化並檢查 S3、DynamoDB 及其他核心服務，在交付之前——在設計階段、而非在正式環境中——找出微妙的錯誤。Lamport 的藍圖論證，從異端走成了實務。

這個領域的詞彙。 happened-before、安全性與活躍性、複製狀態機、循序一致性、拜占庭故障——這些並不是 Lamport 對分散式系統語言所做的貢獻；它們在很大程度上就是那套語言。

貫穿的主軸

Edsger Dijkstra 主張你要在執行程式之前先推理它的正確性——測試只能顯示錯誤的存在，永遠無法顯示其不存在——而 Lamport 是他的直接繼承者，把「執行前先證明」從循序程式，帶進了並行這個遠為艱難的世界；在這裡，你無法測試的那個錯誤是常態，而非例外。Barbara Liskov 以資料抽象與可替換性，讓「對程式行為進行形式化推理」成為一個可運作的基本元素；Lamport 則讓「對系統隨時間的行為進行形式化推理」成為標準，他規格化的不是某個物件保證什麼，而是整個並行系統必須始終、以及最終要做到什麼。而 Donald Knuth 為演算法分析帶來了數學上的嚴謹，並且幾乎是順帶地打造了 TeX，好讓工作能被精確地記載下來——這與 Lamport 形成了近乎精準的呼應：Lamport 出於同樣的理由，在 TeX 之上打造了 LaTeX，並讓規格化本身成為一種數學行為。三位數學家，都拒絕讓「它好像能跑」算作真正的知道。（系列銜接）

我從中學到的

我所牢記的教訓是：思考本身就是工作，而思考在被寫下來之前都不算真實。Lamport 的藍圖論證之所以令人不安，正因為它是對的：一個系統在正式環境中崩壞，原因幾乎從來不是程式碼打錯了——而是沒有人規格化過這個系統在並行與故障之下究竟應該做什麼，於是根本不存在一份可供拿來核對程式碼的陳述。這份紀律，就是在實作之前先寫下規格，而且要用精確到足以讓自身矛盾浮現出來的語言。這與品質是唯一的變數是同一套標準：要問的從來不是「這通得過順利路徑嗎？」而是「我是否精確地陳述了什麼必須始終為真——並且證明了設計確實守住它？」這也正是為什麼我如此倚重在寫程式之前先寫 PRD；一份 PRD，就是一份穿上工作服的 Lamport 規格。

在我如今所打造的世界裡——代理、工具迴圈、多代理系統——Lamport 的教訓正是幾乎所有人都跳過、然後付出代價的那一個。一個代理系統就是一個分散式系統：互相獨立的行程、沒有全域時鐘、訊息亂序抵達或根本不抵達，以及會無聲故障、甚至更糟糕地會說謊的元件。錯誤從來不在提示詞裡；它們在順序裡——兩個代理對著過時的狀態行動、某個工具呼叫的結果在需要它的決策之後才抵達、一對「並行」的事件被協調器佯裝排出了順序。Lamport 的紀律，就是不再信任牆上時鐘的直覺，而是明確地針對因果與故障進行推理，並在把任何東西接線在一起之前，先寫下什麼必須始終為真。「先規格化、再建造」、「對系統進行推理、而非戳它一下試試看」這份信念——正是從 1978 年那篇談時鐘的論文，一路貫穿到 2026 年某個代理框架的主軸；也正因如此，我才會把一個系統的效能與正確性當成你設計進去的性質，絕不當成你指望日後再除錯補回來的東西。

常見問題

Leslie Lamport 的工程哲學是什麼？

Lamport 堅信並行與分散式系統過於微妙，無法靠直覺推理，因此你必須在動筆寫程式之前，先用數學在紙上思考——就像建築師在砌下第一塊磚之前先畫好藍圖那樣。軟體的藍圖就是規格，用數學寫成，因為數學是現有最精確的語言。⁴在這之下還有一種對時間的立場：在分散式系統中，並不存在一個值得信賴的全域時鐘，因此一場運算真正的結構是因果關係——什麼導致了什麼——而非事情何時發生。⁵「思考並不保證我們不會犯錯，」他說，「但不思考則保證我們必然犯錯。」²

什麼是 Lamport 時鐘與 happened-before 關係？

happened-before 關係是 Lamport 對分散式系統中因果關係的形式化：若事件 A 與 B 位於同一行程且 A 在前，或者 A 發送一則訊息而 B 接收它，或經由串接這些情形，則事件 A happened-before 事件 B。⁵它只是一種偏序——位於不同行程、彼此之間沒有任何訊息相連的兩個事件，是真正並行的，沒有任何正確的系統能聲稱其中之一較先發生。⁵Lamport 時鐘以每個行程一個計數器來實作這件事：每次事件時遞增它，為每則發出的訊息蓋上它，並在接收時把計數器推進到「自身值」與「訊息時間戳」兩者中較大者再加一。⁷其結果是一組與因果一致的時間戳——這正是向量時鐘與現代分散式衝突解決的基礎。

什麼是 Paxos 與拜占庭將軍問題？

Paxos 是 Lamport 用於共識的演算法——讓一群不可靠、甚至可能故障的機器對單一數值達成一致，例如複製日誌中的下一條指令——它支撐著幾乎每一個現代分散式系統的協調層。眾所周知，他最初是把它當成一則關於虛構希臘議會的寓言來發表的（〈The Part-Time Parliament〉，《ACM TOCS》1998）；這個玩笑把想法遮蔽得太徹底，以致他最終在 2001 年將它重寫為〈Paxos Made Simple〉。⁸拜占庭將軍問題（Lamport、Shostak、Pease，1982）定義了最棘手的故障模式——元件不只是當機，而是會說謊、發送互相矛盾的資訊——並把它描繪成一群將軍試圖對一份計畫達成一致、而其中的叛徒則在破壞這份一致，並證明出一個系統最多能容忍多少叛徒。⁶它是區塊鏈共識的理論根源。

Leslie Lamport 為何獲得圖靈獎？

ACM 將 2013 年的 A.M. 圖靈獎頒給 Lamport，「以表彰他對分散式與並行系統理論及實務的根本性貢獻，尤其是發明了諸如因果與邏輯時鐘、安全性與活躍性、複製狀態機，以及循序一致性等概念。」⁶這段頌詞道盡了他工作的廣度：他把分散式運算從口耳相傳的經驗法則，變成一門帶有精確定義與證明的科學；他賦予了這個領域大半的詞彙；他創造了 TLA+ 規格語言，讓「先規格化、再寫程式」成為一種可實行的紀律；並且——在 Knuth 的 TeX 之上——寫出了 LaTeX，這套排版系統後來成為橫跨科學與數學的標準。⁶

參考來源