1986 年 HOL 系統：為晶片請來數學保鏢的探案#
報案人：Mike Gordon（劍橋大學電腦實驗室）。 委託人：英國皇家信號與雷達署（RSRE），涉案晶片 VIPER。 兇器：Church 簡單型別＋LCF 可信核心。
案發現場#
1980 年代初，微處理器開始進入軍用與關鍵系統。 一顆晶片若有邏輯錯誤，召回成本是天文數字，軍用後果更不堪設想。 傳統模擬測試只能測「走過的路」，測不到「沒走過的路」。
Gordon 在劍橋研究語義學，RSRE 找上門：能否用數學證明 VIPER 微處理器正確？ 當時的 Boyer-Moore 只懂一階 Lisp，Prolog 不完備， LCF 雖有可信核心卻綁在特定邏輯上。
現場的三個需求：
- 邏輯要夠強，能講硬體的位元、時間、算術與高階規格。
- 證明器要可信，不能「證出」假的硬體正確性。
- 要能分層驗證：閘→ALU→微碼→指令集，每層都是下一層的規格。
Gordon 的回答是 HOL：Higher Order Logic 定理證明器，1986 年前後成形。
偵查過程#
線索一：Church 簡單型別——安全的強大#
Gordon 選了 1940 年 Church 的簡單型別理論 \(\lambda\) 演算＋高階邏輯。 一切項都有型別， \(bool\) 為命題型， \(ind\) 為個體型， 函數型寫為 \(\sigma \to \tau\) ，謂詞即 \(P : \sigma \to bool\) 。
核心公理極簡：
加上選擇公理 \(Hilbert \, \epsilon\) 。全邏輯建在幾條公理上， 其餘的集合、數、串列皆由保守定義擴充，絕不動搖一致性。
| 型別 | 例子 | 用途 |
|---|---|---|
| \(bool\) | \(true\) 、 \(false\) | 命題與規格 |
| \(num\) | \(0\) 、 \(SUC(n)\) | 地址與算術 |
| \(\sigma \, list\) | \([1; 2]\) | 微碼序列 |
| \(time \to bool\) | 波形謂詞 | 時序行為 |
| \((bool \times bool) \to bool\) | 與閘規格 | 閘級建模 |
高階量化允許 \(\forall P \, \exists C \, \dots\) 這類規格， 一階系統寫不出的歸納原理在此只是高階定理。
線索二：LCF 核心移植——小核心，大信任#
HOL 直接繼承 Milner 的 LCF 架構：抽象型別 \(thm\) ， 一切定理只能由 \(MP\) 、 \(GEN\) 、 \(BETA\) 等十來條原語產生。 ML 策略層在其上大興土木， \(tactic\) 與 \(tactical\) 照抄 LCF 詞彙。
REWRITE_TAC [ADD_CLAUSES] THEN INDUCT_TAC THEN ASM_REWRITE_TAC []
這行策略的意思是：先用加法子句重寫，再做歸納， 再用假設重寫子目標。錯了最多失敗，絕不造假。
Gordon 還立下規矩：定義即保守擴充。新常量必須是 \(\vdash c = t\) 形狀的顯式定義，新類型必須是舊類型的子集， 故邏輯一致性只依賴最初幾條公理。
線索三：VIPER——第一次硬體大案#
VIPER 是 RSRE 的 32 位元微處理器。Gordon 團隊把規格分三層：
- 頂層：指令集架構語義， \(Spec_{ISA}(impl, env)\) 。
- 中層：微碼狀態機，每條微指令為狀態轉移 \(Next(s, s')\) 。
- 底層：閘級網表， \(NAND\) 、 \(NOR\) 的布林行為。
驗證目標形如：
即實作的行為蘊含規格。團隊用 HOL 證出微碼層正確， 雖然後來發現規格本身有爭議，但「用高階邏輯驗晶片」 的可行性已被證實。此案直接催生工業界的硬體驗證傳統， 從 ARM 到 Intel 的浮點單元皆受其影響。
結案報告#
HOL 於 1986 年左右在劍橋定型，Gordon 的書《HOL System Description》成為經典。 它破了「軟體證明器能否驗硬體」的案件。
遺產有三：
- 硬體驗證正統：VIPER 案證明定理證明可進晶片廠，後來 HOL 驗浮點除法器成為標配。
- HOL 家族：HOL88→HOL90→HOL4→HOL Light，一脈相承； HOL Light 後來證完克卜勒猜想（Flyspeck），Isabelle／HOL 亦脫胎於此。
- 定義保守性原則：不隨意加公理、只做定義擴充，成為高可信證明的金律。
證據與工具#
- 外延公理： \((f = g) \leftrightarrow \forall x \, (f(x) = g(x))\) ， \(bool\) 僅 \(true\) 與 \(false\) 兩值。
- 與閘規格： \(AND(a, b, out) \equiv (out = (a \land b))\) ，時序擴充為 \(\forall t \, (out(t+1) = (a(t) \land b(t)))\) 。
- 分層蘊含： \(\vdash Impl \to Spec\) ，每層 \(Spec_{i+1}\) 為 \(Spec_i\) 的實作。
(* HOL 典型證明腳本 *)
g `!x. x + 0 = x`;;
e (INDUCT_TAC THEN ASM_REWRITE_TAC [ADD_CLAUSES]);;
- 實驗：用 HOL Light 或 Isabelle／HOL 定義 \(AND\) 與 \(OR\) 閘， 證明半加器的規格 \(sum = (a \oplus b)\) ，體會分層驗證的手感。
- 文獻：Gordon 1986 年〈Why Higher-Order Logic is a Good Formalism〉， Gordon 與 Melham《Introduction to HOL》。