@ryanlpeterman: Xavier Leroy (OCaml 的创始人) 是编译器、软件形式化验证和函数式编程方面的专家。……

Xavier Leroy（OCaml 的创造者）是编译器、软件形式化验证和函数式编程领域的专家。

如果你对软件形式化验证感到好奇，这篇访谈应该是一个很好的入门资源，因为我在访谈中也是边学边问。

本期内容：

• OCaml 与 Rust 和 JavaScript 的对比 • 什么是形式化验证，它是如何工作的 • 语言之间如何跨边界相互调用 • 如何处理“近乎正确”的 LLM 代码 • 编程语言中的类型推断是如何工作的

观看渠道：

• YouTube - https://youtu.be/9Cswiqrq6So • Spotify - https://open.spotify.com/episode/7cdatlBEkAjx4XplVLjFxN?si=T0dXjBf2TkyulzoKvN9Z7Q… • Apple Podcasts - https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835… • 文字记录 - https://developing.dev/p/creator-of-ocaml-functional-programming…

感谢本期赞助商对我工作的支持：

• WorkOS：通过易于使用的 API，只需几行代码即可为你的应用添加 SSO、SCIM、RBAC 等功能，使其达到企业级标准。详情请访问 https://workos.com

章节：

00:00 - 开场 00:43 - OCaml 的独特之处 04:39 - OCaml 与 Rust 对比 07:57 - 为什么手动内存管理性能更高 11:21 - JavaScript 与 OCaml 对比 14:00 - Rob Pike 的名言 16:05 - 类型推断及其工作原理 22:12 - 什么是形式化验证及其工作原理 40:07 - 为什么对 OCaml 来说多核支持很困难 50:17 - 编程语言如何相互接口和调用 57:41 - 近乎正确的 LLM 代码的危险性 01:05:39 - LLM 将如何改变编程语言 01:10:26 - 工业界与学术界 01:15:05 - 最有趣的未解决问题 01:18:30 - 给工程师的推荐书籍 01:21:17 - 给年轻自己的建议 01:23:31 - 结尾

TL;DR： OCaml 的创造者 Xavier Leroy 分享了 OCaml 作为兼具函数式与命令式能力的系统编程语言的特点，对比了它与 Rust、JavaScript 的差异，并讨论了内存管理、类型推断等核心概念。

OCaml 与其他编程语言的区别

OCaml 首先是一门优秀的函数式语言：支持对归纳类型的模式匹配、递归、高阶函数和组合子。但与此同时，它也是一个相当不错的系统编程语言，拥有完整的指令式能力，包括异常处理、线程以及用户定义效果的处理程序（这是最近添加的功能）。

OCaml 具备非常可预测的成本模型和执行模型。编写代码时，你能比较清楚地知道哪些操作耗时、哪些快、哪些慢。这一点并非所有函数式语言都能做到——有些语言的性能表现相当不可预测。此外，OCaml 的实现性能很好，编译器虽然并非同类中最佳，但生成的代码效率很高。它的内存分配器和垃圾回收器延迟很低，不会造成长时间的停顿，这对于网络编程等任务至关重要。

最初 OCaml 并非为系统应用设计，而是偏向定理证明或领域特定语言的实现。后来，团队从系统领域获得了首批用户，尤其是 90 年代末康奈尔大学的 Ensemble 项目——一个用于可靠多播及协作式分布式应用（如协同编辑或多人在线游戏）的网络协议栈。项目初期使用 C 语言编写，代码虽能运行但难以维护和扩展。后来有人提议尝试 OCaml，代码变得优雅许多，性能也与 C 相当。特别地，他们在数据包传输过程中利用空闲时间运行垃圾回收器：发送数据包后有几微秒的空闲，正好可以执行 GC，几乎零成本。之后类似项目如 MirageOS 也使用了 OCaml。参与 Ensemble 的博士生之一 Yaron Minsky 后来加入 Jane Street，并用 OCaml 实现了交易基础设施。直到今天，Jane Street 仍然是 OCaml 的重要用户。自动交易要求快速、可靠且无长时间停顿，同时希望函数式编程的优雅，非程序员（如金融工程师或量化分析师）也能读懂代码。OCaml 恰好满足这些需求。

OCaml 与 Rust：自动与手动内存管理

Rust 和 OCaml 的主要分界线在于内存管理：OCaml 采用自动垃圾回收（GC），而 Rust 是明确的手动内存管理语言。在手动管理领域，Rust 是最优秀的语言——通过借用规则、所有权跟踪等机制，比 C/C++ 安全得多，但仍然是需要开发者自己分配和释放内存的语言。这让程序员对行为有更多控制，但管理内存仍然显著增加编程难度，即便有类型系统的帮助。除了内存管理，Rust 拥有许多函数式语言的高级特性，尤其是数据结构、模式匹配等方面。它成功地将 C/C++ 风格的低级编程与函数式编程的高级设施融合在一起。

性能权衡

手动内存管理并不总是更快。很多 C++ 代码因为不确定自己是否是唯一拥有者而大量复制对象，复制操作在时间和内存膨胀方面成本很高。对于这类应用，GC 语言反而更好。使用 GC 还允许在数据结构中安全地共享数据，而 Rust 的所有权规则限制了共享，导致可能需要取消共享，从而消耗更多内存。

垃圾回收是运行时发生的：程序会不时停止执行你写的代码，转而扫描内存、寻找不再使用的部分，因此存在运行时开销。根据应用不同，开销可能在 10%、20%，甚至 30%。但这并不意味着整个程序比手动管理内存慢 30%，因为手动管理也可能产生其他成本（如复制）。有很多研究尝试在编译时做更多自动内存管理，对于某些编程风格（容易追踪对象生命周期的）可以做到一定程度，但运行时通常仍有不少工作。

能否混合两种内存管理？

Jane Street 正在探索一个名为 Oxidized OCaml 的变体（受 Rust 启发），目前非常实验性。他们尝试对某些数据结构进行栈分配，函数返回时自动释放，成本很低。但早期的实验结果表明实际收益并不像想象中那么大。对于生命周期很短的对象，垃圾回收或堆分配成本其实很低——如果它们在下一次 GC 前就消亡，回收成本微乎其微。长生命周期的数据结构成本更高，因为会被多次扫描和分析。栈分配正好适用于第一类对象（短生命周期），因此收益不显著。

对 JavaScript 的看法

Xavier 明确表示不欣赏 JavaScript。JavaScript 非常动态：类型检查完全在运行时进行，所有东西几乎都可以在运行时重新定义，包括方法调用的语义。语言的某些方面非常灵活，可以大量元编程，但这也是重大弱点——程序可能非常脆弱，并带来安全问题。JavaScript 是终极动态语言，而 OCaml 非常静态：静态类型、静态绑定，所有内容在编译时固定下来。两者的数据模型也不同，JavaScript 更偏向面向对象。不过 JavaScript 内部包含一个不错的函数式语言核心（基本是 Lisp 变体），可以用来做函数式编程。它的设计者 Brendan Eich 以前是 Lisp 背景，但那是非常动态的 Lisp。

Xavier 不喜欢它的主要原因是动态特性做得过头了。那种元对象协议——可以重新定义非常基本的操作如方法调用的语义，方法可以内省自己的调用栈、查看调用者及其代码——简直是安全噩梦。这些东西完全没必要，不利于写出好程序，也容易被滥用。

函数式编程的学习难度

关于“函数式语言更难学”的观点，Xavier 认为函数式编程本质上并不更难，尤其如果你有一点数学背景的话。针对 Rob Pike 关于谷歌招聘年轻毕业生、无法理解“卓越的语言”的引述，Xavier 认为那很大程度上描述了 Google 的招聘方式（招聘大量刚毕业工程师然后在内部培训），而其他公司如 Jane Street 会招聘教育背景更丰富、更多样化的人。Jane Street 甚至把 OCaml 作为筛选候选人的工具——申请者虽然更少，但背景通常更有趣。

最后他指出，Python 有 50% 的函数式特性。很多好的 Python 代码看起来就像带有推导式的函数式代码。当人们熟悉 Python 时，其实已经走了一半的函数式编程道路。

类型推断的原理

类型推断的基本思想是不需要声明每个变量、每个函数参数、每个局部变量的类型，因为类型通常可以从变量的使用方式中推导出来。例如 X = string.length(S) — 你知道 S 是字符串，X 是整数，因为 string.length 的类型告诉了你这些。

实际实现更复杂：编译器需要收集一系列约束，然后尝试求解。如果没有解，就是类型错误；有时有多个解，就需要找到好的准则来选择一个（否则结果对程序员来说不可预测）。程序员仍然可以添加类型注解，以帮助文档化和提高可读性。主要优点是让代码更简洁——你不需要到处写类型，只在有助于文档化的地方加就行。

更具体的例子：假设你有一个函数，带两个参数 X 和 Y……（此处的解释在转录中未完整展开，但基本思想是编译器通过约束求解来推断类型。）

来源： YouTube 视频：@ryanlpeterman 采访 Xavier Leroy (https://www.youtube.com/watch?v=9Cswiqrq6So)