OCaml 创始人谈形式化验证，也谈 LLM 的“几乎正确”代码

nicolascraske · x · 2026-07-21

这期播客采访了 **OCaml 创始人 Xavier Leroy**，主题包括编译器、形式化验证，以及如何看待 LLM 生成的“**几乎正确**”代码。 - 讨论了 OCaml 与 Rust、JavaScript 的差异。 - 解释了形式化验证是什么、在实践中怎么工作。 - 还谈到语言边界之间如何调用、类型推断如何运作。 - 和 AI 最相关的一点，是如何处理 LLM 写出的看似正确、但并不完全可靠的代码。 - 这期内容同时提供了 YouTube、Spotify、Apple Podcasts 和文字稿链接。