科學人／太不優雅了！拒絕一行行寫程式 密爾納搖身成計算機理論科學奠基者

密爾納（ArthurJohn Robin Gorell Milner,1934~2010）把「計算機科學」從單純演算法與數學函數理論，擴展為資訊流動與互動機制的研究 ，將其視為一門可應用於許多領域的資訊和互動機制科學。資訊科學展現了一種洞察力，即資訊行為比計算機或計算包含了更廣泛的見解。他的目標不僅要模仿人工代理之間的互動行為，還要模仿與自然代理之間的互動。最終，我們的資訊模型應該與自然科學融合，並增強自然科學。

然而，密爾納曾認為，一個接一個編寫指令的行為是武斷而不優雅的。他的結論是：「程式設計並不是一件非常美好的事。我下定決心，這輩子都不會靠近電腦。」因此他後續未攻讀博士學位。三年後，他在計算機製造商工作，再次使用了計算機。1963年他改變了對程式設計的看法，認為對程式設計的深入理解，可構成優雅實踐的基礎，熱情激昂轉而走入學術界。

某次，密爾納前往英國牛津參與斯特拉奇（Christopher Strachey）和史考特（Dana Scott）的講座，主題是可算泛函。這是他對程式驗證和語義感興趣的真正起點。在斯旺西大學，他編寫了自己的第一個自動定理證明器，但因為無法做任何有趣的事而敗下陣來。

密爾納對當時程式語言的不便利感到不滿，例如LISP程式語言有一堆出錯的可能性。當密爾納於1974年搬到英國愛丁堡時，想利用LISP開發出一種從未實現的「抽象」語言，但具有清晰的數學基礎和抽象機器的操作語義。

密爾納發明的新程式語言是ML語言（meta language）。這是一個強大而高效的實用工具，以數學的清晰度來進行定義，非常適合於證明任務。ML語言遠遠領先於時代，建立在乾淨和清晰的數學思想之上，可以獨立研究，也可以相對容易地重新混合和重複使用。

密爾納因為早期研究三個不同方面而完整的成就，獲頒1991年圖靈獎。他設計的可算泛函邏輯（LCF）是第一個基於理論但實用的機器輔助證明工具，而他發明的ML語言是第一種包含多態類型推理和類型安全異常處理機制的語言，他的通信系統演算（CCS）完備了並行理論。此外，他還制定並大力推進了完全抽象的操作語義和指稱語義之間關係的研究。

密爾納所有研究的最關鍵因素是，他結合了數學基礎的深刻見解與對實踐和美學問題同樣深刻的理解，從而以令人興奮的方式把理論應用到實際生活。此外，他的嚴謹學術風格和對細節的關注為所有人樹立了榜樣。

（本文出自2026.3.5《科學人》網站，未經同意禁止轉載。）