|
今年8月，雷鋒網(wǎng)將在深圳舉辦盛況空前的“全球人工智能與機(jī)器人峰會(huì)”（CCF-GAIR）,，屆時(shí)雷鋒網(wǎng)(公眾號(hào)：雷鋒網(wǎng))將發(fā)布“人工智能&機(jī)器人Top25創(chuàng)新企業(yè)榜”榜單,。目前，我們正在逐一拜訪人工智能,、機(jī)器人領(lǐng)域的相關(guān)公司,，從中篩選最終入選榜單的公司名單。如果你也想加入我們的榜單之中,，請(qǐng)聯(lián)系：[email protected],。 不管你是不是程序員，你都一定學(xué)過或者聽過C,、Java以及PHP這樣的語(yǔ)言。 沒錯(cuò),，它們是最受程序員歡迎的編程語(yǔ)言。 但有一個(gè)人或許將改變這一格局,，這個(gè)人就是耶魯大學(xué)的終身正教授,、FLINT實(shí)驗(yàn)室主任——邵中,，他是編程語(yǔ)言學(xué)術(shù)界名聲最旺的華人，計(jì)算機(jī)程序語(yǔ)言設(shè)計(jì)領(lǐng)域的國(guó)際權(quán)威,。 不過,，如果你認(rèn)為邵中只是一個(gè)技藝超群的碼農(nóng)，那你就輸了,！更準(zhǔn)確的說他是程序語(yǔ)言標(biāo)準(zhǔn)的制定者,，其研發(fā)的SML/NJ已經(jīng)成為了SML語(yǔ)言最流行的編譯器。 邵中（右） 他和代碼之間的淵源還要從小時(shí)候說起,！ 邵中是1968年出生的，小時(shí)候的他就展現(xiàn)出了超強(qiáng)的學(xué)習(xí)能力,，讀小學(xué)開始做中學(xué)的題,，中學(xué)看大學(xué)的課本。 就是這樣的節(jié)奏,，讓邵中在15歲的時(shí)候就從江蘇常熟中學(xué)考入了中科大少年班,，他學(xué)的是計(jì)算機(jī)科學(xué)專業(yè)。 中科大少年班學(xué)員 面對(duì)來自全國(guó)各地的天才少年們,，邵中對(duì)自己的要求就更高了。大學(xué)幾年他幾乎把所有能看的程序語(yǔ)言類的書籍看了個(gè)遍,，當(dāng)你還只會(huì)寫“Hello World”的時(shí)候,，人家已經(jīng)掌握了各種復(fù)雜程序的原理，于是他又成為了那一屆少年班最優(yōu)秀的畢業(yè)生之一,，并且順手拿了個(gè)中科大郭沫若獎(jiǎng)學(xué)金,。 把編程技術(shù)練到了極致后，邵忠覺得做一個(gè)普通的程序員太沒意思了,！ 所以,，1988年從中科大畢業(yè)之后，邵中又來到了美國(guó)普林斯頓大學(xué)留學(xué),，1991年獲得了該校的計(jì)算機(jī)科學(xué)碩士學(xué)位,，接著在1994年拿到了博士學(xué)位。 你以為邵中不遠(yuǎn)萬(wàn)里來到美國(guó)就是為了拿兩個(gè)學(xué)位證,，圖樣... 在普林斯頓大學(xué)期間,，他跟著導(dǎo)師就在貝爾實(shí)驗(yàn)室計(jì)算機(jī)科學(xué)研究中心做項(xiàng)目，當(dāng)時(shí)他在為SML語(yǔ)言（Standard ML）研發(fā)一個(gè)編譯器,。 沒聽過SML是什么的程序員,，趕緊面壁思過去。（前方高能，非程序員請(qǐng)系好安全帶?。?/p> 做個(gè)小科普,，程序語(yǔ)言其實(shí)可以分為三大類：第一種是命令式的語(yǔ)言，如C,，C++,，Java等；第二種是邏輯式的語(yǔ)言,，如Prolog,；而第三種就是本認(rèn)為更符合人類思維的函數(shù)式語(yǔ)言，如約翰·麥卡錫(John McCarthy)發(fā)明的LISP和ML（SML是其中的一個(gè)分支）,。 懂編程的朋友都知道,，函數(shù)式語(yǔ)言比傳統(tǒng)的編程語(yǔ)言更加高深，它是一種非馮·諾依曼式的程序設(shè)計(jì)語(yǔ)言,，它的代碼更簡(jiǎn)潔也更容易理解,，而且適合多線程編程。 例如在人工智能領(lǐng)域,，需要處理非常復(fù)雜的數(shù)據(jù)結(jié)構(gòu),，函數(shù)式語(yǔ)言的優(yōu)勢(shì)就非常明顯。 但是,，這種語(yǔ)言也有一個(gè)非常致命的缺點(diǎn)，就是執(zhí)行效率非常低,，所以函數(shù)式語(yǔ)言基本上只活躍在學(xué)術(shù)界,，很少有商業(yè)化的。 不過邵中還是沒有放棄,，他希望開發(fā)一款高效的編譯器來解決這個(gè)問題,。 博士畢業(yè)后，邵中來到了位于康涅狄格州紐黑文市的耶魯大學(xué),，這位偏執(zhí)的年輕人在擔(dān)任學(xué)校計(jì)算機(jī)科學(xué)系的助理教授的同時(shí),，還在為那款編譯器而奮斗著。 所以,，除了每天輔導(dǎo)學(xué)生之外，他經(jīng)常到貝爾實(shí)驗(yàn)室計(jì)算機(jī)科學(xué)研究中心做一些有關(guān)SML/NJ（Standard ML of New Jersey）的設(shè)計(jì),。 雖然過程很坎坷,，但最終邵中和其他幾位研究人員還是成功研發(fā)出了SML語(yǔ)言最著名的編譯器——SML/NJ，并且獲得了美國(guó)國(guó)家科學(xué)基金青年學(xué)者獎(jiǎng),。 這一發(fā)明讓邵中的編譯風(fēng)格成為編程語(yǔ)言學(xué)術(shù)研究的典范,，同時(shí)也奠定了其在編程語(yǔ)言界的地位,，現(xiàn)在C++和Java什么的都開始對(duì)函數(shù)式編程提供專門語(yǔ)法支持,。 然而故事還沒有結(jié)束,！ 不久之后，邵中又在FLINT上的研發(fā)取得了突破,，讓類型檢查可以在編譯的任何階段進(jìn)行,。 這樣的研究成果讓耶魯大學(xué)折服了，
現(xiàn)在邵中還是耶魯大學(xué)的FLINT實(shí)驗(yàn)組的主任，研究的方向包括形式化方法開發(fā)可信的kernel,、 新型編程語(yǔ)言,、并發(fā)多核軟件、自動(dòng)定理證明系統(tǒng)等等,。 不懂沒關(guān)系,，看看邵中拿的研究經(jīng)費(fèi)你就知道他研究的項(xiàng)目有多牛X！ 在美國(guó)二十幾年,，邵中從美國(guó)國(guó)家科學(xué)基金會(huì)（NSF）,、美國(guó)國(guó)防部、微軟以及英特爾等手中拿到的研究經(jīng)費(fèi)就達(dá)到了數(shù)千萬(wàn)美元,，其中去年一年就有八百多萬(wàn)美元,，別人拿獎(jiǎng)拿到手軟，他是拿經(jīng)費(fèi)拿到手軟,。 不過在編程學(xué)術(shù)界,，不發(fā)表幾篇像樣的論文做再多研究也是枉然。 邵中是一個(gè)寫論文的好手,，從本科畢業(yè)到現(xiàn)在他一共發(fā)表了七十多篇論文,，其中在POPL上發(fā)表的就有五篇，例如2006年發(fā)表的《嵌入式匯編程序設(shè)計(jì)》以及2012年發(fā)表的《靜態(tài)和用戶可擴(kuò)展的驗(yàn)證檢查》,。 這是什么樣的概念呢,？...拿中國(guó)舉個(gè)例子，中國(guó)大陸學(xué)術(shù)界以第一作者的身份在POPL上發(fā)表過論文的只有一個(gè),，而且這篇論文還是出自邵中領(lǐng)導(dǎo)的中科大－耶魯聯(lián)合中心,。（POPL是編程語(yǔ)言領(lǐng)域歷史最久,、水平最高的國(guó)際會(huì)議，論文錄用率平均不到20%） 當(dāng)然,，邵中還是個(gè)社交能力很強(qiáng)的學(xué)術(shù)專家,，他經(jīng)常會(huì)在全球這頂級(jí)大會(huì)上（如POPL、PLDI和ICFP等）和全球各地的專家交流,，其中2012年第39屆POPL大會(huì)就是他主持的,！ |
|
|
