編譯 苦山

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

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

萊斯利·蘭波特（Leslie Lamport）也許不是一個家喻戶曉的名字，但對于計算機科學家而言，他是以下成果的幕后功臣：排版程序LaTeX，以及使谷歌和亞馬遜的云基礎(chǔ)設(shè)施成為可能的研究。他還引領(lǐng)人們對一些問題給予了更多關(guān)注，給這些問題起了具有特點的名字，比如“面包店算法”和“拜占庭將軍問題”。這絕非偶然。這位81歲的計算機科學家對于人們?nèi)绾问褂煤涂创浖兄惡鯇こ５目b密考量。

2013年，他因在分布式系統(tǒng)方面的工作獲得了圖靈獎，它被認為是計算機領(lǐng)域的諾貝爾獎。分布式系統(tǒng)是指不同網(wǎng)絡(luò)上的多個組件協(xié)同工作以實現(xiàn)共同目標的系統(tǒng)?；ヂ?lián)網(wǎng)搜索、云計算和人工智能都涉及協(xié)調(diào)強大的計算機集群共同工作。當然，這種協(xié)作會帶來更多的問題。

蘭波特曾經(jīng)說過：“在分布式系統(tǒng)中，若有一臺你甚至不知其存在的計算機出現(xiàn)故障，就可能導致你自己的計算機無法使用。”

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

有了這個工具，計算機科學家們接下來想知道他們?nèi)绾文軌蛳到y(tǒng)地擴大這些連接的計算機的規(guī)模，同時不增加錯誤數(shù)量。蘭波特提出了一個優(yōu)雅的解決方案：Paxos，一種允許多臺計算機執(zhí)行復雜任務(wù)的“共識算法”。如果沒有Paxos及其算法家族，現(xiàn)代計算就不可能存在。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

當人們制造芯片的時候，他們希望芯片能正常工作。當人們構(gòu)建云基礎(chǔ)設(shè)施時，他們不希望出現(xiàn)會丟失人們數(shù)據(jù)的錯誤。對于那種精度非常重要的應(yīng)用程序，你需要非常嚴格，需要類似TLA+這樣的東西，特別是在涉及并發(fā)的情況下，而這些系統(tǒng)中通常都會涉及并發(fā)。

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

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

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

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

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

對數(shù)學思維的重視不夠，沒錯。

蘭波特因其在計算機協(xié)作（該領(lǐng)域被稱為分布式系統(tǒng)）方面的成果獲得了2013年的圖靈獎。他的Paxos算法現(xiàn)已成為行業(yè)標準

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

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

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

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

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

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

資料來源 Quanta Magazine