如何寫出在數學層面完美的軟件

編譯 苦山

萊斯利·蘭波特徹底改變了計算機之間的交流方式。如今，他正致力于研究工程師如何與自己的機器交流。

計算機科學家萊斯利·蘭波特的成果使得現代計算機能夠有效地相互協調。從那以來，他將注意力轉向了提高編程本身的效率

萊斯利·蘭波特（Leslie Lamport）也許不是一個家喻戶曉的名字，但對于計算機科學家而言，他是以下成果的幕后功臣：排版程序LaTeX，以及使谷歌和亞馬遜的云基礎設施成為可能的研究。他還引領人們對一些問題給予了更多關注，給這些問題起了具有特點的名字，比如“面包店算法”和“拜占庭將軍問題”。這絕非偶然。這位81歲的計算機科學家對于人們如何使用和看待軟件有著異乎尋常的縝密考量。

2013年，他因在分布式系統方面的工作獲得了圖靈獎，它被認為是計算機領域的諾貝爾獎。分布式系統是指不同網絡上的多個組件協同工作以實現共同目標的系統?；ヂ摼W搜索、云計算和人工智能都涉及協調強大的計算機集群共同工作。當然，這種協作會帶來更多的問題。

蘭波特曾經說過：“在分布式系統中，若有一臺你甚至不知其存在的計算機出現故障，就可能導致你自己的計算機無法使用?！?/p>

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

有了這個工具，計算機科學家們接下來想知道他們如何能夠系統地擴大這些連接的計算機的規模，同時不增加錯誤數量。蘭波特提出了一個優雅的解決方案：Paxos，一種允許多臺計算機執行復雜任務的“共識算法”。如果沒有Paxos及其算法家族，現代計算就不可能存在。

在20世紀80年代早期，蘭波特在開發這一領域時還創建了LaTeX，這是一個文檔準備系統，它為復雜公式的排版和科學文檔的格式編排提供了精密巧妙的方式。LaTeX不僅在數學和計算機科學領域，而且在大多數科學領域都已成為論文格式編排的標準。

蘭波特參觀加利福尼亞州山景城的計算機歷史博物館

自20世紀90年代以來，蘭波特的工作主要集中在“形式驗證”上，即利用數學證明來驗證軟件和硬件系統的正確性。值得注意的是，他創建了一種名為行為時序邏輯（TLA+）的“規范語言”。軟件規范就像是程序的藍圖或配方，它描述了軟件在高層次上應該如何運行。這并非總是必需的，因為編寫一個簡單的程序就和煮雞蛋一樣輕松。但是，一個更加復雜、風險更高的任務——相當于一場九道菜的宴席——則要求更高的精確度。你需要準備好每道菜的每個組成部分，將它們以一種精確的方式組合起來，隨后按照正確的順序提供給每位客人。這就需要用明確簡潔的語言寫出準確的食譜和說明，但用英語寫出的描述可能會留下誤解的空間。TLA+采用精確的數學語言來防止錯誤、避免設計缺陷。

一個叫做“模型檢查器”的程序會把你的“食譜”——也就是規范——當作輸入，以檢查食譜是否有意義、是否按照預期的方式工作，從而按照廚師的要求生產出一道菜。蘭波特抱怨道，程序員時常先拼湊出一個系統，然后才編寫正確的規范，然而廚師若不事先知道他們的食譜可行，是絕不會為宴會提供食物的。

《量子雜志》與蘭波特討論了他在分布式系統方面的工作、計算機科學教育中的問題，以及使用TLA+如何能幫助程序員構建更好的系統。為了清晰起見，下述訪談內容經過了整理簡編。

讓我們從Paxos開始聊吧，因為它是一個影響力如此之大的算法。你最初是出于什么理由著手開發它的？

人們用一些代碼建立了一個系統，而我有預感，他們的代碼想要完成的事情是不可能做到的。所以我決定嘗試證明這一點，并且想出了一種算法——人們理應在他們的系統中使用這種算法。

他們原來的算法有什么問題？

這個嘛，他們原有的其實并非算法，而只是一堆代碼。很少有程序員從算法層面思考問題。在嘗試編寫并發系統時，如果只是編寫代碼而不使用算法，那么你的程序里必然全是錯誤。

介紹Paxos的那篇論文起初并沒有得到廣泛的閱讀。為什么會這樣？

令人們無法閱讀這篇論文的原因是我喜歡用故事來解釋事物，而且我還為角色起了一些偽希臘字母的名字。例如，在論文中有一個奶酪檢查員名叫Γωδα。作為一個數學家，我整天和希臘字母打交道，也就沒有意識到非數學家會被這些字母嚇到。顯然，它們對讀者來說是個問題，因此讀這篇論文的人比預計的要少了許多。

所以，起初它的接受度并不高。盡管從長遠來看，它還是得到了廣泛的認可，因為人們把這個共識算法家族稱為“Paxos”，而非“視圖戳記復制”（viewstamped replication），后者是計算機科學家芭芭拉·利斯科夫（Barbara Liskov）給同一算法起的另一個名字。

在從事了這么多年的分布式系統工作之后，又是什么讓你開始研究TLA+的？

在20世紀70年代，當人們還在對程序進行推理的時候，他們在做的是證明程序本身的屬性，并將這些屬性以編程語言的方式表述出來。隨后人們意識到，他們真正應該表述的是程序應該首先完成的任務，也就是程序的行為。

在20世紀80年代早期，我意識到為并發系統編寫這些高級規范的一種實用方法是將它們作為抽象算法來編寫。通過TLA+，我能夠以一種完全嚴謹的方式在數學層面表達它們。于是一切都變得順利了?；径?，這其中所涉及的并非試圖用編程語言來編寫算法：如果你真的想把事情做對，你需要用數學的方式來編寫算法。

你曾經說過，如果你光思考卻不寫，那你就只是自認為在思考罷了。這就是模型檢查的作用嗎？

模型檢查是對系統的小模型的所有執行情況進行詳盡測試的一種方法。它只顯示模型的正確性，而非算法的正確性。當模型檢查測試正確性時，編碼只生成代碼。它并不測試任何東西。在模型檢查出現之前，確保算法有效的唯一方法是編寫一個證明。

在實踐中，模型檢查會檢查算法的一個小實例的所有執行情況。如果你足夠幸運，你可以檢查足夠大的實例，這會讓你對算法產生足夠的信心。但這一證明可以確證它對于任何規模的系統和算法的任何應用都是正確的。

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

Coq旨在進行真正的數學運算，并能夠捕捉數學家所做的推理。例如，喬治·龔提爾（Georges Gonthier）正是用它證明了四色定理。一個經過了機器檢查的數學陳述的證明表明，該陳述幾乎肯定為真。

蘭波特在過去幾十年里開發的規范語言TLA+允許工程師以精確的數學方式描述程序的目標

TLA+不是為數學家設計的，而是為那些想要證明其系統屬性的工程師設計的。20世紀90年代，在花費了大約15年的時間編寫并發算法的證明之后，我了解到了需要做哪些事才能證明并發算法的正確性。TLA是一種允許完全形式化的邏輯。TLA+則是基于此的完整語言。

像TLA+這樣的規范語言并沒有在行業中得到廣泛的應用，對吧？你認為這是為什么呢？

這個嘛，我盡力而為了。但基本上，程序員和許多計算機科學家（甚至是絕大多數計算機科學家）都對數學心懷恐懼。所以這是一個很艱難的推廣過程。

其次，每個項目都必須在匆忙中完成。有句老話說：“永遠沒有時間去把事情做對。但總有時間把事情再做一遍?！庇捎赥LA+涉及一些前期工作，這意味著你在開發過程中添加了一個新步驟，這也讓它的推廣變得很難。

這種前期努力是否總是值得？

的確，世界各地的程序員所編寫的大多數代碼并不需要事先非常精確地說明它應該做到什么。但有些的確重要，它們需要是正確無誤的。

蘭波特認為，在編程前先行思考和寫作極為重要，這一點需要在本科計算機科學課程中進行教授，但實際并未如此

當人們制造芯片的時候，他們希望芯片能正常工作。當人們構建云基礎設施時，他們不希望出現會丟失人們數據的錯誤。對于那種精度非常重要的應用程序，你需要非常嚴格，需要類似TLA+這樣的東西，特別是在涉及并發的情況下，而這些系統中通常都會涉及并發。

程序員是否傾向于把更多的時間花在寫代碼上，而非在思考代碼上？

是的，在編程前先行思考和寫作極為重要，這一點需要在本科計算機科學課程中進行教授，但實際并未如此。其原因在于，教授程序設計的人和教授程序驗證的人之間缺少交流。

在我看來，這一分歧的雙方都有錯。教編程的人不了解驗證，但他們理應了解。教驗證的人員則不了解如何在實踐中應用驗證。

在這一鴻溝彌合之前，TLA+是不會擁有大量用戶的。我希望我至少能讓教并發編程的人明白他們需要它。這樣也許才會有一些希望。

我感覺你對最近的計算機科學教育不太滿意。是因為它沒有給予數學足夠的重視嗎？

對數學思維的重視不夠，沒錯。

蘭波特因其在計算機協作（該領域被稱為分布式系統）方面的成果獲得了2013年的圖靈獎。他的Paxos算法現已成為行業標準

那么，換做是你的話，會如何構建本科課程呢？

我不是教育工作者，所以我并不清楚怎么教他們數學思維。但我知道人們應該學什么。他們不應該害怕數學。這只是簡單的數學，他們可能已經上過一門相關課程，卻不知道如何運用它。他們不知道數學有什么好處。他們學到的知識足以通過考試，然后就把學過的東西忘了。

數學家常說他們在數學中看到美。你是從這個領域起步的，那么你看到算法之美了嗎？

我不從美學的角度考慮。我可能和其他人有同樣的感受，但我會用不同的詞語來表述它們。我不會說算法是“美”的。但“簡潔”是我非?？粗氐臇|西。

最后一個問題，是關于你的另一個具有相當大影響力的項目LaTeX的。我想最后和你這位創造者澄清一件事。它的發音是“LAH-tekh”還是“LAY-tekh”？

哪個都行。我不建議你花太多時間思考這件事。

資料來源 Quanta Magazine