新智元報道
編輯：David
【新智元導讀】圖靈獎得主、分散式系統先驅、LaTeX之父Leslie Lamport認為，對於程式設計師而言，對數學思維的強調永遠不會過分，要寫出好程式碼，不能懼怕數學。預告：居家辦公讓虛擬人來作伴？歡迎預約直播，教你如何從0到1自己建立一個！
Leslie Lamport可能不是一個家喻戶曉的名字，但一提到和他有關的研究，相信你一定不陌生。
排版程式LaTeX和分散式系統。前者發過論文的都懂，後者則使谷歌和亞馬遜的雲基礎設施成為可能。
2013年，Lamport因其在分散式系統方面的工作而獲得圖靈獎（A。M。 Turing Award）。
這位81歲的計算機科學家對人們如何使用和思考軟體，有著不同尋常的思考。
有了分散式系統，網際網路搜尋、雲計算和人工智慧都可以協調強大的計算機器叢集一起工作。
不過，這類系統也存在一些不可避免的問題。
Lamport曾經說過：「在分散式系統中，你甚至不知道存在的計算機故障，會使你自己的計算機無法使用。」
其中最大的問題來源是 「併發系統」，多個計算操作會發生在重疊的時間片段上，導致了模糊不清的情況。哪臺計算機的時鐘是正確的？
在1978年的一篇開創性的論文中，Lamport引入了「因果關係」的概念來解決這個問題，使用的是狹義相對論的一個觀點。
兩個觀察者可能對事件的順序有異議，但如果一個事件導致了另一個事件，這就消除了模糊性。而傳送或接收一個資訊可以在多個過程中建立因果關係。邏輯時鐘——現在也稱為「Lamport時鐘」提供了一種推理併發系統的標準方法。
有了這個工具，計算機科學家接下來想知道，他們如何能夠系統地擴大這些連線的計算機叢集的規模，同時不增加錯誤的數量。Lamport提出了一個優雅的解決方案。
Paxos，這是一種 「共識演算法」，允許多臺計算機執行復雜的任務。沒有Paxos和它的算法系列，現代分散式計算就不可能存在。
20世紀80年代初，Lamport還建立了LaTeX，這是一個文件準備系統，為複雜公式的排版和科學檔案的格式提供了複雜的方法。
現在，LaTeX不僅在數學和計算機科學領域，而且在大多數科學領域都已成為論文格式的主流標準。
自20世紀90年代以來，Lamport的工作重點是 “形式驗證”，即使用數學證明來驗證軟體和硬體系統的正確性。值得注意的是，他創造了一種名為TLA+（行動的時間邏輯）的 “規範語言”。
大師專訪：用數學的思考寫演算法
最近，QuantaMagazine與Lamport談了他在分散式系統方面的工作，計算機科學教育的問題，以及使用TLA+如何幫助程式設計師建立更好的系統。
以下是訪談內容簡編。
讓我們從Paxos開始，因為它是如此有影響力的演算法。是什麼讓你一開始就開始研究這個問題？
人們正在用一些程式碼建立一個系統，我有一種預感，他們的程式碼試圖完成的事情是不可能的。所以我決定嘗試證明這一點，並想出了一種演算法，而這些人本應在他們的系統中使用我這種演算法。
他們原來的演算法有什麼問題？
嗯，他們其實沒有演算法，只有一堆程式碼。很少有程式設計師從演算法上思考問題。當你試圖編寫一個併發系統時，如果你只是寫程式碼，而沒有演算法，你的程式裡就一定全是錯誤。
介紹Paxos的那篇論文起初並沒有被廣泛閱讀。為什麼？
讓人們無法閱讀論文的原因是，我喜歡透過講故事來解釋事情，而且我為角色編造了一些偽希臘字母的名字。
例如，在論文中，有一個名叫Γωυδα的乳酪檢查員。我是作為數學家長大的，整天和希臘字母打交道，不知道非數學家會不會被這些字母完全嚇壞了。
顯然，這對很多讀者而言是個問題，所以讀那篇文章的人少了不少。
一開始效果並不理想。雖然從長遠來看，它確實如此，因為人們稱這個共識算法系列為Paxos，而不是 「viewstamped replication」，這是計算機科學家Barbara Liskov對該演算法的另一個稱謂。
在從事了這麼多年的分散式系統工作後，是什麼讓你又開始搞TLA+的？
在20世紀70年代，當人們對程式進行推理時，實際上是在證明程式本身的屬性，再以程式語言的方式陳述出來。後來人們意識到，其實應該首先說明程式應該完成什麼任務，即程式的行為。
到了80年代初，我意識到為併發系統編寫這些高階規範的一個實用方法，就是把它們寫成抽象的演算法。有了TLA+，我就能以一種完全嚴謹的方式來表達。一切都變得簡單了。
這就意味著基本上不能用程式語言來寫演算法。如果你真的想把事情做對，你需要用數學的術語來寫你的演算法，你知道這樣做一定會成功的。
Lamport認為，在動手寫程式碼之前，要先思考和寫作的重要性，這需要在本科計算機科學課程中教授，而現在卻沒有。
你曾說過，「如果你只是思考，不寫程式碼，你只是認為你在思考而已」。這就是模型檢查的作用嗎？
模型檢查是一種詳盡地測試系統的小模型的所有執行情況的方法。它只是顯示模型的正確性，而不是演算法的正確性。當模型檢查測試正確性時，編碼只是產生程式碼。它並不測試任何東西。在有模型檢查之前，確定你的演算法能正常work的唯一方法是寫一個證明。
在實踐中，模型檢查會檢查演算法的一個小例項的所有執行情況。如果你很幸運，你可以檢查足夠大的例項，使你對該演算法有足夠的信心。
聽起來，模型檢查與另一種程式驗證方法有關：使用Coq等工具進行互動式定理證明。它們有什麼不同？
Coq的設計是為了做真正的數學，並且能夠捕捉數學家所做的推理。例如，Georges Gonthier就是用它來證明四色定理的。一個經過機器檢查的數學陳述的證明表明，該陳述幾乎肯定是真的。
而TLA+不是為數學家設計的，而是為那些想證明其系統屬性的工程師設計的。上世紀90年代，在花了大約15年時間編寫併發演算法的證明之後，我瞭解到為了證明一個併發演算法的正確性，你需要做什麼。
TLA是一種邏輯，它允許所有的完全形式化表述。而TLA+則是基於此的完整語言。
Lamport因在分散式系統方面的工作在2013年獲得了A。M。 圖靈獎。他提出的Paxos演算法，現在已經成為一個行業的通行標準。
像TLA+這樣的規範語言在工業界的應用並不廣泛，對嗎？你認為這是為什麼呢？
嗯，我一直在盡力推廣這個規範。但基本上，程式設計師和許多計算機科學家都被數學嚇壞了。所以這是一個很艱難的推銷過程。
第二，每一個專案都必須在匆忙中完成。有一句老話，“永遠沒有時間做正確的事。總有時間重做”。因為TLA+涉及前期工作，你在開發過程中增加了一個新的步驟，也會成為一個難點。
這種努力總是值得的嗎？
的確，世界各地的程式設計師所寫的大多數程式碼都不需要非常精確地說明它應該做什麼。但是，有些事情是重要的，需要正確的。
當人們建造一個晶片時，他們希望這個晶片能夠正常工作。當人們建立一個雲基礎設施時，他們不希望出現會丟失人們的資料的錯誤。
對於那種精度很重要的應用，你需要非常嚴格，需要像TLA+這樣的東西，特別是在涉及到併發的情況下，而在這些系統中通常會有併發。
由Lamport在過去幾十年中開發的規範語言TLA+，讓工程人員可以以精確的數學方式描述程式要實現的目標
程式設計師花在寫程式碼上的時間比花在思考上的時間多，這是否是一種偏見？
是的，在編寫程式碼之前思考和寫作的重要性需要在本科計算機科學課程中教授，而現在卻沒有。而原因是，教程式設計的人和教程式驗證的人之間沒有溝通。
從我所看到的情況來看，錯誤在於這個鴻溝的兩邊。教程式設計的人不知道他們需要知道的驗證。教驗證的人不瞭解它應該如何在實踐中應用。
在這個鴻溝被填平之前，TLA+是不可能擁有大量使用者的。我希望我至少能讓教併發程式設計的人明白，他們需要TLA+。這樣也許才會有一些希望。
我感覺，你對現在的計算機科學教育不太滿意。是不是對覺得對數學強調得不夠？
對數學思維的重視不夠，是的，遠遠不夠。
那麼，按你的想法，本科計算機課程應該怎樣設定？
我不是教育家，所以我不知道如何教學生。但我知道人們應該學什麼。他們不應該害怕數學。這只是簡單的數學，他們可能已經學過一門課程，但不知道如何使用，也不知道使用數學有什麼好處。
他們只是學了足夠的東西來透過考試，然後就把學過的東西忘了。
數學家經常說，他們在數學中看到了美。你是在這個領域起步的，你有在演算法中看到美嗎？
我不從美不美的角度考慮。我可能有其他人的那種感覺，但我會用不同的詞來表達。「美」不是我對演算法的評價。但是「簡單性」是我非常重視的一點。
最後一個問題，是關於你的另一個專案 LaTeX的。想最後跟你澄清一件事。LaTeX到底怎麼讀？是LAH-tekh還是LAY-tekh？
想怎麼讀就怎麼讀。我建議不要花太多的時間去考慮這個問題。
參考連結：
https：//www。quantamagazine。org/computing-expert-says-programmers-need-more-math-20220517/
—分割線—
【元宇宙·新人類 第3期直播重磅來襲！】
居家辦公是不是有虛擬人作伴更好？如何從0到1建立一個虛擬人？虛擬人產業大爆炸，有哪些應用場景和商業化路徑？
歡迎掃碼下方海報預約直播，為你解答一切疑惑