1977 年 LCF 與 ML：可信核心的誕生探案#

報案人：Robin Milner（愛丁堡，後赴史丹佛與劍橋）。

案發現場#

1970 年代的定理證明器有個致命傷：證明器本身是幾萬行程式，誰能保證沒有 bug？ Boyer-Moore 用 Lisp 寫證明器，搜尋策略與邏輯糾纏在一起，錯一行就可能「證出」假定理。

Milner 在史丹佛研究 Scott 的計算理論 Logic for Computable Functions（LCF），想把證明器建立在堅實基礎上。現場的三個難題是：

1977 年左右，Milner 交出答案：LCF 架構＋ML 語言。 HOL、Isabelle、Coq 皆繼承此架構，影響延續至今。

Milner 的神來一筆是借用抽象資料型別。系統中宣告一個型別 \(thm\) ，它只能由少數幾個「公理與推理規則」構造出來：

\[ \frac{}{\vdash A \quad (A 為公理)} \quad \frac{\vdash A \quad \vdash A \to B}{\vdash B} \]

在 ML 中寫為：

abstype thm = Thm of formula
  with
    val axiom : formula -> thm
    val modus_ponens : thm * thm -> thm
    val gen : var -> thm -> thm
end

使用者可以在 \(thm\) 之外寫任意程式，即使寫錯也造不出假的 \(thm\) 值，因為唯一能產生 \(thm\) 的函數就是那幾個可信原語。這就是可信核心（trusted kernel）：小到可審查，強到撐起一切。

為了寫證明策略，Milner 發明了 ML（Meta Language）。它有三件利器：

一個 \(tactic\) 把目標 \(G\) 化為子目標 \(G_1\) 與 \(G_2\) ，一個 \(tactical\) 把小策略組合成大策略，例如 \(THEN\) 、 \(ORELSE\) 、 \(REPEAT\) ：

\[ TACTIC_1 \, THEN \, TACTIC_2 \quad,\quad REPEAT(TAC) \quad,\quad TAC_1 \, ORELSE \, TAC_2 \]

例如證明 \(A \land B\) 的策略是先拆合取消去，再分別證明 \(A\) 與 \(B\) ：

let prove_conj = CONJ_TAC THENL [prove_A; prove_B]

策略語言與物件邏輯徹底分離：錯的策略最多證明失敗，絕不會證明出假定理。

LCF 本是為 Scott 的 LCF 邏輯打造，但架構一出，人人仿效：

一句话：現代證明器都是「小核心＋大策略層」的兩層建築，圖紙正是 Milner 在 1977 年畫下的。

LCF 破了「誰來證明證明器」的後設案件。它沒有讓證明器一次就全自動，而是讓人類寫高階策略、機器執行低階細節，且一切结果都經核心封印認證。

遺產有三：

可信核心原則：今天審查 Coq、Lean、Isabelle，第一件事就是看核心有多小。
ML 語言家族：Standard ML、OCaml、F# 皆源於此，函數式程式因此發揚光大。
tactics 範式： \(tactic\) 與 \(tactical\) 的詞彙成為全行業通用語，從 Coq 的 \(Ltac\) 到 Lean 的 \(tactic\) 框架皆是回聲。

Milner 因此獲 1991 年圖靈獎。

核心三公設： \(thm\) 只能由公理與原語構造，任何 \(tactic\) 失敗只回傳失敗而非假 \(thm\) ，核心程式碼行數即信任成本。
\(tactic\) 簽名： \(tactic : goal \to ((goal \, list) \times (thm \, list \to thm))\) ，前者是子目標，後者是正當性函數。
最小模擬（概念 Python）：

class Thm:
    def __init__(self, f): self.f = f  # 私有構造，外界禁調
def modus_ponens(th1, th2):
    # 僅當 th2 為 th1.f -> X 形狀才放行
    return Thm(conclusion)