2015-Rust與線性型別#

案件摘要#

2015 年 5 月，Mozilla 發布 Rust 1.0——這樁案件的核心創新是 ownership/borrowing 系統，一個在編譯期追蹤資源、無需 GC 的記憶體安全方案。Graydon Hoare 於 2006 年私下啟動 Rust 專案，2010 年獲 Mozilla 支援，歷經九年終於結案。案發背景是雙重夾擊：C/C++ 的記憶體安全噩夢（Microsoft 統計約 70% 的嚴重安全漏洞是記憶體錯誤），以及 GC 語言（Java/Go）的 runtime 開銷不適合系統程式。破案線索來自學界：Haskell 的線性型別研究（Wadler 1990 linear types）早已證明「編譯期追蹤資源」可行。Rust 把線性型別 λ-Calculus 變成了工程變體——每個值恰好一個 owner，賦值即移動。這是 λ-Calculus 的資源分支（substructural logic）首次大規模落地。

前因 -- 為什麼會有這個案子#

C/C++ 的記憶體安全噩夢：use-after-free、double-free、buffer overflow 泛濫；Microsoft 統計約 70% 的嚴重安全漏洞源自記憶體錯誤。
GC 語言（Java/Go）以垃圾回收換取安全，但 runtime 開銷（暫停、記憶體占用）使它們不適合作業系統、瀏覽器引擎等系統程式。
C++ 的 RAII（Resource Acquisition Is Initialization）用解構函式管理資源，正確但全靠人工紀律，編譯器不檢查。
學界線索：Wadler（1990）的線性型別證明——若型別系統要求「每個變數恰好使用一次」，即可在編譯期追蹤資源；Tofte-Talpin（1994）的 region inference 證明壽命可被自動推導。
Hoare 的自述：Rust 源於對「安全與效能不可兼得」這一公理的不服——他要證明兩者可兼得。

線索與推理 -- 數學式、程式、理論#

線索一：ownership 規則與 move semantics#

Rust 的 ownership 三規則：

每個值恰好有一個 owner；
同一時刻只能有一個可變借用或多個不可變借用；
owner 離開作用域，值被釋放（RAII 的型別化）。

關鍵在賦值即移動（move semantics）。這是線性型別 λ-Calculus 的工程變體：在線性邏輯中，每個變數恰好使用一次：

\[ x : A \vdash e : B \quad \text{且 } x \text{ 恰好出現一次} \]

若 \(A\) 是非 Copy 型別（如 String），則賦值後原變數「失效」——資源的所有權被轉移而非複製： \(\text{let } y = x; \Rightarrow x\) 已消耗。

這讓「use-after-free」在編譯期就成為型別錯誤——這是破案的第一根支柱。

線索二：borrowing 與 borrow checker#

每次使用都轉移所有權太嚴格，於是 Rust 加入借用（borrowing）：

&T：共享借用（shared），可同時存在多個；
&mut T：可變借用（exclusive），全程序同一時刻至多一個。

互斥規則由編譯器的 borrow checker 靜態檢查：

\[ (\exists^{\geq 1} \ \&T) \Rightarrow \nexists \ \&\text{mut} \ T \quad ; \quad \exists \ \&\text{mut} \ T \Rightarrow \nexists \ \text{任何其他借用} \]

讀者與寫者的互斥在編譯期解決——資料競態（data race）與 iterator invalidation 成為編譯錯誤而非 runtime 噩夢。這是破案的第二根支柱。

線索三：lifetime 與 region inference 的血緣#

借用能活多久？Rust 用壽命標註（lifetime annotation）與推導回答。這與 Tofte-Talpin 的 region inference 同源：每個引用的壽命是它所指向的 region 的血緣——引用絕不能活得比資料本身久：

\[ \text{borrow}(r, \ 'a) \quad \text{且} \quad 'a \subseteq \text{region}(r) \ \Rightarrow \ \text{安全} \]

編譯器沿函數呼叫與作用域的血緣圖推導每個 'a，無需 GC 即知資料何時可釋放。這是破案的第三根支柱。

線索四：Result/Option monad 與 ? 運算子#

Rust 沒有 null 與例外，錯誤處理用型別：

Option<T> = Some(T) | None：可能缺席；
Result<T, E> = Ok(T) | Err(E)：可能失敗。

? 運算子是 monad bind 的語法糖：失敗即提前返回：

\[ \text{let } y = f()?; \quad \equiv \quad \text{match } f() \{ \text{Ok}(v) \Rightarrow v, \ \text{Err}(e) \Rightarrow \text{return Err}(e) \} \]

這是 Maybe monad 的工程變體：錯誤路徑被寫進型別簽名，不可能忘記處理。

破案時刻：可執行程式碼示範#

以下 Rust 程式展示 move semantics、borrow checker 拒絕的程式（註解保留），以及 Result + ? 鏈。可用 rustc 編譯執行：

#[derive(Debug)]
struct Report { title: String }

fn analyze(r: &Report) -> usize { r.title.len() }   // 共享借用
fn finish(r: Report) -> String { format!("done: {}", r.title) } // 取得所有權

fn parse(s: &str) -> Result<Report, String> {
    if s.is_empty() { Err(String::from("empty input")) }
    else { Ok(Report { title: s.to_string() }) }
}

fn main() {
    // 1) move semantics：賦值即移動
    let a = Report { title: String::from("case-42") };
    let b = a;                       // a 的所有權移給 b
    // println!("{:?}", a);          // 編譯錯誤：value borrowed here after move
    println!("{:?}", b);

    // 2) borrowing：多個 &T 共存，但 &mut 互斥
    let r = Report { title: String::from("borrow-me") };
    let r1 = &r;
    let r2 = &r;                     // 兩個共享借用：OK
    println!("{} {}", analyze(r1), analyze(r2));
    // let m = &mut r.title;         // 編譯錯誤：cannot borrow as mutable
    //                               //   while borrowed as immutable

    // 3) Result + ? 鏈：失敗即提前返回（main 含 ? 時須改為 -> Result 簽名，見下方 run()）
}

fn run() -> Result<(), String> {
    let report = parse("linear-types")?;   // Err 時 run 提前返回 Err
    let summary = finish(report);          // 所有權進入 finish
    println!("{}", summary);
    let bad = parse("")?;                  // Err("empty input")：提前返回
    let _ = bad;
    Ok(())
}

（main 中含 ? 時須將簽名改為 fn main() -> Result<(), String>；改用 run() 可獨立驗證 ? 鏈。）

註解中的兩行若解開，編譯器立即拒絕——memory safety 不靠 runtime，靠型別系統。這是破案證據：線性型別理論四十五年後首次在系統程式語言中完全落地。

結案 -- 後果與影響#

Rust 成為系統程式的函數式類型革命：無 GC 且記憶體安全，證明安全與效能可兼得。
Rust 連續多年（2016-2024）獲 Stack Overflow 開發者調查「最受喜愛語言」。
Linux kernel 自 2022 年（6.1 起）正式支援 Rust 編寫核心模組；Windows 內核部分元件（如 win32k 附近的驅動）開始以 Rust 重寫。
線性型別理論（λ-Calculus 的資源分支，substructural logic）首次大規模工業落地——Girard 的線性邏輯（1987）與 Wadler 的線性型別（1990）從學術走進作業系統。
「編譯期資源管理」證明函數式類型論可以取代 GC：RAII 的型別化 + borrow checker = 免 runtime 的記憶體安全。
borrow checker 的「所有權 + 借用」模型啟發了後續語言設計（如 Swift 的 ARC 演化、 Mojo、Zig 的對照路線）。

關鍵人物與文獻（條例，含真實文獻書目）#

Graydon Hoare：Rust 創始人，2006 年啟動專案，2010 年帶入 Mozilla；Niko Matsakis、Aaron Turon、Felix Klock 為 ownership 規則的核心設計者（Mozilla Research）。
Wadler, P. (1990). Linear types can change the world!. In Programming Concepts and Methods (IFIP TC 2/WG 2.2 Working Conference), 347-359.
Girard, J.-Y. (1987). Linear Logic. Theoretical Computer Science, 50(1), 1-101.
Tofte, M., & Talpin, J.-P. (1994). Implementation of the Typed Call-by-Value λ-Calculus Using a Stack of Regions. Proceedings of POPL '94, 188-201.
Matsakis, N. D., & Klock, F. S. (2014). The Rust Language. ACM SIGAda Ada Letters, 34(3), 103-104.
Jung, R., et al. (2017). RustBelt: Securing the Foundations of the Rust Programming Language. Proceedings of POPL 2018.