Leslie Lamport可能并不是一個家喻戶曉的名字，但對于計算機科學家們來說，他是一些耳熟能詳的「名字」幕后的貢獻者。比如Paxos算法、排版程序LaTeX、規格語言TLA+、「面包店算法」和「拜占庭將軍問題」等等。

Leslie Lamport 徹底改變了現代計算機之間的對話方式。2013年，他被授予圖靈獎，以表彰他在分布式系統方面的工作。

在分布式系統中，不同網絡上的多個組件協調一致，以實現一個共同的目標。互聯網搜索、云計算和人工智能都需要協調眾多強大的計算機器協同工作。當然，這種協調也會使我們遇到更多的問題。

Lamport曾經說過：「分布式系統是這樣一種系統，在這種系統中，一臺你甚至不知曉其存在的計算機出現了故障，就會導致你自己的計算機無法使用。」

最大的問題來源之一是「并發系統」，即在重疊的時間片段內發生多個計算操作，這導致了一種模糊性：哪臺計算機的時鐘是正確的？在1978年的一篇開創性論文中，Lamport引入了「因果關系」的概念，利用狹義相對論的觀點來解決這個問題。兩個觀察者在事件順序上可能存在分歧，但如果是一個事件導致另一個事件的發生，那么就能消除模糊性。發送或接收消息可以在多個進程之間建立因果關系。「邏輯時鐘」（現在也被稱為Lamport時鐘），提供了一種標準的方法來對并發系統進行推理。

有了這個工具以后，計算機科學家開始想知道他們如何系統地將這些連接的計算機變得更大，而不增加Bug。Lampor提出了一個優雅的解決方案：Paxos，一種允許多臺計算機執行復雜任務的「一致性算法」。沒有Paxos及其算法家族，現代計算就不可能存在。Paxos算法現在已經成為行業標準。

Lamport的另一貢獻，是他在上世紀80年代初創建了文檔準備系統LaTeX，提供了復雜公式排版和科學文檔格式的復雜方法。不僅在數學和計算機科學領域，而且在大多數科學領域，LaTeX已經成為論文格式的標準。

另外，Lamport所開發的規格語言TLA+使得工程師能夠以一種精確的、數學的方式描述程序的目標。自20世紀90年代以來，Lamport的工作就一直專注于「形式驗證」（formal verification），即使用數學證明來驗證軟件和硬件系統的正確性。他的突出貢獻便是創建了一種「規格語言」，稱為TLA+（Temporal Logic of Actions，行為時序邏輯）。軟件規格說明就像一個程序的藍圖或配方，它描述軟件應該如何在高層次上運行。這并不總是必要的，因為編寫一個簡單的程序就像煮一個雞蛋一樣。但若是一項更復雜、風險更高的任務，則需更高的精確度，編寫這樣一個程序就相當于準備一場九道菜的盛宴。你需要準備每道菜的每個組成部分，以一種精確的方式組合它們，然后按照正確的順序把它們端給每一位客人。這需要精確的食譜和說明，并以明確簡潔的語言來書寫，而描寫成英語散文，則可能會導致誤解。TLA+使用精確的數學語言來防止錯誤和避免設計缺陷。

將你的菜譜或規格作為輸入，一個叫做模型檢查器的程序會檢查菜譜是否合理、是否按預期工作，從而按照廚師的要求做出一道菜。在Lamport為程序員編寫適當的規格以前，程序員們經常胡亂拼湊一個系統，這曾讓他感到惋惜，畢竟廚師在不知道自己的食譜是否正確的情況下，是無法為宴會準備食物的。

這些成就并不是偶然的。這位81歲的計算機科學家對于人們如何使用和思考軟件有著不同尋常的見解。

最近，Quanta Magazine對Lamport進行了一次專訪，討論了他在分布式系統方面的工作。在采訪中，Lamport談論了他所創建的TLA+語言如何幫助程序員構建更好的系統，還談及了當前計算機科學教育中存在的問題，強調了數學思維在計算機科學中的重要性。

AI科技評論在不改變原意的基礎上對該專訪進行了編譯，以饗讀者。

2013年圖靈獎得主 Leslie Lamport 專訪：程序員需要更多的數學知識
圖注：Lamport參觀加州山景城的計算機歷史博物館

Quanta：我們先從Paxos談起，因為它是一個非常有影響力的算法。能否談談是什么驅動您開始做這項工作的？

Lamport：當時人們使用一些代碼去構建一個系統，我有種預感，他們的代碼所試圖實現的目標是不可能的。因此，我決定嘗試去證明這一點，并提出了一種人們應該在他們的系統中使用的算法。

Quanta：他們原有的算法存在什么問題？

Lamport：他們并沒有算法，而是只有一堆代碼。很少有程序員用算法來思考問題。在嘗試編寫并發系統時，如果只編寫代碼而沒有算法，那么你的程序必然會到處都是bug。