@ryanlpeterman: Xavier Leroy (creator of OCaml) is an expert in compilers, formal verification of software and functional programming. …

Xavier Leroy (creator of OCaml) is an expert in compilers, formal verification of software and functional programming.

This interview should be an approachable resource if you’re curious about formal verification of software since I was learning that on the fly during it.

In this episode:

• OCaml compared with Rust and JavaScript • What is formal verification and how does it work • How languages call each other across boundaries • How to address “almost-correct” LLM code • How type inference works in programming languages

Where to watch:

• 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… • Transcript - https://developing.dev/p/creator-of-ocaml-functional-programming…

Thank you to the sponsor of this episode for supporting my work:

• WorkOS: makes your app Enterprise Ready with easy to use APIs to add SSO, SCIM, RBAC, and more in just a few lines of code, check them out at https://workos.com

Chapters:

00:00 - Intro 00:43 - What sets OCaml apart 04:39 - OCaml vs Rust 07:57 - Why is manual memory management more performant 11:21 - Javascript vs OCaml 14:00 - Famous Rob Pike quote 16:05 - Type inference and how it works 22:12 - What is formal verification and how does it work 40:07 - What made multicore support difficult for OCaml 50:17 - How programming languages interface and call each other 57:41 - The danger of almost-correct LLM code 01:05:39 - How LLMs will change programming languages 01:10:26 - Industry vs academia 01:15:05 - Most interesting unsolved problems 01:18:30 - Top book recommendations for engineers 01:21:17 - Advice for his younger self 01:23:31 - Outro

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…（此处的解释在转录中未完整展开，但基本思想是编译器通过约束求解来推断类型。）

Source: YouTube 视频：@ryanlpeterman 采访 Xavier Leroy