如何寫(xiě)出在數(shù)學(xué)層面完美的軟件

編譯 苦山

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

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

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

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

蘭波特曾經(jīng)說(shuō)過(guò)：“在分布式系統(tǒng)中，若有一臺(tái)你甚至不知其存在的計(jì)算機(jī)出現(xiàn)故障，就可能導(dǎo)致你自己的計(jì)算機(jī)無(wú)法使用?！?/p>

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

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

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

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

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

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

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

讓我們從Paxos開(kāi)始聊吧，因?yàn)樗且粋€(gè)影響力如此之大的算法。你最初是出于什么理由著手開(kāi)發(fā)它的？

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

他們?cè)瓉?lái)的算法有什么問(wèn)題？

這個(gè)嘛，他們?cè)械钠鋵?shí)并非算法，而只是一堆代碼。很少有程序員從算法層面思考問(wèn)題。在嘗試編寫(xiě)并發(fā)系統(tǒng)時(shí)，如果只是編寫(xiě)代碼而不使用算法，那么你的程序里必然全是錯(cuò)誤。

介紹Paxos的那篇論文起初并沒(méi)有得到廣泛的閱讀。為什么會(huì)這樣？

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

所以，起初它的接受度并不高。盡管從長(zhǎng)遠(yuǎn)來(lái)看，它還是得到了廣泛的認(rèn)可，因?yàn)槿藗儼堰@個(gè)共識(shí)算法家族稱為“Paxos”，而非“視圖戳記復(fù)制”（viewstamped replication），后者是計(jì)算機(jī)科學(xué)家芭芭拉·利斯科夫（Barbara Liskov）給同一算法起的另一個(gè)名字。

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

在20世紀(jì)70年代，當(dāng)人們還在對(duì)程序進(jìn)行推理的時(shí)候，他們?cè)谧龅氖亲C明程序本身的屬性，并將這些屬性以編程語(yǔ)言的方式表述出來(lái)。隨后人們意識(shí)到，他們真正應(yīng)該表述的是程序應(yīng)該首先完成的任務(wù)，也就是程序的行為。

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

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

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

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

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

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

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

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

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

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

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

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

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

蘭波特認(rèn)為，在編程前先行思考和寫(xiě)作極為重要，這一點(diǎn)需要在本科計(jì)算機(jī)科學(xué)課程中進(jìn)行教授，但實(shí)際并未如此

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

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

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

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

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

我感覺(jué)你對(duì)最近的計(jì)算機(jī)科學(xué)教育不太滿意。是因?yàn)樗鼪](méi)有給予數(shù)學(xué)足夠的重視嗎？

對(duì)數(shù)學(xué)思維的重視不夠，沒(méi)錯(cuò)。

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

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

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

數(shù)學(xué)家常說(shuō)他們?cè)跀?shù)學(xué)中看到美。你是從這個(gè)領(lǐng)域起步的，那么你看到算法之美了嗎？

我不從美學(xué)的角度考慮。我可能和其他人有同樣的感受，但我會(huì)用不同的詞語(yǔ)來(lái)表述它們。我不會(huì)說(shuō)算法是“美”的。但“簡(jiǎn)潔”是我非?？粗氐臇|西。

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

哪個(gè)都行。我不建議你花太多時(shí)間思考這件事。

資料來(lái)源 Quanta Magazine