Leslie Lamport可能并不是一個(gè)家喻戶曉的名字，但對(duì)于計(jì)算機(jī)科學(xué)家們來(lái)說(shuō)，他是一些耳熟能詳?shù)摹该�字」幕后的貢獻(xiàn)者。比如Paxos算法、排版程序LaTeX、規(guī)格語(yǔ)言TLA+、「面包店算法」和「拜占庭將軍問(wèn)題」等等。

Leslie Lamport 徹底改變了現(xiàn)代計(jì)算機(jī)之間的對(duì)話方式。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)也會(huì)使我們遇到更多的問(wèn)題。

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

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

有了這個(gè)工具以后，計(jì)算機(jī)科學(xué)家開(kāi)始想知道他們?nèi)绾蜗到y(tǒng)地將這些連接的計(jì)算機(jī)變得更大，而不增加Bug。Lampor提出了一個(gè)優(yōu)雅的解決方案：Paxos，一種允許多臺(tái)計(jì)算機(jī)執(zhí)行復(fù)雜任務(wù)的「一致性算法」。沒(méi)有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所開(kāi)發(fā)的規(guī)格語(yǔ)言TLA+使得工程師能夠以一種精確的、數(shù)學(xué)的方式描述程序的目標(biāo)。自20世紀(jì)90年代以來(lái)，Lamport的工作就一直專注于「形式驗(yàn)證」（formal verification），即使用數(shù)學(xué)證明來(lái)驗(yàn)證軟件和硬件系統(tǒng)的正確性。他的突出貢獻(xiàn)便是創(chuàng)建了一種「規(guī)格語(yǔ)言」，稱為TLA+（Temporal Logic of Actions，行為時(shí)序邏輯）。軟件規(guī)格說(shuō)明就像一個(gè)程序的藍(lán)圖或配方，它描述軟件應(yīng)該如何在高層次上運(yùn)行。這并不總是必要的，因?yàn)榫帉懸粋�(gè)簡(jiǎn)單的程序就像煮一個(gè)雞蛋一樣。但若是一項(xiàng)更復(fù)雜、風(fēng)險(xiǎn)更高的任務(wù)，則需更高的精確度，編寫這樣一個(gè)程序就相當(dāng)于準(zhǔn)備一場(chǎng)九道菜的盛宴。你需要準(zhǔn)備每道菜的每個(gè)組成部分，以一種精確的方式組合它們，然后按照正確的順序把它們端給每一位客人。這需要精確的食譜和說(shuō)明，并以明確簡(jiǎn)潔的語(yǔ)言來(lái)書(shū)寫，而描寫成英語(yǔ)散文，則可能會(huì)導(dǎo)致誤解。TLA+使用精確的數(shù)學(xué)語(yǔ)言來(lái)防止錯(cuò)誤和避免設(shè)計(jì)缺陷。

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

這些成就并不是偶然的。這位81歲的計(jì)算機(jī)科學(xué)家對(duì)于人們?nèi)绾问褂煤退伎架浖�有著不同尋常的�?jiàn)解。

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

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

2013年圖靈獎(jiǎng)得主 Leslie Lamport 專訪：程序員需要更多的數(shù)學(xué)知識(shí)
圖注：Lamport參觀加州山景城的計(jì)算機(jī)歷史博物館

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

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

Quanta：他們?cè)�有的算法存在什么�?wèn)題？

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