2013年圖靈獎得主 Leslie Lamport 專訪：程式設計師需要更多的數學知識

• 2022 年 5 月 24 日
• AI

作者｜李梅

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科技評論在不改變原意的基礎上對該專訪進行了編譯，以饗讀者。

圖註：Lamport參觀加州山景城的電腦歷史博物館

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

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

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

Lamport：他們並沒有演算法，而是只有一堆程式碼。很少有程式設計師用演算法來思考問題。在嘗試編寫並發系統時，如果只編寫程式碼而沒有演算法，那麼你的程式必然會到處都是bug。

Quanta：介紹Paxos的那篇論文（「The Part-Time Parliament」）起初並沒有被廣為閱讀。為什麼會這樣？

論文鏈接：//dl.acm.org/doi/pdf/10.1145/279227.279229

Lamport：原因可能是我喜歡用故事來解釋事情，而且我用希臘字母來為人物命名。例如，在論文中，有一位乳酪檢查員名叫ΓωИΔα。身為一名數學家，在這裡隨處可見希臘字母，我只是沒有意識到那些不是數學家的人會被這些字母給嚇到。這導致了這篇原本應該被看見的論文而沒有被看見。

所以在一開始Paxos的應用效果並不太好，但從長遠來看它的確實現了它的目標，因為人們稱這一系列的共識演算法為Paxos，而不是「viewstamped replication」（這是電腦科學家、圖靈獎得主Barbara Liskov對共識演算法的另一個命名）。

Quanta：在分散式系統領域研究了這麼多年之後，是什麼讓您開始了創建TLA+的工作？

Lamport：在20世紀70年代，當人們對程式進行推理時，他們試圖證明程式本身的屬性，這些屬性是用程式語言表述的。後來人們意識到，他們確實應該說明程式首先要完成什麼——即程式的行為。

在20世紀80年代初，我意識到，為並發系統編寫這些更高級別規格的實用方法，是將它們編寫為抽象的演算法。有了TLA+，我就能夠以一種足夠嚴謹的方式用數學去表達它們。後來證明，TLA+的確做得很出色。重要的是，不要試圖用程式語言來編寫演算法：如果你真的想把事情做好，你需要用數學的術語來編寫你的演算法。

Quanta：您曾說過，「如果你只思考而不寫作，你就只會思考你在思考的東西。」這就是模型檢測（model checking）的目的嗎？

Lamport：模型檢測是一種全面檢測系統小模型的所有執行情況的方法。它只顯示模型的正確性，而不是演算法的正確性。當模型檢測去驗證正確性時，編碼只會生成程式碼，它不測試任何東西。在進行模型檢測之前，確保演算法有效的唯一方法是寫證明（proof）。

在具體實踐中，模型檢測會檢查演算法的一個小實例的所有執行情況。如果幸運的話，您可以檢查足夠多的實例，從而使你對演算法有足夠的信心。但對於任何規模的系統和演算法的使用，證明都可以驗證其正確性。

Quanta：聽起來，模型檢測與另一種程式驗證方法有關：使用Coq等工具進行互動式定理證明。它們有何不同？

Lamport：Coq的目的是解決真正的數學問題，它能夠捕捉數學家所做的推理。例如， Georges Gonthier用它來證明了四色定理（four-color theorem）。一個數學命題的證明經過機器驗證後，幾乎可以肯定該命題為真。

TLA+不是為數學家設計的，而是為希望證明其系統特性的工程師設計的。20世紀90年代，在花了大約15年的時間編寫並發演算法的證明之後，我了解到為了證明並發演算法的正確性需要做什麼。TLA是能夠一種讓證明過程具有完全的形式化的邏輯，而且TLA+也是基於TL邏輯的一套完整語言。

Quanta：像TLA+這樣的規範語言在工業中使用得不是很廣泛，是嗎？您認為這是為什麼？

Lamport：我正在盡我所能。但基本上，程式設計師和許多（如果不是大多數的話）電腦科學家都被數學給嚇壞了。所以它的「銷路」很困難。

另外，每個項目都必須急匆匆地趕完。有句老話，「永遠沒有足夠的時間把一件事做到完美，但總是有時間去重新來過。」因為TLA+涉及到前期工作，在開發過程中又會添加新步驟，所以這也導致了它沒有被廣泛使用。

Quanta：前期的工作是否總是值得的？

Lamport：的確，世界各地的程式設計師編寫的大多數程式碼都不需要非常精確的語句來說明它應該做什麼。但有些事情很重要，需要保證正確。

例如，當人們製造晶片時，他們希望晶片能正常工作。當人們構建雲基礎設施時，他們不希望出現會丟失人們數據的bug。對於那些要求精度的應用程式，你需要非常嚴格。而且你需要類似於TLA+的東西，尤其是當涉及到通常存在於這些系統中的並發時。

Quanta：程式設計師是否傾向於花更多的時間去寫程式碼而非思考程式碼？

Lamport：是的，在編寫程式碼之前進行思考和寫作的重要性，需要在本科的電腦科學課程中教授，但事實並非如此。原因是教編程的人和教程式驗證的人之間沒有交流。

就我所見，這一分歧的兩邊都存在問題。教編程的人不了解他們需要知道的驗證，而教授驗證的人不理解它應該如何應用和在實踐中使用。

在彌合這一鴻溝之前，TLA+是不會收穫大量用戶的。我希望我至少能讓教授並發編程的人明白他們需要TLA+。那樣的話，TLA+也許還有希望被更多人使用。

Quanta：我感覺到，您對近年來的電腦科學教育不太滿意。是不是因為對數學重視不夠？

Lamport：是的，在數學思維方面。

Quanta：那麼，您會如何構建本科課程？

Lamport：我不是一個教育家，所以我不知道如何教他們。但我知道人們應該學到什麼。他們不應該害怕數學。他們可能學過一門簡單的數學，但不知道如何使用它。他們不知道這有什麼好處。他們學了足夠多的知識，通過了考試，然後就拋之腦後。

Quanta：數學家常說他們在數學中看到了美。你是從演算法領域起步的，那麼您看到演算法之美了嗎？

Lamport：我並不從美學的角度來考慮。我可能和其他人有同樣的感覺，但我只是用不同的語言來表達。關於演算法，我考慮的不是美，簡單是我非常看重的東西。

參考鏈接：

//www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

雷峰網