编程语言的「第三条道路」上，走得最远的其实是 C#

"测试只能证明 bug 的存在，却永远无法证明 bug 的缺席。"

—— Edsger Dijkstra

写在前面

最近读到一篇基于 OCaml 之父 Xavier Leroy 深度访谈的文章，标题叫《编程语言的"第三条道路"》。

Leroy 是法国科学院院士、法兰西公学院教授，1996 年创造了 OCaml，2024 年拿下了 ACM SIGPLAN 编程语言软件奖。这场近 90 分钟的访谈横跨了函数式编程、形式化验证、内存管理和生成式 AI——几乎每个话题，都能直接映射到 C# 的处境上。

读完后我有个越来越强烈的感受：

这篇文章讲的是"第三条道路"，而 C# 是这条路上商业化最成功、却最少被这样叙述的语言。OCaml 证明了这条路可行，C# 证明了这条路能赢。

下面分五条线索，聊聊这篇访谈和 C# 之间的隔空对话。

一、混血语言：C# 才是「又纯又脏」路线的商业冠军

Leroy 对 OCaml 的定位很有意思：

"OCaml 是一种优秀的函数式语言……但它同时也是一门相当不错的系统编程语言。"

纯函数式语言（Haskell、Coq）活在学术象牙塔里，系统语言（C、C++）活在工程泥潭里。OCaml 不站队，两头都要，靠这种"不媚俗"的混血活了 30 年^[1:1]。

但说实话，这条混血路线走得最远的其实是 C#——只是它做得更隐蔽：

• LINQ：Erik Meijer 把 Haskell 的 monad 和查询综合"偷运"进了主流语言；
• records、模式匹配、switch 表达式、init-only：这些全是 ML 家族的家当，经由 F# 先在 .NET 里趟路，再反向输入给 C#；
• async/await：原型是 F# 的 computation expressions——"学术成果经工业界放大"的教科书案例。

这里有个常被忽略的事实：F# 本身就是 OCaml 的直系兄弟（Don Syme 在微软剑桥研究院起家时，做的就是"OCaml for .NET"）。

所以 .NET 生态其实是混血双轨制——F# 保留了纯血 ML 的完整类型推断和不可变默认，C# 负责把这些特性"平民化"。

比如 var：C# 只做局部类型推断，在 API 边界强制显式标注。这恰好踩中了 Leroy 说的权衡——全局推断固然优雅，但大规模项目需要显式签名充当文档^[1:2]。C# 没有追求完整的 Hindley-Milner 推断，不是不能，而是判断了对工程团队的阅读成本不划算。

这是 C# 一以贯之的设计哲学：不求理论上最纯，只求工程上最优。

二、GC 之争：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：覆盖高频热路径；
• NativeAOT：把 GC 的存在感压到极低，打进嵌入式和 CLI 启动场景。

换句话说：OCaml 证明了"GC 语言可以做系统编程"，C#/.NET 则进一步证明了"GC 语言可以按需在单个函数尺度上做手动内存决策"。

这比 Rust 的全局所有权纪律更符合 Leroy 那套"组织经济学"逻辑——团队里不是每个人都需要精通生命周期，但热路径上的那个人手里有工具。

三、并发哲学：Leroy 大概会更喜欢 Orleans

访谈里最生动的一段，是 Leroy 吐槽共享内存并发：

"共享内存并发就像你想和邻居交流，你破门而入，移动他们家的家具，等他们回来时会说'哦，有东西被移动了，大概是想告诉我什么'……也许你可以直接去见你的邻居？——这就是消息传递。"

他推崇的是 Erlang 风格的 Actor 模型^[1:4]。

有意思的是，C# 主线走的是 async/await + 共享状态的老路，但 Orleans 的 Virtual Actor Model 就是 .NET 世界对消息传递的完整回答：grain 之间不可共享状态、只能收发消息，单机到集群共用同一套心智模型。

再加上：

• System.Threading.Channels：标准的 CSP 管道；
• TPL Dataflow：数据流网络；
• async/await：任务并发。

C# 其实是把三种并发范式都摆上了货架。

这里有个颇具讽刺意味的对照：OCaml 5 为了 Jane Street 的需求在共享内存上做了妥协，而 C# 这个"共享内存出身"的语言，反而把 Actor 模型做成了工业级产品。

四、形式化验证：C# 是「轻验证」路线的极致

文章里有一张三种形式化方法的对比表^[1:5]：

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% 的普通项目也用得起。

五、AI 时代：C# 最大的隐藏优势

访谈最尖锐的部分是关于 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# 的回答

访谈结尾，Leroy 说了一段让我印象很深的话：

"写出代码从来不是终点。理解代码为什么正确，才是真正的编程能力。"

一个学术语言的守护者，用三十年证明"可靠性与工程实用可以共存"。

而 C# 用另一种方式回应了同样的命题：不必要求每个开发者都成为证明专家，而是把验证、内存安全、类型纪律，一层层织进语言和平台的基础设施里，让正确的代码成为默认路径。

OCaml 是第三条道路的宣言，C# 是第三条道路的基建。

Dijkstra 那句话放在今天依然紧迫：我们应该用自己完全理解的程序，去解决未知世界的问题——而不是反之。

只不过在 2026 年，帮你"理解程序"的，除了你的大脑，还多了一个编译器，和一个永远在生成"差不多正确"代码的 AI。

选一门能让编译器替你吵架的语言，可能是这个时代最务实的浪漫。

本文基于 Xavier Leroy 在 The Peterman Podcast（2026 年 7 月）访谈的解读文章展开，部分观点为作者延伸。