亚洲中文字幕在线一区二区三区|精品在免费线中文字幕久久|成人精品一区二区三区电影免费|中文字幕av一区中文字幕

咨詢熱線:021-80392549

2013年圖靈獎得主 Leslie Lamport 專訪:程序員需要更多的數(shù)學(xué)知識

放大字體  縮小字體 發(fā)布日期:2022-05-24     來源:雷鋒網(wǎng)     瀏覽次數(shù):662
核心提示:Leslie Lamport可能并不是一個家喻戶曉的名字,但對于計算機科學(xué)家們來說,他是一些耳熟能詳?shù)摹该帧鼓缓蟮呢暙I者。比如Paxos算
人物
Leslie Lamport可能并不是一個家喻戶曉的名字,但對于計算機科學(xué)家們來說,他是一些耳熟能詳?shù)摹该帧鼓缓蟮呢暙I者。比如Paxos算法、排版程序LaTeX、規(guī)格語言TLA+、「面包店算法」和「拜占庭將軍問題」等等。

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

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

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

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

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

Lamport的另一貢獻,是他在上世紀(jì)80年代初創(chuàng)建了文檔準(zhǔn)備系統(tǒng)LaTeX,提供了復(fù)雜公式排版和科學(xué)文檔格式的復(fù)雜方法。不僅在數(shù)學(xué)和計算機科學(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的工作就一直專注于「形式驗證」(formal verification),即使用數(shù)學(xué)證明來驗證軟件和硬件系統(tǒng)的正確性。他的突出貢獻便是創(chuàng)建了一種「規(guī)格語言」,稱為TLA+(Temporal Logic of Actions,行為時序邏輯)。軟件規(guī)格說明就像一個程序的藍圖或配方,它描述軟件應(yīng)該如何在高層次上運行。這并不總是必要的,因為編寫一個簡單的程序就像煮一個雞蛋一樣。但若是一項更復(fù)雜、風(fēng)險更高的任務(wù),則需更高的精確度,編寫這樣一個程序就相當(dāng)于準(zhǔn)備一場九道菜的盛宴。你需要準(zhǔn)備每道菜的每個組成部分,以一種精確的方式組合它們,然后按照正確的順序把它們端給每一位客人。這需要精確的食譜和說明,并以明確簡潔的語言來書寫,而描寫成英語散文,則可能會導(dǎo)致誤解。TLA+使用精確的數(shù)學(xué)語言來防止錯誤和避免設(shè)計缺陷。

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

這些成就并不是偶然的。這位81歲的計算機科學(xué)家對于人們?nèi)绾问褂煤退伎架浖兄煌瑢こ5囊娊狻?br />
最近,Quanta Magazine對Lamport進行了一次專訪,討論了他在分布式系統(tǒng)方面的工作。在采訪中,Lamport談?wù)摿怂鶆?chuàng)建的TLA+語言如何幫助程序員構(gòu)建更好的系統(tǒng),還談及了當(dāng)前計算機科學(xué)教育中存在的問題,強調(diào)了數(shù)學(xué)思維在計算機科學(xué)中的重要性。

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

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

Quanta:我們先從Paxos談起,因為它是一個非常有影響力的算法。能否談?wù)勈鞘裁打?qū)動您開始做這項工作的?

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

Quanta:他們原有的算法存在什么問題?

Lamport:他們并沒有算法,而是只有一堆代碼。很少有程序員用算法來思考問題。在嘗試編寫并發(fā)系統(tǒng)時,如果只編寫代碼而沒有算法,那么你的程序必然會到處都是bug。 
工博士工業(yè)品商城聲明:凡資訊來源注明為其他媒體來源的信息,均為轉(zhuǎn)載自其他媒體,并不代表本網(wǎng)站贊同其觀點,也不代表本網(wǎng)站對其真實性負(fù)責(zé)。您若對該文章內(nèi)容有任何疑問或質(zhì)疑,請立即與商城(m.pjyby.com)聯(lián)系,本網(wǎng)站將迅速給您回應(yīng)并做處理。
聯(lián)系電話:021-31666777
新聞、技術(shù)文章投稿QQ:3267146135  投稿郵箱:syy@gongboshi.com