最佳的執行時期檢查是永遠不會執行的檢查。
POSIX Socket API 是一個狀態機。Socket 必須先被建立，然後繫結，接著設定為監聽狀態，才能接受連線。以錯誤的順序呼叫操作——在未連線的 Socket 上傳送資料、在監聽前接受連線、重複關閉——會在 C 語言中返回一個錯誤碼，但沒有任何機制能強制你檢查它。
每個生產環境的 Socket 函式庫都透過以下三種方式之一來處理這個問題：
執行時期檢查——在每次呼叫時斷言狀態，違規時拋出例外（Python、Java、Go）。
文件說明——信任程式設計師會閱讀 man page（C、Rust）。
忽略它——讓作業系統返回 EBADF，並希望有人檢查回傳碼。
這三種方法都會將錯誤推遲到執行時期。Lean 4 提供第四種選擇：讓錯誤在型別層級上無法表示，然後在編譯時期抹除證明， so 產生的程式碼與原始 C 程式碼完全相同。
五個狀態、七個轉換和一個證明義務。這就是整個 POSIX Socket 協定。讓我們來編碼它。
DecidableEq 讓我們免費獲得 by decide——編譯器可以在沒有任何使用者努力的情況下證明任何兩個具體狀態是不同的。
狀態參數僅存在於型別層級。它在執行時期被抹除：一個 `Socket.fresh` 和一個 `Socket.connected` 具有完全相同的記憶體佈局（指向作業系統檔案描述子的單一指標）。零額外開銷。
建構子被保護起來，以防止隨意的狀態偽造。
Lean 4 的核心將這些約束貫穿整個程式。如果你寫 `send freshSocket data`，核心會看到 `Socket.fresh` 而不是預期的 `Socket.connected`，並回報型別錯誤。沒有執行時期檢查。沒有斷言。沒有例外。產生的程式碼中沒有分支。
這就是依賴型別最閃耀的地方。第二個參數是一個證明，證明 Socket 還沒有被關閉。讓我們追蹤每個具體狀態的處理方式：
對於前四種狀態，預設的 `by decide` 策略會自動解除證明——呼叫者無需編寫任何內容。對於第五種狀態，命題 `.closed ≠ .closed` 在邏輯上是錯誤的：不存在任何證明，因此程式會在編譯時期被拒絕。
證明在編譯過程中被抹除。產生的 C 程式碼是：
沒有分支。沒有標誌。沒有狀態欄位。證明在型別檢查期間完成了它的工作並消失了。
我們也證明所有五個狀態都是成對不同的：
這些可以透過 `decide` (核心評估 `BEq` 實例) 輕鬆證明。它們的存在是為了讓下游程式碼能夠將它們用作引理，而無需重新證明其相異性。
在 Lean 4 Playground 中開啟此範例——嘗試取消註解失敗的範例，以即時查看型別錯誤。
取消註解 `bad_double_close` 或 `bad_send_fresh`，核心會立即拒絕程式——錯誤訊息會精確告訴你哪個狀態轉換是無效的。
這個狀態機模擬了程式設計協定——你呼叫了哪些操作——而不是 Socket 的作業系統層級狀態。真實世界更為複雜：
非同步的 `connect` 在 TCP 握手進行中時會返回 `EINPROGRESS`。Socket 既不是 `.fresh` 也不是 `.connected`——它正在連接中。一個真正的非同步 API 需要一個 `.connecting` 狀態和一個解析步驟（`pollConnect`）。
對方的斷線可能隨時發生。一個 `Socket.connected` 可能在底層被破壞；你只會在 `send`/`recv` 返回錯誤時才發現。型別保證了呼叫是合法的嘗試，而不是它一定會成功——這就是 IO 所編碼的。
透過 `shutdown(SHUT_WR)` 進行的半關閉會使 Socket 可讀但不可寫。五狀態模型無法表達這一點。
總之，型別層級的狀態機對於正常路徑上的同步 Socket 是健全的。對於生產環境的非同步伺服器，則需要更豐富的狀態和基於 IO 的解析協定——這是未來文章的主題。
Lean 4 是獨一無二的：證明義務 `state ≠ .closed` 是一個真實的邏輯命題，核心會驗證它。它不是一個 lint，不是一個靜態分析啟發式方法，也不是一個約定。它是一個協定相容性的數學證明，由驗證 Mathlib 定理的相同核心檢查——然後被丟棄， so 產生的程式碼以 C 的速度運行。
這篇文章是關於 Hale 系列的一部分——Hale 是 Haskell 的 Web 生態系統移植到 Lean 4，具有最大主義的型別。