92歲圖靈獎得主：沒博士學位，卻改寫了編程

一位沒讀過博士的牛津古典學畢業生，拿了圖靈獎、英國皇家爵士頭銜，還發明了程序員每天用的東西。Tony Hoare上周去世，92歲。

他的貢獻清單長得離譜：快速排序、霍爾邏輯、通信順序進程（CSP）、空指針的發明（以及公開道歉）……隨便拎一個出來，都夠別人吃一輩子。

更離譜的是他的寫作。學術圈能把遞歸講清楚的人不少，但像他這么寫的，沒見過——

「解決無限遞歸的辦法簡單且戲劇性：允許把想要的結論本身作為證明過程的假設。于是我們被允許證明過程體具有某個性質，假設每次遞歸調用都具有該性質，然后斷言每次調用——遞歸或非遞歸——都具有該性質。這種在證明開始前就假設我們想證明的東西，很好地解釋了程序員初次接觸遞歸編程時感受到的那種魔法氛圍。」

這是他在圖靈獎演講里解釋遞歸公理規則的原話。沒有公式轟炸，沒有居高臨下，像是在跟朋友聊一個有點tricky的魔術手法。

從行業碼農到學術宗師

Hoare給人的印象是標準老派教授：永遠打領帶，照片里幾乎沒見過他穿休閑裝（除了本文開頭那張船上照片）。但這形象有誤導性。

他職業生涯起步于企業，做的是程序員和項目經理。學術背景更是非主流——牛津古典學訓練，數學和邏輯全是自學。沒有博士學位，后來拿了一堆榮譽博士。

這種"野路子"背景反而塑造了他的風格：永遠關注真正重要的問題，拒絕為復雜而復雜。

快速排序（Quicksort）是他26歲時在莫斯科開會，沒聽報告在旅館想出來的。這個算法至今仍是編程入門必學，也是實際應用最廣的排序方法之一。

霍爾邏輯（Hoare Logic）給程序驗證奠定了數學基礎，讓"證明程序正確"從哲學討論變成可操作的數學問題。

CSP（通信順序進程）影響了Go語言的并發模型、Erlang的設計，甚至Rust的某些思想也能追溯到這兒。

那個價值十億美元的錯誤

Hoare最有名的一句話，可能是2009年QCon大會上的道歉：

「我稱之為我的十億美元錯誤。1965年我發明了空引用（null reference）……當時我設計第一個面向對象語言ALGOL W的全面類型系統，目標是確保所有對引用的使用都絕對安全，由編譯器自動檢查。但我沒能抵擋住誘惑，加入了空引用，只因為實現起來太容易?！?/p>

這個"偷懶"的設計，導致此后幾十年無數程序崩潰、安全漏洞、調試噩夢。Java的NullPointerException、C#的null引用問題，全源于此。

他后來花大力氣研究如何"還債"——設計避免空引用的類型系統，比如SPARK語言和Rust的所有權系統都有他的影子。

能公開承認錯誤并持續修正的科學家，不多見。

一圖讀懂：Hoare的技術遺產

如果把他的貢獻畫成一張圖，核心是這個邏輯鏈條——

基礎層：算法

快速排序。分治思想的典范，平均時間復雜度O(n log n)，原地排序，緩存友好?，F代優化版本（三數取中、隨機化、尾遞歸優化）仍在用。

驗證層：邏輯

霍爾三元組 {P} C {Q}。前置條件、程序、后置條件。把程序執行變成可推導的數學命題。現代形式化驗證工具（Coq、Isabelle）的理論根基。

并發層：CSP

進程通過顯式通道通信，而非共享內存。Go的goroutine+channel、Erlang的actor模型，都是這一思想的工程實現。"不要通過共享內存通信，要通過通信共享內存"——Go的這句口號，源頭在這里。

糾錯層：空安全

從"發明錯誤"到"修正錯誤"的完整弧線?，F代語言的可空類型（Nullable Types）、Rust的Option、Swift的Optional，都是對他早年設計的反思與超越。

為什么現在還要讀Hoare

他的論文沒有一篇是"水"的。1978年圖靈獎演講《皇帝的舊衣》批評軟件工程過度依賴管理方法而非技術本質；1980年CSP論文用40頁定義了一套完整并發理論；2003年還在發論文討論"統一編程理論"。

這種持續產出高質量工作的能力，來自他對"寫作即思考"的堅持。他說研究和寫作沒有明確界限——寫不清楚，就是沒想明白。

對今天的技術從業者，Hoare的啟示很具體：

第一，基礎問題值得反復做。排序、并發、類型安全，這些"老問題"他研究了幾十年，每次都有新進展。

第二，工程直覺和數學嚴謹可以兼得。他既有企業編程經驗，又能寫出最嚴格的邏輯證明。

第三，承認錯誤是進步的開始?？罩羔樀牡狼覆皇亲藨B，而是推動了整個類型系統領域的演進。

數據收束

92年，圖靈獎1座，皇家爵士頭銜1個，榮譽博士10+個，核心論文被引用次數超過50000次?？焖倥判蛟贕itHub公開代碼中出現頻率排名前10的算法之一。CSP直接影響了至少3門主流編程語言的設計?？罩羔樝嚓P漏洞至今仍在CVE數據庫中每年新增數百條記錄——他發明的錯誤，我們還在付錢。