《程式與數學的雙向鏡：從柯里-霍華德同構、類型論到形式化驗證》#
The Two-Way Mirror of Computation and Mathematics
本書的主張：現代高階程式設計，本質上就是一門在電腦上執行的、活生生的數學。
打破「寫 code 的人不懂數學、搞數學的人不會寫 code」的二分法：Lambda 演算與證明同構、型別系統對邏輯的具體實現、Lean 等工具讓電腦檢驗數學。
前言#
- 前言 — 0.1 雙向鏡的誕生 / 0.2 計算與證明的邊界消融 / 0.3 閱讀地圖
第一篇：邏輯的機械化——計算與證明的同構#
- 第1章-命題與證明的起源：從傳統邏輯到形式系統
- 第2章-蘭布達演算：計算的純粹化學式
- 第3章-柯里-霍華德同構：世紀的對決與交融
第二篇：型別的代數——結構化資料與泛函基石#
- 第4章-型別系統的數學本質
- 第5章-代數資料類型（Algebraic Data Types, ADT）
- 第6章-多型性與高階邏輯
第三篇：範疇論的代碼化——程式設計的宏觀架構#
- 第7章-程式設計師的範疇論入門
- 第8章-單子（Monad）：副作用的數學駕馭
- 第9章-極限、餘極限與資料結構的統一
第四篇：機器與數學的未來——形式化驗證#
- 第10章-當電腦成為數學裁判
- 第11章-在 Lean 中寫數學
- 第12章-軟體正確性保證：代數與驗證的工業級應用
第五篇：計算數學的深度交叉#
- 第13章-演算法的代數幾何與符號計算
附錄#
- 附錄 A：從數學符號到程式碼語法對照表（ \(\forall, \exists, \to, \times, +\) 與 Haskell/Lean 語法）
- 附錄 B：範疇論名詞在泛函編程中的中英對照字典
- 附錄 C：Lean / Haskell 基礎小範例速查
本書寫作核心觀點#
本書的靈魂在於打破「寫 code 的人不懂數學、搞數學的人不會寫 code」的二分法。透過展示 Lambda 演算與證明的同構、型別系統對邏輯的具體實現，以及 Lean 等工具如何讓電腦檢驗數學，讀者將會明白：現代高階程式設計，本質上就是一門在電腦上執行的、活生生的數學。