AI 讀書團隊 - Claude AI team 開發 C Compiler : Rust 能在 compile time 時檢查出 Data Race , 而 Kotlin 做不到?

前篇：AI 讀書小組 - 和 AI 組隊一起讀書 - 2026.2.19

( 圖 by ChatGPT )

===

心得 ： 

這個 AI 學習小組, 遠超乎我的想像!

孤陰不長，獨陽不生;

團隊除了驗證者 Verifier 之外, 有個 總愛批評吐槽的 Critics , 能幫助團隊, 再上一層樓;

Claude Sonnet 4.6 令人驚艷, 狠起來連自己寫的都噴！

而 Synthesizer 的 昇華與湧現, 人的創意＋頭腦風暴 也不見得能匹敵

加上 Coordinator 的 秒級別 的 規劃決斷力, 難怪 OpenAI 的 CEO Sam Altam 也想讓位

天才之國，著實可怕！

把資料中心放到太空, 再做個太空電梯回到地面, 這不就是巴別塔嗎？

似乎有些能體會, 為何 Claude 的安全研究員 夏爾馬 要離職了... 

===

在和 Grok AI 組學習小組閱讀 這篇時：

 https://www.anthropic.com/engineering/building-c-compiler

看到一句：“I tasked 16 agents with writing a Rust-based C compiler”

好奇為何選擇用 Rust ; 詢問了 Grok AI, 回答很棒如下; 

想到這也是一篇文章, 於是選用號稱吐槽有名的 Claude, 再開一個學習小組,

來閱讀這篇看看^^

== Grok AI 回答文章 ==

=== 文章結束 ===

我是用 Perplexity Pro (台灣大哥大去年六月免費贈送一年）

+ 剛上線的 Claude Sonnet 4.6 

1. 載入 AGENDS.md

2. 文章餵入後, Coordinator 的規劃令我驚艷, 看來 Sam Altman 說 AI 可以當 CEO 可能不是開玩笑 ^^

接著 Explainer 解說 ：

PS: mermaid 圖在 Github 上, 應該可以渲染？

當然看書最重要是自己 (人）能吸收, 否則也只是轉貼複製;

於是繼續問 AI 

Explainer : 請介紹 Rust 的 borrow checker, 說明為何能在 compile time 解決 Data race 的問題？ kotlin 在語言定義上, 本質上就沒辦法做到嗎?

執行緒安全 - 維基百科

本來這網誌想寫 “Claude 16 AI Agents 開發 C Compiler, 為何選擇用 Rust 語言來開發, 而非 Kotlin ? ” 看到 Claude AI 的回答, 又用這開啟新的讀書討論串 ^^ ...

Coordinator : 

--- 

Verifier : 

Claude 不虧是吐槽大王,  Verifier 自己就開始指正自己了...

---

Critic 更是犀利！還會主動找 Affirmer 和他對話！

--

Synthesizer 

這昇華與湧現太令我驚艷了！ 

人的團隊腦力激盪（頭腦風暴）brainstorming 都不見得能有這結果

===

===

Writer 的整理寫作能力, 比我強太多了...

一個關於型別系統哲學的故事

---

記憶體，是被所有執行緒共享的公地。

當多個執行緒同時爭奪這塊公地——一邊讀、一邊寫、誰也不等誰——就會發生 Data Race：程式不崩潰，但資料已悄悄損壞；測試可能通過，但在生產環境的某個深夜，它突然出現了。

這類 bug 惡名昭彰，難以重現、難以定位，是並發程式設計的頭號惡夢。

Rust 的答案令人驚訝：讓這種 bug 從一開始就無法被編譯出來。

不是執行期偵測，不是 linter 警告——是編譯失敗。

Kotlin 則做不到這一點。但這不是 Kotlin 工程師不夠努力，而是兩種語言在設計之初，就走上了完全不同的路。

---

什麼是 Data Race？

在深入之前，先對齊定義。Data race 的發生需要同時滿足三個條件 ：

1. 兩個以上的執行緒同時存取同一塊記憶體
2. 其中至少一個是寫入操作
3. 沒有任何同步機制（mutex、atomic 等）保護

三個條件缺一不可。這意味著：只要能在語言層面從結構上保證這三個條件不會同時成立，data race 就不可能發生——Rust 正是這樣做的。

---

Rust 的答案：三條鐵律

Rust 的編譯器中有一個叫做 Borrow Checker 的靜態分析模組，它在程式碼被編譯的那一刻，強制執行三條規則 ：

規則	內容	消滅的問題
Rule 1：唯一可變	同一作用域內，同一資料只能有一個 &mut	防止多處同時寫入
Rule 2：共享不可變	有多個 & 時，不得同時存在 &mut	確保讀取期間沒有人在寫
Rule 3：Lifetime 界定	所有 reference 的存活時間不得超過資料的擁有者	消滅 use-after-free

Rule 1 + Rule 2 合起來，從邏輯上封死了 data race 的發生條件：「有人在寫」和「有人在讀或寫」這兩件事，在 safe Rust 中永遠不會同時成立。

來看一個具體例子 ：

fn main() {
    let mut data = vec![1, 2, 3];

    let r1 = &data;       // ✅ immutable borrow
    let r2 = &data;       // ✅ 多個 immutable borrow 可以共存
    // let w = &mut data; // ❌ 編譯>錯誤！r1, r2 還活著，不能同時有 &mut

    println!("{:?} {:?}", r1, r2);
    // r1, r2 在這裡結束生命週期

    let w = &mut data;    // ✅ 現在可以了，
因為 r1, r2 已結束
}

這不是執行期的檢查，是 rustc 的靜態分析，沒有任何 runtime overhead 。違規的程式碼在你按下 build 的那一刻就被拒絕，還會附上明確的錯誤訊息告訴你衝突在哪裡。

---

這不是工程師的魔法，而是數學

很多人以為 borrow checker 是 Rust 工程師發明的聰明黑魔法，但它其實有嚴格的數學理論根基。

Rust 的 ownership 模型本質上是 Affine Type System（仿射型別系統），源自邏輯學家 Jean-Yves Girard 在 1987 年提出的 Linear Logic（線性邏輯）。這個理論研究的核心問題是：資源（resource）應該被使用幾次？

型別系統	規則	代表語言
Linear Types	資源必須使用恰好一次	Haskell（GHC Linear Types）
Affine Types	資源最多使用一次（可以丟棄）	Rust
無限制引用	資源可使用任意多次	Kotlin、Java、Python

Rust 選擇 Affine 而非嚴格 Linear，是為了允許 drop（丟棄值而不使用），讓語言保持實用性 。這個數學結構從根本上保證了：在型別系統層面，一個 mutable reference 不可能有分身，於是 data race 的前提條件在型別層就被消滅了。

---

Kotlin 為何做不到？

這裡要先給一個公道的說法：不是 Kotlin 不努力，而是 GC 設計從根本上決定了它的上限 。

問題根源：Aliasing

Kotlin 依賴 JVM 的 Garbage Collector 管理記憶體。GC 的存在前提是：多個 reference 可以同時指向同一個物件（aliasing），讓 GC 追蹤誰還在用它。

但這個前提，恰好是 affine type 系統的對立面。

// Kotlin：完全合法的程式碼，但潛藏 data race
val data = mutableListOf(1, 2, 3)
val alias1 = data  // ← 指向同一個 list
val alias2 = data  // ← 也指向同一個 list

// Thread A 透過 alias1 寫入，Thread B 透
過 alias2 讀取
// Kotlin 編譯器不知道 alias1 和 alias2 >是同一個物件
// → data race，但編譯成功 💥

Kotlin 的編譯器看到 alias1 和 alias2，無從得知它們指向同一塊記憶體。沒有 aliasing 追蹤，就無法做出「有人在寫，所以現在不能讀」的靜態保證 。

Kotlin 的應對方式

這不代表 Kotlin 對 data race 束手無策，只是它的防線在不同的地方 ：

• 開發者手動加鎖：使用 Mutex、Atomic、limitedParallelism
• 執行期工具：Google 在生產環境使用 ThreadSanitizer（TSAN）在 test runtime 偵測 race condition
• 靜態分析工具：Google 已開發基於 heuristics 的 Kotlin static analysis，可在 compile time 偵測部分 racy pattern

關鍵差異在於：Kotlin 的這些防護都依賴開發者紀律或外部工具，而不是語言本身的強制保證。你寫了有 race 的程式碼，Kotlin 編譯器不會攔你。

---

一個必要的誠實補充：unsafe 的存在

說 Rust 保證無 data race，需要加上一個重要的限定語：這個保證只在 safe Rust 的範圍內成立 。

Rust 提供 unsafe block，允許開發者繞過 borrow checker，直接操作裸指標、呼叫 FFI、使用 UnsafeCell。在 unsafe 中，data race 是可能發生的——Rust 官方 Reference 明確將其列為 Undefined Behavior。

// 在 unsafe 中，開發者自己負責安全性
unsafe {
    // 這裡的記憶體操作不受 borrow checker 保護
    *raw_ptr = 42;
}

好消息是：unsafe 在現實的 Rust codebase 中使用率極低，通常集中在底層函式庫，而非業務邏輯層 。大多數應用層程式碼完全活在 safe Rust 的保護罩之下。

---

更大的設計哲學

這整件事背後，有一個值得深思的設計哲學差異：

Rust 選擇讓非法狀態在型別系統中無法被表達。 Kotlin 選擇讓非法狀態在執行期被偵測或由開發者預防。

沒有絕對的對錯，只有不同的取捨。Rust 的代價是更陡的學習曲線，以及 borrow checker 偶爾拒絕合法程式碼的摩擦感 。Kotlin 的代價是並發安全永遠是「開發者責任」而非「語言責任」。

用一個簡單的類比來說：Rust 像是把「禁止同時讀寫同一份文件」寫進了辦公室的建築結構——物理上就是做不到；Kotlin 像是貼了一張告示牌——規則在那裡，但沒有東西阻止你無視它。

---

語言光譜

這不是非黑即白的問題。各語言在「並發安全強制程度」上，形成一個連續光譜 ：

強制程度（低） ←————————————————————→ 強制程度（高）
  C/C++    Python   Kotlin/Java   Go   Rust (safe)   SPARK/Ada
  完全自理    GIL鎖      手動加鎖       channel    編譯器保證      形式驗證

Rust 在主流語言中，站在最靠近「編譯器強制保證」的那一端，但它不是終點——SPARK 和 Idris 等語言用形式驗證走得更遠，代價是更高的使用門檻。

---

一句話總結

Rust 能在 compile time 抓出 data race，是因為它的型別系統（Affine Type System）從數學層面保證「可變 reference 不能有分身」，讓 data race 的前提條件在靜態分析時就不可能成立。Kotlin 做不到，是因為 GC 的設計允許 aliasing 存在，而沒有 aliasing 追蹤，語言就無法在編譯期做出「無 data race」的完整保證——不是 Kotlin 不努力，是 GC 決定了它的型別系統上限。

---

參考資料：Rust Borrow Checker Explained · Introducing the Borrow Checker — LogRocket · Prevent Race Conditions in Coroutines — Dave Leeds · Behavior Considered Undefined — Rust Reference · From Linear Types to Rust — YouTube

---

---

PS:  Aliasing（別名）：兩個或更多的變數名稱，指向記憶體中同一個物件。