Leslie Lamport可能并不是一個(gè)家喻戶曉的名字，但對于計(jì)算機(jī)科學(xué)家們來說，他是一些耳熟能詳?shù)摹该帧鼓缓蟮呢暙I(xiàn)者。比如Paxos算法、排版程序LaTeX、規(guī)格語言TLA+、「面包店算法」和「拜占庭將軍問題」等等。

Leslie Lamport 徹底改變了現(xiàn)代計(jì)算機(jī)之間的對話方式。2013年，他被授予圖靈獎(jiǎng)，以表彰他在分布式系統(tǒng)方面的工作。

在分布式系統(tǒng)中，不同網(wǎng)絡(luò)上的多個(gè)組件協(xié)調(diào)一致，以實(shí)現(xiàn)一個(gè)共同的目標(biāo)。互聯(lián)網(wǎng)搜索、云計(jì)算和人工智能都需要協(xié)調(diào)眾多強(qiáng)大的計(jì)算機(jī)器協(xié)同工作。當(dāng)然，這種協(xié)調(diào)也會使我們遇到更多的問題。

Lamport曾經(jīng)說過：「分布式系統(tǒng)是這樣一種系統(tǒng)，在這種系統(tǒng)中，一臺你甚至不知曉其存在的計(jì)算機(jī)出現(xiàn)了故障，就會導(dǎo)致你自己的計(jì)算機(jī)無法使用?！?/span>

最大的問題來源之一是「并發(fā)系統(tǒng)」，即在重疊的時(shí)間片段內(nèi)發(fā)生多個(gè)計(jì)算操作，這導(dǎo)致了一種模糊性：哪臺計(jì)算機(jī)的時(shí)鐘是正確的？在1978年的一篇開創(chuàng)性論文中，Lamport引入了「因果關(guān)系」的概念，利用狹義相對論的觀點(diǎn)來解決這個(gè)問題。兩個(gè)觀察者在事件順序上可能存在分歧，但如果是一個(gè)事件導(dǎo)致另一個(gè)事件的發(fā)生，那么就能消除模糊性。發(fā)送或接收消息可以在多個(gè)進(jìn)程之間建立因果關(guān)系?！高壿嫊r(shí)鐘」（現(xiàn)在也被稱為Lamport時(shí)鐘），提供了一種標(biāo)準(zhǔn)的方法來對并發(fā)系統(tǒng)進(jìn)行推理。

有了這個(gè)工具以后，計(jì)算機(jī)科學(xué)家開始想知道他們?nèi)绾蜗到y(tǒng)地將這些連接的計(jì)算機(jī)變得更大，而不增加Bug。Lampor提出了一個(gè)優(yōu)雅的解決方案：Paxos，一種允許多臺計(jì)算機(jī)執(zhí)行復(fù)雜任務(wù)的「一致性算法」。沒有Paxos及其算法家族，現(xiàn)代計(jì)算就不可能存在。Paxos算法現(xiàn)在已經(jīng)成為行業(yè)標(biāo)準(zhǔn)。

Lamport的另一貢獻(xiàn)，是他在上世紀(jì)80年代初創(chuàng)建了文檔準(zhǔn)備系統(tǒng)LaTeX，提供了復(fù)雜公式排版和科學(xué)文檔格式的復(fù)雜方法。不僅在數(shù)學(xué)和計(jì)算機(jī)科學(xué)領(lǐng)域，而且在大多數(shù)科學(xué)領(lǐng)域，LaTeX已經(jīng)成為論文格式的標(biāo)準(zhǔn)。

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

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

這些成就并不是偶然的。這位81歲的計(jì)算機(jī)科學(xué)家對于人們?nèi)绾问褂煤退伎架浖兄煌瑢こ５囊娊狻?/span>

最近，Quanta Magazine對Lamport進(jìn)行了一次專訪，討論了他在分布式系統(tǒng)方面的工作。在采訪中，Lamport談?wù)摿怂鶆?chuàng)建的TLA+語言如何幫助程序員構(gòu)建更好的系統(tǒng)，還談及了當(dāng)前計(jì)算機(jī)科學(xué)教育中存在的問題，強(qiáng)調(diào)了數(shù)學(xué)思維在計(jì)算機(jī)科學(xué)中的重要性。

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

圖注：Lamport參觀加州山景城的計(jì)算機(jī)歷史博物館

Quanta：我們先從Paxos談起，因?yàn)樗且粋€(gè)非常有影響力的算法。能否談?wù)勈鞘裁打?qū)動您開始做這項(xiàng)工作的？

Lamport：當(dāng)時(shí)人們使用一些代碼去構(gòu)建一個(gè)系統(tǒng)，我有種預(yù)感，他們的代碼所試圖實(shí)現(xiàn)的目標(biāo)是不可能的。因此，我決定嘗試去證明這一點(diǎn)，并提出了一種人們應(yīng)該在他們的系統(tǒng)中使用的算法。

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

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

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

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

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

所以在一開始Paxos的應(yīng)用效果并不太好，但從長遠(yuǎn)來看它的確實(shí)現(xiàn)了它的目標(biāo)，因?yàn)槿藗兎Q這一系列的共識算法為Paxos，而不是「viewstamped replication」（這是計(jì)算機(jī)科學(xué)家、圖靈獎(jiǎng)得主Barbara Liskov對共識算法的另一個(gè)命名）。

Quanta：在分布式系統(tǒng)領(lǐng)域研究了這么多年之后，是什么讓您開始了創(chuàng)建TLA+的工作？

Lamport：在20世紀(jì)70年代，當(dāng)人們對程序進(jìn)行推理時(shí)，他們試圖證明程序本身的屬性，這些屬性是用編程語言表述的。后來人們意識到，他們確實(shí)應(yīng)該說明程序首先要完成什么——即程序的行為。

在20世紀(jì)80年代初，我意識到，為并發(fā)系統(tǒng)編寫這些更高級別規(guī)格的實(shí)用方法，是將它們編寫為抽象的算法。有了TLA+，我就能夠以一種足夠嚴(yán)謹(jǐn)?shù)姆绞接脭?shù)學(xué)去表達(dá)它們。后來證明，TLA+的確做得很出色。重要的是，不要試圖用編程語言來編寫算法：如果你真的想把事情做好，你需要用數(shù)學(xué)的術(shù)語來編寫你的算法。

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

Lamport：模型檢測是一種全面檢測系統(tǒng)小模型的所有執(zhí)行情況的方法。它只顯示模型的正確性，而不是算法的正確性。當(dāng)模型檢測去驗(yàn)證正確性時(shí)，編碼只會生成代碼，它不測試任何東西。在進(jìn)行模型檢測之前，確保算法有效的唯一方法是寫證明（proof）。

在具體實(shí)踐中，模型檢測會檢查算法的一個(gè)小實(shí)例的所有執(zhí)行情況。如果幸運(yùn)的話，您可以檢查足夠多的實(shí)例，從而使你對算法有足夠的信心。但對于任何規(guī)模的系統(tǒng)和算法的使用，證明都可以驗(yàn)證其正確性。

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

Lamport：Coq的目的是解決真正的數(shù)學(xué)問題，它能夠捕捉數(shù)學(xué)家所做的推理。例如， Georges Gonthier用它來證明了四色定理（four-color theorem）。一個(gè)數(shù)學(xué)命題的證明經(jīng)過機(jī)器驗(yàn)證后，幾乎可以肯定該命題為真。

TLA+不是為數(shù)學(xué)家設(shè)計(jì)的，而是為希望證明其系統(tǒng)特性的工程師設(shè)計(jì)的。20世紀(jì)90年代，在花了大約15年的時(shí)間編寫并發(fā)算法的證明之后，我了解到為了證明并發(fā)算法的正確性需要做什么。TLA是能夠一種讓證明過程具有完全的形式化的邏輯，而且TLA+也是基于TL邏輯的一套完整語言。

Quanta：像TLA+這樣的規(guī)范語言在工業(yè)中使用得不是很廣泛，是嗎？您認(rèn)為這是為什么？

Lamport：我正在盡我所能。但基本上，程序員和許多（如果不是大多數(shù)的話）計(jì)算機(jī)科學(xué)家都被數(shù)學(xué)給嚇壞了。所以它的「銷路」很困難。

另外，每個(gè)項(xiàng)目都必須急匆匆地趕完。有句老話，「永遠(yuǎn)沒有足夠的時(shí)間把一件事做到完美，但總是有時(shí)間去重新來過?！挂?yàn)門LA+涉及到前期工作，在開發(fā)過程中又會添加新步驟，所以這也導(dǎo)致了它沒有被廣泛使用。

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

Lamport：的確，世界各地的程序員編寫的大多數(shù)代碼都不需要非常精確的語句來說明它應(yīng)該做什么。但有些事情很重要，需要保證正確。

例如，當(dāng)人們制造芯片時(shí)，他們希望芯片能正常工作。當(dāng)人們構(gòu)建云基礎(chǔ)設(shè)施時(shí)，他們不希望出現(xiàn)會丟失人們數(shù)據(jù)的bug。對于那些要求精度的應(yīng)用程序，你需要非常嚴(yán)格。而且你需要類似于TLA+的東西，尤其是當(dāng)涉及到通常存在于這些系統(tǒng)中的并發(fā)時(shí)。

Quanta：程序員是否傾向于花更多的時(shí)間去寫代碼而非思考代碼？

Lamport：是的，在編寫代碼之前進(jìn)行思考和寫作的重要性，需要在本科的計(jì)算機(jī)科學(xué)課程中教授，但事實(shí)并非如此。原因是教編程的人和教程序驗(yàn)證的人之間沒有交流。

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

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

Quanta：我感覺到，您對近年來的計(jì)算機(jī)科學(xué)教育不太滿意。是不是因?yàn)閷?shù)學(xué)重視不夠？

Lamport：是的，在數(shù)學(xué)思維方面。

Quanta：那么，您會如何構(gòu)建本科課程？

Lamport：我不是一個(gè)教育家，所以我不知道如何教他們。但我知道人們應(yīng)該學(xué)到什么。他們不應(yīng)該害怕數(shù)學(xué)。他們可能學(xué)過一門簡單的數(shù)學(xué)，但不知道如何使用它。他們不知道這有什么好處。他們學(xué)了足夠多的知識，通過了考試，然后就拋之腦后。

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

Lamport：我并不從美學(xué)的角度來考慮。我可能和其他人有同樣的感覺，但我只是用不同的語言來表達(dá)。關(guān)于算法，我考慮的不是美，簡單是我非?？粗氐臇|西。