"测试只能证明 bug 的存在，却永远无法证明 bug 的缺席。"
—— Edsger Dijkstra
最近读到一篇基于 OCaml 之父 Xavier Leroy 深度访谈的文章，标题叫《编程语言的"第三条道路"》[1]。
Leroy 是法国科学院院士、法兰西公学院教授，1996 年创造了 OCaml，2024 年拿下了 ACM SIGPLAN 编程语言软件奖。这场近 90 分钟的访谈横跨了函数式编程、形式化验证、内存管理和生成式 AI——几乎每个话题，都能直接映射到 C# 的处境上。
读完后我有个越来越强烈的感受：
这篇文章讲的是"第三条道路"，而 C# 是这条路上商业化最成功、却最少被这样叙述的语言。OCaml 证明了这条路可行，C# 证明了这条路能赢。
下面分五条线索，聊聊这篇访谈和 C# 之间的隔空对话。
Leroy 对 OCaml 的定位很有意思：
"OCaml 是一种优秀的函数式语言……但它同时也是一门相当不错的系统编程语言。"
纯函数式语言（Haskell、Coq）活在学术象牙塔里，系统语言（C、C++）活在工程泥潭里。OCaml 不站队，两头都要，靠这种"不媚俗"的混血活了 30 年[1:1]。
但说实话，这条混血路线走得最远的其实是 C#——只是它做得更隐蔽：
这里有个常被忽略的事实：F# 本身就是 OCaml 的直系兄弟（Don Syme 在微软剑桥研究院起家时，做的就是"OCaml for .NET"）。
所以 .NET 生态其实是混血双轨制——F# 保留了纯血 ML 的完整类型推断和不可变默认，C# 负责把这些特性"平民化"。
比如 var：C# 只做局部类型推断，在 API 边界强制显式标注。这恰好踩中了 Leroy 说的权衡——全局推断固然优雅，但大规模项目需要显式签名充当文档[1:2]。C# 没有追求完整的 Hindley-Milner 推断，不是不能，而是判断了对工程团队的阅读成本不划算。
这是 C# 一以贯之的设计哲学：不求理论上最纯，只求工程上最优。
访谈里 Leroy 抛出了一个反直觉的观点：
"手动内存管理并不总是更快。或者你需要是一位非常优秀的程序员才能让它总是更快。"
他的论据很实在：GC 语言的对象分配是指针递增式的 bump-allocation，接近 O(1)；共享结构不需要拷贝，而手动管理下"因为你不确定是不是唯一所有者，所以拷贝一份——但拷贝在时间和内存膨胀上都代价高昂"[1:3]。
Jane Street 的案例最耐人寻味：高频交易领域每一微秒都是钱，他们却选了带 GC 的 OCaml 而不是 Rust——因为人为错误的成本远高于 GC 开销。
面对"GC vs 手动"的站队题，C# 的回应比选边站更精明：
默认 GC，但系统性提供逃生舱。
Span<T> / Memory<T>：零分配地切片内存，不放弃 GC；stackalloc + ArrayPool：覆盖高频热路径；换句话说：OCaml 证明了"GC 语言可以做系统编程"，C#/.NET 则进一步证明了"GC 语言可以按需在单个函数尺度上做手动内存决策"。
这比 Rust 的全局所有权纪律更符合 Leroy 那套"组织经济学"逻辑——团队里不是每个人都需要精通生命周期，但热路径上的那个人手里有工具。
访谈里最生动的一段，是 Leroy 吐槽共享内存并发：
"共享内存并发就像你想和邻居交流，你破门而入，移动他们家的家具，等他们回来时会说'哦，有东西被移动了，大概是想告诉我什么'……也许你可以直接去见你的邻居？——这就是消息传递。"
他推崇的是 Erlang 风格的 Actor 模型[1:4]。
有意思的是，C# 主线走的是 async/await + 共享状态的老路，但 Orleans 的 Virtual Actor Model 就是 .NET 世界对消息传递的完整回答：grain 之间不可共享状态、只能收发消息，单机到集群共用同一套心智模型。
再加上：
System.Threading.Channels：标准的 CSP 管道；C# 其实是把三种并发范式都摆上了货架。
这里有个颇具讽刺意味的对照：OCaml 5 为了 Jane Street 的需求在共享内存上做了妥协，而 C# 这个"共享内存出身"的语言，反而把 Actor 模型做成了工业级产品。
文章里有一张三种形式化方法的对比表[1:5]：
| 方法 | 自动化程度 | 成本比（vs 写代码） | 典型工具 |
|---|---|---|---|
| 类型系统 | 全自动 | 0.1x | OCaml / TypeScript |
| 静态分析 | 全自动 | 0.5x | Infer, Astrée |
| 程序证明 | 交互式 | 10–50x | CompCert, seL4, Lean |
C# 在"10–50x"那层基本缺席（Spec# 和 Code Contracts 都死在了沙滩上），但在 0.1x–0.5x 区间做到了极致：
可空引用类型（C# 8+）
本质上是把"十亿美元错误"变成编译期流分析问题。不用写一行证明，编译器替你盯着每一个可能为 null 的路径——这是向验证迈出的最实用一步。
Roslyn 编译器平台
Analyzer 和 Source Generator 让每个团队都能低成本编写自己的静态验证规则。等于把"静态分析"这一层民主化了。
Dafny
微软研究院真正做程序证明的语言，可以把 C# 作为编译目标之一。重验证的路线，微软也没完全放弃。
Leroy 花了大半辈子在 CompCert 上——一个携带数学证明、保证"编译器不会引入源程序中不存在的 bug"的 C 编译器，2026 年 3 月还帮空客 ATR 42/72 的航电系统拿下了 DO-178C 认证[1:6]。
C# 走不了这条路，也不需要走。它的策略是：把验证的成本压到接近于零，让 99% 的普通项目也用得起。
访谈最尖锐的部分是关于 LLM 的。Leroy 作为 OCaml 维护者，吐槽非常直接：
"我们收到了很多明显由 AI 生成的 issue。10 份报告里可能只有 1 份是好的。每份报告都有好几页——详细的解释、复现步骤——但最终什么也复现不了。"
"对我来说，每一行新代码都是负债。我不想要海量代码，我要的是 50 行经过多年打磨的代码。"[1:7]
他的核心警告是：AI 降低了"写代码"的成本，但没有（甚至提高了）"验证正确性"的成本。 程序员从"写代码者"变成"代码审查者"，工作并没有变轻松，只是从一种认知负荷切换到另一种[1:8]。
在这个语境下，C# 的位置其实相当好：
第一，强静态类型 + nullable 流分析 + 全套 Analyzer，构成了一道机器可自动检查的质量门槛。 AI 生成的 slop，在编译器这一关就会被过滤掉一大半。
第二，Roslyn 是 compiler-as-a-service。 Agent 可以程序化地调用编译、拿到结构化诊断、再迭代修正——C# 大概是主流语言里最适合做"LLM 生成 → 编译器反馈 → 自动修正"闭环的之一。
第三，Leroy 的愿景是"AI 生成代码的同时生成一份 Lean/Coq 证明"。 离 C# 最近的现实版是：AI 生成代码，同时生成 analyzer 规则和属性测试（Property-Based Testing）。证明不必是数学形式的，可执行的规约也是证明。
顺便说一句 DDD：C# 的 records、不可变值对象、模式匹配做领域建模已经很顺手，但真正完整的"用类型让非法状态不可表示"还得看 F# 的路数（Scott Wlaschin 的 Domain Modeling Made Functional 就是这套思路）。做领域对象投影、工作流 DAG 这类强结构化场景，F# 的判别联合 + 编译期完备性检查，比 C# 的 class 层级更贴合"建模即验证"。
访谈结尾，Leroy 说了一段让我印象很深的话：
"写出代码从来不是终点。理解代码为什么正确，才是真正的编程能力。"
一个学术语言的守护者，用三十年证明"可靠性与工程实用可以共存"。
而 C# 用另一种方式回应了同样的命题：不必要求每个开发者都成为证明专家，而是把验证、内存安全、类型纪律，一层层织进语言和平台的基础设施里，让正确的代码成为默认路径。
OCaml 是第三条道路的宣言，C# 是第三条道路的基建。
Dijkstra 那句话放在今天依然紧迫：我们应该用自己完全理解的程序，去解决未知世界的问题——而不是反之。
只不过在 2026 年，帮你"理解程序"的，除了你的大脑，还多了一个编译器，和一个永远在生成"差不多正确"代码的 AI。
选一门能让编译器替你吵架的语言，可能是这个时代最务实的浪漫。
本文基于 Xavier Leroy 在 The Peterman Podcast（2026 年 7 月）访谈的解读文章展开，部分观点为作者延伸。
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。