Xavier Leroy Warns AI Slop Floods CompCert Bug Trackers

Xavier Leroy警告AI垃圾信息正涌入CompCert缺陷追踪系统 Xavier Leroy指出，形式化软件验证或将终于在工业界获得关注，因为大语言模型迫使开发者不得不面对规范瓶颈。 Xavier Leroy探讨了OCaml的架构权衡，将其垃圾回收模型与Rust的编译期所有权语义进行了对比，并分析了Multicore OCaml重构过程中攻克的工程难关。他阐释了形式化验证的数学基础，重点介绍了Coq和Lean等交互式定理证明器如何对CompCert与seL4等关键任务系统进行验证。此外，Leroy还批判了大量涌入的AI生成代码，强调合成软件带来的运营负担以及形式化规范瓶颈所构成的持续挑战。 Xavier Leroy提醒称，AI并没有将软件工程的成本降至为零，因为验证、审查和维护依然是代价高昂的负担。 (57:41) 开源维护者正面临AI生成的问题报告所带来的巨大运营开销，Leroy指出像OCaml和CompCert这类项目报告的问题中，大约只有十分之一属于真正的bug。 (57:41) 通用软件的形式化验证仍受限于规范瓶颈，即编写精确且不自相矛盾的数学前提条件往往比编写代码本身更难。 (61:40) CompCert证明了安全关键型基础设施可以使用Coq等交互式证明助手进行直至汇编层面的全面验证，从而消除整类编译器bug。 (25:19)

OCaml creator Xavier Leroy argues that programming language design and formal verification are converging to address software reliability, though the rise of generative AI introduces new specification bottlenecks and maintenance risks. OCaml's Pragmatic Systems Balance and Predictability (0:43) Leroy distinguishes OCaml by its combination of functional expressiveness, imperative power, and a transparent cost model that makes runtime performance intuitive to predict. Paired with a native-code compiler and an incremental, low-latency garbage collector, the language moved beyond academic roots like theorem provers to mission-critical systems. Cornell's late-1990s Ensemble project matched raw C networking speeds by triggering incremental GC passes during the microsecond intervals while network packets were in flight. This operational predictability later led trading firm Jane Street to adopt OCaml for its core automated trading infrastructure. Memory Management Trade-Offs: OCaml vs. Rust (4:39) While Leroy praises Rust as the finest manual memory management language available, he highlights that explicit borrow checking imposes a continuous cognitive tax compared to automatic garbage collection. Furthermore, manual management does not inherently guarantee better performance. Developers fearful of ownership ambiguities in languages like C++ often resort to defensive object cloning, incurring substantial overhead. In contrast, garbage collection handles deep structural sharing naturally without duplicating data. Leroy notes that runtime garbage collection typically costs between 10% and 30% of application execution time due to heap tracing. However, hybrid experiments like Jane Street's "Oxidized OCaml"—which introduces stack allocation for temporary values—yield smaller performance gains than expected. In generational collectors, short-lived objects are already reclaimed cheaply in the minor heap, meaning stack allocation optimizes the exact category of data that generational collectors already handle with minimal overhead. Mechanized Proofs and Formal Verification Realities (22:11) Distinguishing verification from traditional testing, Leroy cites Edsger W. Dijkstra's maxim that testing proves only the presence of bugs, never their absence. Formal verification relies on mathematical semantics to verify every execution path against a formal contract of preconditions and postconditions. Because interactive proof assistants operate strictly in mathematical logic, language semantics must explicitly model state transitions to reason about imperative code. While Turing's halting problem renders universal verification undecidable, Leroy emphasizes that domain-specific verification remains fully achievable. Leroy applied these principles to CompCert, a C compiler written in a pure functional style whose translation to assembly was mathematically verified using Coq to eliminate compiler-introduced bugs. Similarly, the Australian seL4 microkernel achieved complete verification across roughly 8,000 lines of systems C code. Although constructing formal proofs requires substantially more initial effort than writing raw code, it significantly eases long-term maintenance by ensuring modifications cannot introduce silent regressions. Shared Memory, Concurrency, and Runtime Architectures (40:06) OCaml operated with a Global Interpreter Lock (GIL) for decades before introducing multicore support in 2022. Leroy explains that the prolonged timeline stemmed from the complex challenge of redesigning the sequential runtime and garbage collector for multi-threaded execution without tanking single-core performance with mutexes. While Leroy personally favors message passing, industrial demand forced a shift to shared-memory concurrency, which introduces intricate hardware memory models and data-race hazards. Safe managed languages like OCaml and Java face the strict requirement of preserving type safety and complete object initialization across threads even under data races, rather than relegating races to undefined behavior as C and C++11 do. Outside runtime cores, bridging managed code with native C libraries remains inherently messy due to mismatched data layouts, such as boxed floating-point numbers and multi-dimensional pointer arrays. Leroy strongly advocates for static linking over dynamic loading via dlopen to eliminate runtime dependency failures. Generative AI, Verification Limits, and Software Quality (57:41) Leroy pushes back against claims that generative AI reduces programming costs to zero, arguing that generating large volumes of synthetic code simply creates operational liabilities because human auditing remains expensive and fatigue-prone. Bug trackers for OCaml and CompCert have experienced an influx of multi-page AI-generated issue reports that rarely present reproducible bugs. Pairing code generation with formal proof checking offers a potential safeguard, but that introduces a specification bottleneck: drafting formal specs remains notoriously difficult, and flawed or contradictory preconditions can cause provers to vacuously verify broken implementations. Looking at broader trends, Leroy notes that static type systems act as useful structural rails for LLM generation, though current translation pipelines frequently output fragile code, such as translating C into monolithic unsafe Rust blocks. He identifies preserving software engineering discipline against pressure to deploy unverified AI code as an urgent challenge, alongside the open problem of creating high-level programming models for non-numerical computing on GPUs. Leroy suggests computing may finally be entering the decade of formal software verification as machine learning assists mechanized proof assistants. However, whether formal methods can expand beyond safety-critical software depends on overcoming the specification bottleneck and finding abstractions capable of verifying complex modern workloads.

OCaml 创造者 Xavier Leroy 在本次访谈中指出，可预测的成本模型、强类型系统与形式化语义是构建高可靠软件的核心基石。他主张在面对现代高并发、硬件异构以及大语言模型代码生成的浪潮时，工程师应坚持严格的工程规范与数学验证，而非盲目追求代码生成数量或无谓的语言动态性。 OCaml的系统设计与内存权衡 (0:43) Xavier Leroy 说明 OCaml 之所以能跨越学术界走向工业界，关键在于兼具函数式表达力与极度透明、可预测的底层执行模型。虽然 OCaml 最初用于定理证明器与领域特定语言开发，但 1990 年代末康奈尔大学的 Ensemble 多播网络栈重写项目证明，通过在网络数据包传输的微秒级空隙触发增量垃圾回收，其运行效率完全足以匹敌 C 语言；随后 Jane Street 等量化交易公司也在高频交易基础设施中重度依赖其毫秒级确定性。针对与 Rust 的对比，Leroy 称赞 Rust 是最出色的手动内存管理语言，但他指出手动资源管理并非天然具备性能优势，开发人员因担心所有权边界而频繁防御性深拷贝反而会拖累性能，而垃圾回收则能零成本原生支持深度结构共享。对于运行时开销，他解释分代垃圾回收处理短生命周期对象极为轻量，诸如栈上分配等局部优化带来的实际性能收益往往低于预期。 形式化验证与程序契约的边界 (22:11) 针对软件正确性保障，Leroy 重申了 Edsger W. Dijkstra 的经典断言，即测试只能证明缺陷的存在，而无法证明缺陷的缺席。形式化验证借助静态分析与数学定理证明，穷举程序在所有可能输入下的执行路径。在微内核 seL4 或他本人主导的验证 C 编译器 CompCert 项目中，机器可检查的交互式证明器（如 Coq/Rocq）确保了编译输出的汇编指令严格保持源代码语义，杜绝了误编译隐患。Leroy 强调，纯函数式编程由于摒弃了可变状态共享，与数学语义最为贴近，这也是 CompCert 采用纯函数式编写的核心原因。针对图灵停机问题等理论上的不可判定性，Leroy 认为理论限制并不妨碍针对特定工程领域与具体程序建立完备的数学规范，只要在函数边界明确前置条件与不变量契约，就能有效阻断导致安全漏洞的崩溃与未定义行为。 共享内存并发与跨语言运行时鸿沟 (40:06) 回顾 OCaml 历经数十年才于 2022 年推出多核支持（Multicore OCaml），Leroy 坦言迟滞不仅源于重构垃圾收集器与分配器的系统工程重担，更源于对共享内存并发哲学的保留。相比于 Erlang 式基于消息传递的通信范式，现代主流工业界强制要求共享内存，但这在硬件重排序下极易诱发数据竞争与未定义行为。为了在乱序执行下维持类型安全并杜绝未初始化读取，语言设计团队必须制定极为繁琐的内存模型。而在单核时代，OCaml 与 Python 类似，长期通过全局解释器锁（GIL）来保护堆分配安全，该机制虽然允许交替执行 I/O 操作，却彻底阻断了真正的多核并行计算。此外在跨语言互操作（FFI）层面，托管语言的装箱机制、堆分配协调与根对象追踪，与 C 语言原生连续内存布局存在根本冲突，Leroy 坚持生产环境应尽可能采用静态链接，以在链接期提前消除动态符号查找的不确定性。 大模型生成代码的缺陷与规范瓶颈 (57:41) 面对生成式人工智能工具的普及，Leroy 明确反对将编程成本降为零的宣传，直言后续的审查、校对与维护成本不仅未清零，反而在迅速上升，他认为新增的每一行代码本质上都是系统负债。针对开源社区遭遇的合成内容泛滥与虚假 Issue 轰炸，Leroy 指出大模型生成代码往往呈现出“表面看似正确实则潜藏细微 Bug”的特征，而由于类型系统能充当结构化护栏，大模型在强静态类型语言中的输出质量显著优于无约束环境。部分项目尝试通过大模型将 C/C++ 转换为 Rust，却往往只是机械生成了满篇由 unsafe 块包裹的代码，未真正获得所有权安全。若想利用 Lean 等证明器对 AI 代码进行形式化校验，最大阻碍在于“规范本身难以形式化”，一旦大模型草拟出互相矛盾或不可满足的前置条件，就会导致函数体在空真（vacuous truth）逻辑下被判为正确，给系统注入虚假的安全感。 在工业界日益追求代码生成速度的背景下，Leroy 认为软件工程的关键未解难题在于如何在缺乏形式化规范的复杂系统与深度学习模型中坚守代码质量。他建议工程师过早专注狭隘方向不如扎实打牢计算理论基础，并推荐通过精读经典著作来培养对算法精简性与代码优雅度的底层直觉。

[22:11] Xavier Leroy: Code that crashes is always code that can be attacked. [57:41] Xavier Leroy: And for me every new line of code is a liability. [61:40] Xavier Leroy: It's not just that verification is hard, but agreeing on the spec can be difficult, too. [35:56] Xavier Leroy: Purely functional style is much closer to mathematical style, so much easier to reason about. [55:32] Xavier Leroy: I think programs should be statically linked so that there's no surprise when you run them. [78:09] Xavier Leroy: Maybe this will be the decade of formal verification of software. We've been waiting for that for 50 years so maybe it will finally take off. [14:00] Xavier Leroy: I think functional programming is not fundamentally harder, especially if you have a little bit of mathematics background.

[0:00] Testing can only show the presence of [0:01] bugs, but not their complete absence. [0:04] >> This is the creator of the OCaml [0:06] programming language, and I asked him [0:08] all about programming language design [0:09] and formal verification. [0:11] >> Oh my god. [0:12] >> [laughter] [0:12] >> Uh [0:13] yeah, I'm not a big fan of JavaScript. [0:15] And Rust is the finest language for [0:18] manual memory management. Manual memory [0:20] management is not always faster. [0:22] Maybe this will be the the decade of [0:25] formal verification of software. [0:27] >> If you took LLM-generated code and [0:30] turned it up, what languages would [0:32] become more popular? What languages [0:34] might fade away? [0:35] >> Woof. [0:36] Uh [0:37] >> Here's the full episode. [0:43] What sets OCaml apart from other [0:45] programming languages? [0:47] >> It it is a fine functional language. [0:50] Okay, you can [0:51] like functions by case over inductive [0:54] types and recursion and combine them [0:57] with combinators and then higher-order [0:59] functions and everything. So so it's [1:01] really a a a fine functional language, [1:04] but it's also a fairly decent systems [1:07] programming language. [1:08] And [1:10] um [1:11] so it has fully imperative power. It has [1:13] lots of [1:14] interesting control structures, um [1:17] exceptions, threads, [1:20] handlers for user-defined effects, which [1:22] we added recently. [1:24] Um and it has a very predictable cost [1:28] model execution model. So so when you [1:31] write your code, you have a pretty good [1:32] idea what what will take time and what [1:36] will be fast and what will be slow. And [1:38] that that's not the case for all [1:39] functional languages. [1:41] Some are pretty unpredictable. And and [1:43] then the implementation is also pretty [1:45] performant. Okay, so there's there's a [1:47] fairly decent compiler, not the best in [1:50] in its class, but the code is pretty [1:52] efficient. There's a very good allocator [1:54] and garbage collector with low latency, [1:56] so you don't have much pauses. [1:59] You don't have long long pauses and that [2:01] that's quite important when you do [2:02] things like network programming. [2:04] And and so [2:06] and so you can write systems [2:08] applications in [2:10] in in mostly functional style and and [2:13] with all the benefits of functional [2:15] programming. [2:16] And and so initially [2:19] OCaml wasn't [2:21] wasn't designed for those kind of [2:22] applications, okay? It was more for [2:24] things like theorem proving [2:27] or implementing domain-specific [2:28] languages. [2:30] And then we got some of the first users [2:33] who were from the systems community, in [2:35] particular [2:37] the Ensemble project in the late '90s at [2:40] Cornell University. So so it was a [2:42] network stack for a network protocol [2:46] stack for [2:47] reliable multicast and those kind of, [2:50] you know, [2:51] collaborative distributed applications [2:53] like collaborative editing or [2:55] multiplayer video games. [2:57] And and their first code was in C, of [2:59] course. [3:00] They were systems people, right? And and [3:03] it worked, but it was unmaintainable and [3:05] they couldn't extend it anymore. And [3:07] someone had the idea to try OCaml and [3:10] and so first the code became a lot nicer [3:13] and easier to to to evolve and the [3:15] performance was about as good [3:18] as the C code. And in particular, they [3:20] they had this uh [3:22] brilliant trick of running the garbage [3:23] collector while [3:26] packets are in flight, okay? Well, [3:28] once you've sent a packet, you're you're [3:30] idle for a few [3:32] microseconds and so you can run some [3:35] GC. It costs nothing. [3:37] And so they were very happy with that [3:40] and and and then there were some other [3:42] projects [3:44] like this using [3:46] OCaml for systems applications like the [3:49] Mirage Mirage uh [3:52] And and and yeah, and and and another [3:55] benefit or consequence of this uh [3:58] Ensemble project is that uh one of the [4:00] PhD students working on that was Yaron [4:02] Minsky, who then went to Jane Street and [4:06] and implemented their [4:08] their trading infrastructure in OCaml. [4:11] Uh so they are still today one of our [4:13] big users. [4:14] >> [snorts] [4:14] >> And and again, it's well, they do [4:16] automatic trading, so it must be fast [4:18] and reliable and [4:20] and no long pauses, but they also want [4:22] the elegance of functional programming. [4:24] And they want non- non-programmers to be [4:27] able to read and and their code like [4:30] financial engineers or quantitative [4:32] analysts. [4:33] And and so yeah, so OCaml is a fairly [4:36] good match for those kind of [4:37] applications. [4:39] >> I thought it might be interesting to [4:41] ground some of the conversation here by [4:44] making comparisons across programming [4:46] languages, maybe ones that people know [4:49] more. [4:50] When you think about Rust versus OCaml, [4:53] what are the big differences and the [4:55] pros and cons of the various design [4:57] decisions in those languages? [4:59] >> The the big dividing line is between [5:02] Rust and OCaml is [5:04] uh well, OCaml has automatic memory [5:05] management, garbage collection. [5:07] And Rust is uh is definitely uh a [5:11] language for manual memory management. [5:13] Uh it's a it's it's the finest language [5:16] for that I know for uh manual memory [5:18] management, okay? It means manages to to [5:20] make it [5:21] uh mostly safe [5:23] uh with with the discipline of uh [5:26] borrowing, etc. And uh and and tracking [5:29] ownership and so on. So it's in [5:31] infinitely uh uh safer than C or C++, [5:35] but it's still uh a language where you [5:38] uh allocate and free memory uh yourself. [5:42] And on the one hand, it gives more [5:44] control over what the program is doing. [5:46] On the other hand, it's still a big [5:47] responsibility. It's significantly [5:50] harder to write programs when you have [5:51] to to manage your memory, even with the [5:54] help of Rust [5:56] types. [5:57] So, [5:59] so yeah, so for me that that's kind of [6:01] the main [6:02] dividing line. [6:03] Otherwise, Rust has [6:07] Well, Rust has many of the high-level [6:10] features of functional languages, okay? [6:13] And in particular in in [6:17] data structures and ability to do [6:19] pattern matching and so on. So, it's a [6:22] very interesting design because they [6:24] really managed to [6:26] some kind of fusion between [6:29] you know, C or C++ style low-level [6:31] programming [6:33] and and some of the high-level [6:34] facilities of functional programming. [6:37] But still, that that divide, garbage [6:39] collection versus manual memory [6:41] management, remains. [6:43] >> So, it sounds like this is a performance [6:46] trade-off where you give more to the [6:48] programmer in exchange for higher [6:50] performance. [6:52] >> That's mostly true. That said, [6:56] manual memory management is not always [6:58] faster. [7:00] Or or or you need to be a very good [7:02] programmer so that it's always faster. [7:05] There's been some [7:07] some some mostly C++ code, for instance, [7:10] that that does a lot of copying [7:12] of objects just because you know, you're [7:15] you're not quite sure you're the only [7:16] owner. So, so you make a copy and now [7:19] you're the only owner. But the copying [7:21] is is quite costly in time and in and in [7:24] memory [7:26] bloat. [7:27] So, and and for those kind of [7:29] applications, a garbage collected [7:30] language is better. [7:32] And likewise with with [7:34] GC, you can work with shared sharing in [7:38] data structures, okay? And it's [7:40] perfectly safe. [7:42] Um [7:43] uh while um [7:45] uh [7:46] sharing is kind of limited with uh [7:48] Rust's uh [7:49] ownership discipline. Uh [7:52] there there are more constraints. And so [7:54] you may end up unsharing and so using [7:56] more memory. [7:57] >> It is surprising to me that um [8:01] that manual memory management would in [8:03] many cases be more performant than [8:05] automatic because for instance in in [8:08] other patterns in computer science, like [8:10] let's say letting the compiler optimize [8:12] things for you instead of optimizing [8:14] things yourself, I would have thought [8:16] that, you know, letting some system [8:19] manage memory for you rather than [8:21] manually mem- managing it would also be [8:24] better. So, why is there a difference [8:26] there? [8:27] >> Well, because garbage collection takes [8:28] place at run time. So, so we need from [8:31] time to time the [8:33] the program is no longer [8:35] computing, executing [8:37] what what you wrote. It is actually uh [8:40] uh scanning memory, [8:42] trying to find uh memory that is no [8:43] longer used. So, [snorts] so uh there's [8:47] there is uh a run time overhead. [8:50] And it can be uh depending on [8:52] applications 10%, 20%, [8:55] maybe sometimes 30%. Um but again uh [8:59] that that doesn't mean the whole program [9:01] is 30% uh [9:03] slower than if uh you had written it [9:05] with manual memory management because [9:07] there may have been uh other costs as [9:09] you said uh uh of of of manual memory [9:12] management. But yes, um there's [9:16] Uh um well, there's been a lot of [9:18] research on on trying to do um more, I'd [9:21] say, compile time automatic memory [9:23] management. [9:25] And you can do that to some extent, but [9:28] it it's for for for some some [9:30] programming styles where it's easy to [9:31] track the lifetime of of objects and and [9:34] and data blocks. [9:36] But in general, you still have quite a [9:38] bit of work to do at runtime. [9:41] >> I think a lot of people for garbage [9:42] collection, they might think of it as a [9:44] binary thing. It's either you have it or [9:47] you don't. [9:48] But I wonder in OCaml, is there some way [9:51] to [9:53] like turn down the memory management and [9:55] do some manual, so kind of like a [9:57] mixture to have the benefits of both? [10:00] >> So that's one of the things that the [10:02] Jane Street people are looking at. So [10:04] they have their [10:06] OCaml variant, Oxidized OCaml, which is [10:10] kind of OCaml with some inspiration from [10:12] Rust. So it's still very very [10:14] experimental, but yeah, they've been [10:16] playing with things like stack [10:18] allocation of some data structures [10:21] so that automatically deallocated when [10:23] the function returns, which is quite [10:25] cheap. Yeah, there there are a few [10:27] things you could try, but but I'm not [10:29] sure they are going to make such a big [10:30] difference. I remember doing this with a [10:33] student some experiments with stack [10:34] allocation of uh [10:37] of data structures a long time ago, and [10:40] you don't win as much as you would [10:42] think. See, garbage collection or [10:45] heap allocation is pretty cheap for [10:47] objects that have a very short lifetime. [10:49] Okay, if if they if they die before the [10:52] next garbage collector, [10:55] they they they will cost very little in [10:56] garbage collection time. [10:58] Uh but it's more expensive for [11:01] long-lived data structures, okay, [11:03] because those will be scanned and uh [11:05] analyzed uh [11:07] multiple times. [11:08] And stack allocation works for the first [11:10] kind of objects, things that [11:13] have short lifetime anyway. [11:15] So so you don't you don't win as much as [11:17] as as you think. [11:20] >> Um one of the most popular programming [11:23] languages JavaScript. Uh curious when [11:25] you think about the difference between [11:26] JavaScript and OCaml, what's the main [11:29] thing that comes to mind? [11:31] >> Yeah, I'm not a big fan of JavaScript. [11:33] Well, so JavaScript is uh Well, first [11:35] it's it's very dynamic. So, [11:38] type checking is entirely dynamic, but [11:40] it's more than that. I mean, pretty much [11:42] everything can be redefined at run time, [11:44] including, I don't know, the semantics [11:46] of method invocation, for instance. So, [11:48] so really some some pretty [11:52] fundamental aspects of the language [11:55] are very flexible. So, some people say, [11:57] "Oh, that's great. We can do lots of [11:59] meta meta programming, etc." And and to [12:03] me it it also it it's a big weakness. I [12:05] mean, it it is pro it makes programs [12:07] that are that can be very fragile [12:10] and [snorts] [12:11] also have some security issues. So, so [12:13] yeah, so JavaScript is the ultimate [12:16] dynamic language, in my opinion, while [12:18] OCaml is very static. Static typing, [12:20] static binding, pretty much everything [12:22] is fixed at compile time. Okay. [12:25] Uh [12:26] and then [12:27] Well, I guess it's a kind of a different [12:29] data data model. Uh JavaScript is a [12:32] little more object-oriented in in in the [12:35] way it it presents data. Maybe that's [12:37] not that important. And and to say one [12:40] good thing about JavaScript is that it [12:42] also contains a decent functional [12:45] language [12:46] inside. You know, there's there's a [12:47] little bit of a little core of [12:49] JavaScript which is basically Lisp [12:51] and and can be used to do a functional [12:54] programming if you want. [12:56] Um and and actually the the designer [12:59] of JavaScript, I think, was a former [13:02] Lisp person. I can't remember his name, [13:04] but [13:05] >> Brendan Eich, maybe? [13:06] >> Uh yeah, Brendan Eich, yeah. [13:08] There there was a little bit of heritage [13:10] from from Lisp to to JavaScript. [13:14] But a very dynamic kind of Lisp. [13:17] >> You said you weren't the biggest fan. Is [13:19] that just because of the dynamics or is [13:21] there some other aspect? [13:22] >> Yeah, mostly the dynamics. I think [13:26] They really went overboard with that. [13:28] This kind of meta meta object protocol [13:31] where you can really find the semantics [13:33] of [13:34] very basic operations like method [13:36] invocation. The fact that a method can [13:40] There's a lot of introspection. A method [13:41] can look at its own call stack, look at [13:44] its callers, look at the code of their [13:46] of its callers, which is a security [13:48] nightmare. [13:49] Um [13:50] All those things I think are completely [13:52] unnecessary and not conducive to good [13:55] programs. [13:57] Easily abused. Yeah. Easily abused. [14:00] >> I think on the topic of functional [14:02] languages compared to imperative [14:04] languages, there's this thought that uh [14:07] functional languages are kind of hard [14:09] harder to learn or maybe they have more [14:11] perceived complexity. And actually, I [14:15] when I my research, there's this popular [14:17] quote from the designer of Go, Rob Pike. [14:21] And he's talking about what they [14:22] intended to do with code with Go. [14:25] And he said, you know, the key point [14:27] here is the programmers are are [14:29] Googlers. They're not researchers. You [14:31] know, they they're young, fresh out of [14:33] school. They're not capable of [14:35] understanding a a brilliant language. [14:37] And I think, you know, that that thought [14:40] of a brilliant language is often [14:42] attributed to functional languages. [14:44] What do you think about is a language [14:47] like OCaml harder for programmers to [14:49] grasp than imperative languages? [14:51] >> I think functional programming is not [14:53] fundamentally harder, especially if you [14:56] have a little bit of mathematics [14:57] background. So, coming back to the quote [15:00] by [15:01] by Rob Pike, uh [15:04] I think it describes very much how they [15:06] go about hiring at Google. Okay, they [15:08] they they hire a lot of uh [15:11] engineers who are fresh out of of [15:14] college. Some of them have master's [15:15] degree, but And and then they train them [15:17] internally. Other other companies I I [15:20] try to to hire people with more [15:22] education and perhaps a more diverse [15:25] backgrounds. [15:27] Um and and yeah, so so Jane Street for [15:30] instance and and some of those use OCaml [15:33] as a filter on on who who they want to [15:35] hire. [15:36] Yeah, they have fewer applicants, but in [15:39] general they have more interesting [15:40] backgrounds. So [15:42] um [15:44] And perhaps one last thing I would like [15:46] to say, Python is 50% functional [15:48] language. [15:49] Okay. Uh [15:51] a lot of good Python code looks like [15:53] functional uh code with comprehensions. [15:56] So I think uh uh [15:58] people are already halfway uh through [16:00] through functional programming uh when [16:02] when when they are comfortable with [16:04] Python. [16:05] >> Yeah, when I was learning OCaml in [16:07] college, I think one thing that really [16:10] stood out to me and I thought was [16:11] interesting was this concept of type [16:13] inference [16:15] where the compiler is [16:17] kind of uh it knows the types of [16:19] everything implicitly in the the way [16:21] that the code is written. [16:23] Um can you explain uh type inference and [16:25] what the advantages are? [16:27] >> Well, the the basic idea is that uh you [16:30] don't have to declare the type of every [16:32] variable you introduce, every function [16:35] parameter, every local variable because [16:37] quite often the type can be deduced from [16:39] the uses of the variable. Okay? Uh like [16:43] if you do uh I don't know X equals [16:45] string length of S, uh then you kind of [16:48] know that S is a string and X is an [16:51] integer, right? Because that's what the [16:52] string length function uh that's the [16:55] type of string length and it it tells [16:57] you that. [16:59] Um so so that's the basic idea. Uh [17:03] now the the actual realization is a [17:05] little more complicated. Basically, you [17:07] need to collect a number of con- the [17:09] compiler needs to collect a number of [17:11] constraints and then try to solve them. [17:14] Uh see uh [17:16] well, if there's no solution, then it's [17:17] a type error. But, sometimes there are [17:19] several solutions and you must find good [17:22] criteria to choose one, otherwise you're [17:25] I mean, it also needs to be predictable [17:27] for for programmers. [17:28] Um, and often also you can you [17:32] um you can still put type annotation as [17:34] a programmer you can still put type [17:35] annotations if that makes the code [17:37] clearer. [17:38] So, I think the the the main advantage [17:40] is precisely to have less verbose code, [17:43] less verbose code. Well, you don't [17:46] you don't need to put types everywhere, [17:49] but only where they help uh [17:51] documentation and and documenting the [17:53] code and and making the making it easier [17:57] to read. Okay. [17:59] Uh, but quite often you [18:02] um for for like small local functions, [18:05] for uh short-lived temporary variables, [18:07] you you [18:09] the type is obvious from the context, so [18:11] let's just omit it. [18:13] >> If I'm trying to figure out how this [18:14] type inference works, the intuitive [18:16] example you said makes sense. But, uh [18:18] you mentioned it seems to be some sort [18:20] of system of equations that you solve or [18:23] something like that. Can you give a uh [18:25] concrete example maybe, you know, what [18:27] does that look like to the compiler? [18:29] >> Okay. Well, for a slightly more complex [18:31] example, say you have um [18:34] function with two parameters X and Y, [18:36] and then you do if X equals Y. [18:40] So, that tells you that X and Y have the [18:41] same type, but that still doesn't tell [18:43] you which type it is, uh assuming a [18:46] polymorphic uh equality comparison. [18:49] So, you've learned something about X and [18:51] Y, that they have the same type, but you [18:53] still don't know what the type is. [18:55] And later maybe you will learn something [18:56] about the type of X. [18:58] And now you will have determined the [19:00] type of Y as well. [19:02] So, so that's the kind of constraints [19:04] you you you accumulate and solve, um [19:07] little bit like, you know, Sudoku or uh [19:10] those kind of puzzles. And then there's [19:12] the interesting case where you don't [19:14] have enough constraints to find [19:17] a unique type. [19:18] So maybe in the end X and Y will be you [19:21] know they have the same type but it's [19:23] still unconstrained. [19:24] And and then that's where you [19:26] automatically get polymorphism for free. [19:29] Okay, the type checker said, "Okay, [19:31] those types are unconstrained so it can [19:33] work for any type." [19:35] So my function can take an X of any type [19:37] and a Y of the same type. Again, any [19:40] type and it's a polymorphic function. [19:43] So there's there's this beautiful I [19:45] think [19:47] phenomena phenomenon that that [19:50] polymorphism can be discovered [19:52] just by running type inference and [19:54] noticing that oh there are no [19:56] constraints so it must be polymorphic. [19:59] And and that was a great insight by [20:01] Robin Milner, the British computer [20:03] scientist pioneer who invented this ML [20:05] family of languages and and and this [20:08] kind of type inference in the 70s. [20:11] Polymorphism [20:12] was was [20:14] was not very well understood at the time [20:16] and so the fact that that he could have [20:19] he could introduce polymorphism so [20:21] easily in his language just as a [20:23] consequence of type inference [20:26] was a beautiful discovery. [20:28] >> So for type inference it seems like the [20:30] benefit is [20:33] you know the code is going to be a lot [20:34] more concise because we don't need to [20:37] write out all the types which seems [20:39] nice. But what are the tradeoffs of [20:41] adding type inference to a programming [20:43] language? [20:43] >> Well, as I said error messages can be [20:46] type error messages can be very [20:48] confusing [20:49] because [20:51] they not always point to the actual [20:54] source of the type error. [20:55] Okay. [20:58] The system may have done some some wrong [21:00] inferences and and and will report [21:03] though some of those inferences instead [21:05] of reporting the source the actual [21:07] source of the type error. So, it's been [21:09] it's been [21:11] the subject of much research. [21:13] And and there's there's no very [21:16] well-defined idea of the the source of a [21:18] type error, basically. [21:20] Um so, yeah. So, errors can be an issue. [21:24] Some features of type systems [21:26] are easy to combine with type inference, [21:28] to handle with type inference, and some [21:29] are harder. [21:31] Uh for instance, when it comes to [21:32] genericity, so I mentioned the [21:35] polymorphic parameter uh parametric [21:36] polymorphism, which which is very well [21:38] handled, but subtyping, the kind of [21:42] uh [21:42] thing you have in object-oriented [21:44] languages, is actually harder to to [21:46] combine with with type inference for [21:50] super technical reasons that I'm not [21:52] going to to go into. [21:53] Um so, so sometimes uh you have to make [21:57] a choice. Either you have type [21:58] inference, but it is less powerful, [22:02] uh or you you have uh full type [22:05] inference, but more restrictive type [22:07] system. [22:08] Uh [22:09] And and that that that that choice is [22:11] part of the language design, actually. [22:14] >> You mentioning this uh solver kind of [22:17] reminds me of the topic of formal [22:19] verification. Could you explain what [22:21] formal verification is? [22:23] >> Woo. [22:25] Well, it's the idea that um [22:28] um [22:29] you for for some programs, you want you [22:31] want strong guarantees that that that [22:34] the program is correct. Well, and and [22:36] guarantees that are hard to get just [22:37] with testing and and reviews, code [22:40] reviews. [22:41] Uh you know, there's uh this famous [22:43] quote by [22:44] uh Dijkstra, the the Dutch computer [22:47] pioneer, [22:48] uh which is which goes something like uh [22:51] testing can only show the presence of [22:53] bugs, but not their complete absence. [22:56] Uh because in general, there's an [22:57] infinite infinitely many inputs to your [23:00] program, and you cannot test them all. [23:03] So, you only test in your sample and [23:04] then sometimes you have surprises. [23:07] So, what if you want to make sure that [23:09] program is correct for an infinite [23:10] number of inputs? [23:12] And that's where you need to turn to [23:14] those so-called formal methods. So, [23:16] you're using mathematical reasoning, [23:18] you're using the uh [23:20] uh [23:21] static analysis algorithms on your on [23:23] your program to [23:26] really analyze all possible executions [23:28] of a piece of code and making sure that [23:32] it matches a specification. [23:35] The specification can be very simple [23:36] like the code will never crash [23:39] given well-formed inputs. [23:41] So, that that's a fairly simple [23:44] property, but still extremely useful [23:46] because code that crashes is always code [23:48] that can be attacked. It's always is [23:50] often security hole. [23:52] >> [sighs and gasps] [23:52] >> Um [23:54] so, for instance, all accesses within [23:56] array [23:58] all array accesses are within bounds. [24:01] That's a very simple property and it's [24:03] very hard to to ensure just by a type [24:06] system or just by testing. So, that's [24:09] [snorts] where you need some more [24:11] advanced formal verification. [24:12] And then there are [24:14] there are much more powerful specific [24:15] much more precise specifications that [24:17] you may want to check that can be where [24:19] the program always terminates. It can be [24:21] the program [24:22] doesn't [snorts] leak [24:23] confidential data. It can even be where [24:26] the program computes this mathematical [24:29] function [24:30] >> [snorts] [24:30] >> uh with [24:31] with an error floating point error under [24:35] I don't know, 10 to the minus six. Okay. [24:38] Something like that. Something very [24:39] precise like that. [24:42] And so, it's it's been really hot topic [24:45] in in [24:46] in in software sciences since the [24:49] uh since the '70s, I would say. There's [24:51] lots of techniques. [24:53] Some are just fully automatic like [24:56] static analysis, uh [24:58] but they're already pretty good at [25:00] finding bugs and making sure that some [25:02] bugs like array out of bounds are not [25:04] there. [25:06] And some [25:07] are a lot more interactive and and [25:09] require a lot more formal assistance to [25:11] write specifications and then do can so [25:15] called program proofs. So proving [25:17] mathematical statements about the [25:18] program. [25:19] >> I hear about it a lot more now which is [25:22] lean and these theorem provers. [25:24] Um what are those in this context and [25:28] how how are they used? [25:30] >> Uh so yeah so lean is is an example an [25:34] instance of the so called [25:36] provers or proof assistants. [25:40] Um so originally those were developed to [25:43] do mathematics on the computer. So not [25:46] nothing with [25:48] not formal verification of programs but [25:51] but they can also be used for formal [25:52] verification of programs. But the [25:54] initial motivation was really to do [25:56] mathematics with the help of the [25:57] computer. [25:59] Um where originally everyone focused on [26:02] automatic theorem proving. So having the [26:05] machine find proofs from [26:07] all by itself. [26:09] But that's very very difficult [26:12] and not necessarily what what [26:15] mathematicians need. [26:17] And so those proof assistants are more [26:20] like [26:22] where formal language is like like [26:24] programming languages but where you can [26:26] write mathematic definition mathematical [26:28] definitions mathematical statements [26:31] and they will help you prove. So so some [26:34] small proof steps they will do [26:35] automatically and for others the the [26:38] user still has to guide the prover [26:41] through through the major steps. [26:43] But the good thing is that the proof is [26:45] recorded also in a format that the [26:46] machine can understand and recheck. [26:50] So when you complete a proof in lean or [26:52] Coq, or Isabelle, or one of those tools, [26:55] and and it is rechecked, and and the [26:58] computer makes sure that all inferences [27:00] are justified, that you didn't forget [27:02] any case, that you uh you didn't use a [27:05] conclusion as an hypothesis, or where [27:08] all all kind of [27:09] problems you can have with a pencil and [27:11] paper proof. [27:13] And so, in the end, you get proofs that [27:15] are extremely uh [27:16] reliable, extremely credible. [27:20] Um and and it's been so so those tools [27:23] have been used a little bit uh [27:27] for well for for for some um [27:30] uh some big mathematical results, where [27:32] where the proofs are so big that that [27:34] that they can't be done just by humans. [27:37] They really need uh [27:38] computer assistance. [27:40] Uh [27:41] I think there's a recent example with a [27:43] weak uh Goldbach conjecture. Uh so, part [27:46] of the proof involved checking a whole [27:48] lot of inequality, maybe a thousand [27:50] inequalities involving several real [27:53] variables, and blah blah blah. And so, [27:56] um [27:57] computer assistance was really needed uh [27:59] to make sure that that everything was [28:01] checked, and and there was no no human [28:04] mistakes uh left. [28:07] And and maybe we'll talk about [28:09] generative AI later, but there's there's [28:11] also now a lot of interest in [28:13] conjunction with generative AI. [28:16] Uh AI is pretty good as that coming up [28:18] with plausible proofs. [28:20] Okay, but then they have to be checked [28:22] by humans. [28:25] Unless uh [28:26] AI writes a proof in one of those formal [28:29] languages like Lean, in which case it [28:31] can be checked by a machine, and that's [28:34] much more much more effective. [28:37] Um [28:38] So, yeah. So, it's it's the idea of of [28:41] using the machine to help you write [28:43] proofs and recheck proofs that you've [28:45] written yourself, or maybe with some [28:47] help from an AI. [28:49] And now those tools can also be used to [28:51] prove properties about programs. [28:54] And so so I I spent uh [28:58] many [clears throat] years uh uh [29:00] proving the correctness of a compiler, C [29:02] compiler, [29:04] uh using one of those tools, the the [29:06] Rock uh proof assistant. [29:09] Um so so basically um [29:12] when I'm proving about the compiler, so [29:14] it takes C code, it produces assembly [29:16] code, and [29:18] um proving that the assembly code is [29:19] faithful to the C code. So so there's no [29:21] miscompilation. The the compiler didn't [29:23] introduce a bug in the program that [29:25] wasn't there originally. [29:28] And and it's a fairly big proof because [29:31] compilers do complicated things about [29:32] programs, and then you have to define [29:34] exactly what it means to preserve the [29:36] semantics of a program. So you have to [29:37] define the semantics of your programming [29:39] languages. And and so so it's all a very [29:42] good use of those uh uh machines [29:46] uh of those proof assistants. Uh [29:49] the the same work could be done on [29:50] paper, but I mean this would be a proof [29:52] of several thousand pages, and nobody [29:55] would want to read it. [29:57] Nobody would trust it. It's just too [29:59] big. Uh and and it would be very hard to [30:01] evolve. Um [30:03] One good thing about [30:05] um those um [30:07] mechanized verifications of of programs [30:09] is that [30:10] uh [30:11] it can also help you evolve the program. [30:13] Okay? You can add new features and so [30:15] on, and and adapt your proofs, and be [30:17] really sure that you haven't introduced [30:19] a regression or things like that. [30:23] Um so yeah, so it's really uh [30:24] programming taken to a higher level. Um [30:28] And and today it's quite expensive. Um [30:31] it takes a lot more time to to prove a [30:34] program than to write it in the first [30:36] place. But maybe this is getting a [30:38] little better. [30:39] Um [30:41] Yeah, and I should also mention another [30:43] great uh of certified software is the [30:46] it's a microkernel, the SEL4 [30:49] microkernel, [30:50] uh developed in Australia, and which is [30:53] used as an hypervisor in in some in some [30:56] applications. [30:58] And so it is uh [31:00] is [31:02] really like 8,000 lines of extremely [31:04] technical C code that that, you know, [31:06] manipulates uh [31:08] uh processes and uh [31:11] capabilities and security tokens and so [31:14] on. And it's been proved correct. Every [31:16] line has been proved correct. And that [31:18] that's a very big achievement. [31:21] >> When you mentioned the example of [31:22] verifying a mathematical proof, that [31:26] uh makes sense to me. When you talk [31:28] about proving something about a program, [31:31] it's a little bit more abstract to me or [31:33] I'm having some trouble visualizing. [31:35] Could you give a concrete example like [31:38] uh maybe some trivial program that we're [31:41] trying to prove something about it and [31:43] how that uh theorem prover would work. [31:46] >> Let's say [31:48] you have a function that takes three [31:49] numbers, X, Y, Z, and um returns the [31:52] average of those numbers. [31:55] Okay? [31:56] Um [31:58] only [31:59] yeah, and and maybe [32:02] you're using a not completely obvious [32:05] formula like uh [32:07] T equals X plus Y and then T equals T [32:10] plus Z and then um T equals T divided by [32:14] 3 and then return T. Okay? So not that [32:17] exactly is the formula for the [32:20] average. [32:22] Uh and you want to prove that that [32:24] function is correct. So so you want to [32:26] prove that [32:28] it it returns uh [32:30] X plus Y plus Z divided by 3. And maybe [32:33] you will have to make it clear whether [32:35] you're rounding up or rounding down. [32:38] If you're using integers or [32:39] floating-point numbers, you know, it's [32:41] not a exact arithmetic, so [32:43] >> [snorts] [32:43] >> um [32:45] So, yeah, you you'll have to to say [32:46] exactly what you mean by divided by [32:48] three. [32:49] >> [snorts] [32:50] >> And then, uh if you are in a language [32:51] like C, you can have arithmetic [32:53] overflows. [32:54] Okay? When you compute X + Y or [32:57] + Z, [32:59] um [33:00] you can overflow the range of [33:01] representable representable integers, [33:03] and in C, it's it's a bug. It's an [33:05] undefined behavior. [33:07] So, typically, you will want to put a [33:10] so-called precondition on your function [33:11] saying, "Okay, [33:13] uh if you call me, call me with numbers [33:15] that are between, I don't know, zero and [33:18] 1 million for instance, but no bigger [33:20] than that." And and then, the prover [33:23] will check that no overflow can occur in [33:26] this case. [33:27] Um okay? And so So, basically, you have [33:31] the precondition that says, "Okay, these [33:33] are safety guarantees um [33:35] that must hold of the parameters, [33:37] otherwise, anything can happen." [33:40] And then, there will be a little bit of [33:42] kind of symbolic execution of the [33:43] function body [33:45] that says, "Okay, when you T equals X + [33:47] Y, then T plus equals Z, then T {slash} [33:50] equals three, then in the end, T is X + [33:52] Y + Z divided by three, provided no [33:55] overflow occurred." [33:58] And then, you put that with a [33:59] precondition that says, [34:01] "There cannot be any [34:02] overflow," and you get your final [34:04] result. [34:05] Okay? So, basically, you're stating a [34:07] contract for your function, the pre- [34:09] hypotheses on the arguments, [34:11] uh guarantees on the results. [34:14] And [34:15] uh and and you want to prove or analyze [34:18] the function body to show that this [34:21] contract is respected. [34:23] I hope it's a little more concrete. [34:25] >> So, it it sounds like a lean will help [34:28] you basically take in some invariants [34:31] about a program and kind of propagate [34:33] them through line by line and uphold [34:36] them. And so you can say something about [34:38] >> Yes. [34:41] Maybe not Lean by itself. Well, a [34:43] program prover a program prover will do [34:45] exactly what you say. [34:47] And for Lean to be able to do it, you [34:49] still need to teach it a little bit [34:51] about the semantics of your programming [34:52] language. [34:54] Okay, that [34:55] what does a plus means, what does [34:59] assignment means, okay? Lean Lean is [35:02] mathematics. You don't assign in [35:03] mathematics. You don't say x equals x [35:05] plus one or or or [35:08] or you're just comparing x and x plus y [35:10] and it's always false. There's no [35:11] assignment in mathematics. There's [35:13] assignment in many programs. So you need [35:16] to [35:17] make it explicit that [35:19] there are [snorts] actually three [35:20] different states for the t variable, [35:22] three different values and and [35:26] and relate [clears throat] those values [35:27] to [35:29] Well, the program defines what those [35:30] values are and then a prover like Lean [35:33] can can reason about those three [35:35] successive values. [35:37] Because now you're in you're in [35:38] mathematics. [35:40] And and that that kind of bridge between [35:43] programs and their mathematical meaning [35:46] is called semantics. That that the field [35:48] of semantics of programming languages [35:51] has been a big topic in in PL research [35:53] since the the '60s at least. [35:56] >> Am I understanding then that [35:58] like a pure functional programming [36:00] language, the gap between mathematics [36:03] and [36:04] the actual symbols is much smaller than [36:07] an imperative? [36:08] >> Absolutely. Yeah, you're you're [36:10] absolutely right. [36:12] And that's one of the reasons why [36:15] people who do formal methods don't like [36:17] assignment, don't like imperative [36:18] features. [36:20] Purely functional style is much closer [36:22] to mathematical style, so much easier to [36:24] reason going [36:26] There can still be few discrepancies [36:28] between the program and the math. Uh, [36:31] for instance, functional programs may [36:32] not terminate. [36:33] They may loop forever. Um, mathematics [36:36] doesn't like that. So, so you need a way [36:38] to to reason about termination. [36:41] Um, and uh [36:44] and also yeah, sometimes for instance, [36:47] the the arithmetic you get in the [36:48] programming language is not [36:50] uh, integer arithmetic or is not [36:53] uh, real reals. [clears throat] You [36:55] know, it's floating point, it's not [36:56] reals. So, so you still have to [36:59] uh, account for that [37:01] gap. Uh, but you're you're absolutely [37:03] right that the gap is much shorter for [37:06] functional programming. And and uh [37:10] in the experience of CompCert, my my [37:12] verified compiler, [37:13] I think the the first decision was to [37:15] write it in a purely functional style [37:18] so that it would be easier to to reason [37:20] about it later. [37:22] >> You mentioned the the specifications [37:24] that we could prove, and one of them was [37:27] proving that the program terminates, but [37:29] I thought that's a famously [37:32] difficult or impossible. I forgot [37:33] exactly that the halting problem, right? [37:35] So, how how is that something that you [37:37] could prove? [37:39] >> Okay, so what the [37:41] um computability theory says is that [37:43] there is no algorithm that will always [37:46] that can always say [37:48] this program terminates or this program [37:50] doesn't terminate. [37:51] Um, [37:52] so so there will always be some very [37:53] weird programs for which your your [37:57] analyzer your your automatic termination [37:59] analyzer will produce a wrong result [38:02] or will not terminate itself. [38:06] Uh, so it will not work. [38:08] Um, uh but [38:11] still for for many programs, you can [38:13] succeed. Okay, you can write automatic [38:16] termination analyzers that will work for [38:18] a large uh class of programs. [38:21] And then the termination analysis, [38:23] termination proof can also be done by [38:25] hand by by a mathematician. Okay, so [38:30] So, perhaps [38:32] a human can can see through those weird [38:36] Turing programs that that are hard to [38:38] prove to terminate and [38:40] and and recognize the trick. [38:43] But, anyway, so yeah, it's a hard [38:44] problem and all all program verification [38:47] tasks are are difficult pro [38:49] problems, okay? Uh [38:52] They are pretty much all undecidable. [38:55] So, you know that there there is no [38:57] static analyzer that will always [38:59] find all problem all problems in all [39:02] programs. [39:03] >> [snorts] [39:03] >> But, still you can try, okay? You can [39:06] try for specific problems, for specific [39:08] programs and and get some very useful [39:11] results out of them out of that. [39:13] You only need to be able to do it for [39:15] the cases that are of interest to you, [39:17] the programs you really care about. [39:20] >> OpenAI, Anthropic, Cursor, and Vercel [39:23] all use this product to make their lives [39:25] better. [39:26] And the problem it solves is when you're [39:28] building SaaS or an AI product and you [39:30] want to sell to other companies, there's [39:32] all these requirements you need to meet. [39:34] There's SSO, there's SCIM, there's RBAC, [39:38] there's audit logs. These are all things [39:40] that take time to integrate, but aren't [39:42] the main focus of your app. WorkOS is an [39:44] API layer that lets you meet all of [39:46] these requirements in just a few lines [39:48] of code. So, let's say you have a new [39:50] SaaS product and you want to sell to [39:52] other companies, WorkOS will solve all [39:54] of these critical feature gaps for you. [39:57] You can check them out at workos.com to [40:00] learn more and get started. And I [40:02] appreciate them for supporting my work [40:04] and sponsoring this podcast. One thing [40:06] [snorts] I saw when I was researching [40:07] OCaml is that [40:09] uh in 2022, OCaml added multicore [40:13] support. And but from my memory, I [40:16] remember multi-core processors became [40:19] standard much earlier than that. And so, [40:21] I figured there might be some unique [40:23] engineering challenge in adding that [40:25] support. So, yeah, what what happened [40:27] there and what made it difficult? [40:29] >> Uh well, there were [40:31] engineering challenges, that's for sure. [40:33] There there were also some language [40:34] design issues. [40:36] So, so but let's talk about the [40:38] engineering challenges first. [40:40] Um so, it's true that that when you have [40:42] a a language with with a runtime system [40:45] memory allocator or garbage collector [40:48] uh [40:49] well, at least the one of for for OCaml [40:51] was really designed with sequential [40:53] executions in mind. [40:55] So, if you have if you add a shared [40:57] memory concurrency, then you need a [41:00] garbage collector or a memory allocator [41:01] that that that that can work [41:03] concurrently. And that's actually quite [41:05] difficult. [41:06] Uh at least if you want them to be fast. [41:09] Of course, you [41:11] you could always, you know, take take [41:12] take a lock at at every operation in the [41:15] heap, but then uh you would [41:17] sequentialize your programs. Basically, [41:19] they they they would run as slowly as a [41:21] single processor. So, so that's not [41:24] interesting. So, yeah, so there were [41:25] engineering challenges. Um um yeah, I [41:28] was at least initially quite quite [41:30] reluctant to [41:32] uh basically re-implement a complete uh [41:36] garbage collector and and uh memory [41:38] allocator or large parts of the runtime [41:40] system. That's what we did eventually [41:42] with uh as well, it was done mostly by [41:45] the team at OCaml Labs at Cambridge [41:47] University. [41:48] >> [snorts] [41:48] >> Uh but yes, it was a really big rewrite. [41:53] Um but then I said there's also a [41:56] language design issue. [41:58] Which is that for for the longest time [42:01] well [42:02] uh [42:03] is [42:04] now when when you say uh [42:06] multi-core [42:09] processors and so on, pretty much [42:10] everyone [42:11] and language support for multi-core [42:13] processors, everyone thinks about [42:16] language support for shared memory [42:18] concurrency. [42:19] You know, this model where you have [42:20] several sites of control and they access [42:23] the same memory [42:24] and basically the sites communicate by [42:26] modifying the memory and someone else is [42:29] going to notice. [42:31] You know, it and [42:32] I've never liked this model of of [42:35] communication. [42:38] I mean, it's a bit like if you want to [42:40] communicate with your neighbor then then [42:42] you you you break into their houses and [42:44] their house and then you move the [42:46] furniture around and then when they are [42:48] back they say, "Oh, something something [42:51] was moved so it's probably Iron who's [42:53] trying to tell us something." [42:55] Maybe you could just meet your [42:56] neighbors, you know? And and that would [42:58] be things like message passing [43:01] which is a completely different form of [43:02] communication, much higher level. [43:05] So, yeah, so for the longest time I was [43:07] really interested in message passing [43:10] concurrency. [43:12] And there's for instance a functional [43:15] language called Erlang that was built on [43:18] around those ideas and that I found [43:20] quite interesting. [43:22] However, I never got to to have a [43:24] decent language design and [43:28] everyone was saying, "No, but but it [43:30] it's it's too costly. It's not [43:32] effective. There's too much copying of [43:34] data. [43:35] With shared memory you can you can share [43:37] some kind of huge database in memory. If [43:40] you don't modify it too much, then [43:42] basically the sharing is the the [43:44] concurrency is free. [43:46] While with message passing we'll have to [43:48] exchange a lot of data so [43:50] to to get the same effect so so you will [43:52] pay more for it. [43:53] Anyway, [43:54] so [43:55] so okay, so [43:57] starting with Java I guess and then C [44:00] C++ 2011 there was this idea that okay, [44:04] we we we need to expose shared memory [44:06] concurrency to the programmers. [44:09] But then comes the problem of the memory [44:10] model, which is that [44:12] what happens when there's a race, for [44:15] instance, when when two [44:17] uh two threads want to access the same [44:20] uh location, and maybe they want to [44:21] modify it in different ways. [44:23] And so, sometimes parts of the C C++ [44:27] standard says, "It's undefined behavior. [44:29] Anything can happen." But still, you [44:31] need to give a little more guarantees. [44:33] Uh at the other end of the spectrum, [44:35] there's a so-called uh sequential [44:36] consistency, which says, "Well, what [44:38] happens is like an interleaving of reads [44:41] and writes of your program." [44:43] You don't know which interleaving, but [44:44] there is an interleaving. [44:47] But that doesn't work with modern [44:50] uh processors, multi-core processors. [44:52] They reorder memory accesses in in very [44:54] clever ways to get more performance. And [44:57] so, viewed from the program, it's very [44:59] hard to predict what they are actually [45:00] doing. [45:01] And so, you need to give your [45:03] programmers, when you're designing a [45:04] language with shared memory concurrency, [45:06] you need to give your programmers some [45:07] guarantees about uh the ordering of [45:11] reads and writes, concurrent reads and [45:12] writes, while not constraining the [45:14] hardware too much. [45:17] And it's very difficult. So, Java went [45:20] through like five different iterations [45:22] of the memory model. Some were too [45:23] strict, some were too lax, some were [45:25] kind of in [45:27] inconsistent. They were were were making [45:29] predictions, impossible predictions, [45:31] where where the past depends on the [45:32] future. [45:34] >> [snorts] [45:34] >> Crazy, really crazy stuff. [45:37] Uh then C C++ 11 did a little better, [45:40] but still extremely complex memory [45:42] model. And so, when we wanted to add [45:44] when the especially the OCaml Labs [45:46] people wanted to add uh shared memory [45:48] concurrency to OCaml, we had to also [45:51] agree on a memory model [45:53] that would be [45:54] exposed to the programmers. [45:56] And and that's also took quite a bit of [45:58] a design uh quite a bit of time to come [46:01] up with a good design. Uh [46:03] And I [46:04] I think it's it's [46:05] better and easier to understand and use [46:08] than the one of Java, but the the OCaml [46:11] memory model is still quite complicated. [46:14] And [46:15] And sometimes I feel sorry our users are [46:18] are exposed to that. Okay. Uh [46:21] Uh [46:22] So, that that that explains why it took [46:24] so long. [46:25] Solving the [46:27] engineering challenges, but also [46:30] having a [46:31] agreeing on the memory model and what [46:33] kind of guarantees we're going to give [46:34] to programmers. [46:36] Oh, yeah. I forgot to say one thing, [46:38] which is that [46:40] So, C and C++ there's a lot of things [46:42] you can say, "Oh, it's just undefined [46:44] behavior or anything can happen." [46:46] In type-safe languages like Java and [46:48] OCaml, you want to give stronger [46:49] guarantees. Okay. Maybe many things can [46:53] happen, but your data should should [46:55] remain well-typed. [46:57] Okay. Typically, you don't want to [46:59] expose an object to another thread [47:02] before it's been fully initialized, for [47:03] instance. [47:04] Um And And that's that's actually very [47:08] hard to guarantee in your memory model. [47:10] And then [47:12] you have to implement that memory model, [47:13] so your compiler also needs to take [47:15] extra [47:16] precautions to to to guarantee this. So, [47:19] yeah, type safety in the presence of [47:22] shared memory concurrency is is not [47:25] obvious at all. [47:27] And so, that's why it took so long. [47:30] >> So, in Python, I know there's the famous [47:32] GIL or the global interpreter lock. What [47:35] is that lock protecting? Is it the the [47:37] cleanup of objects on the heap or is it [47:40] something else? [47:41] >> Among other things, yes. So, yeah, we we [47:44] had the same thing in OCaml before [47:46] before [47:47] multicore OCaml with [47:50] >> [snorts] [47:51] >> with Marstin. So, yeah, well, basically, [47:53] the idea that when when your runtime [47:55] system is not thread-safe, as we said, [47:57] you can protect the non-thread safe [47:59] functions by your lock so that [48:02] they will never be executed [48:03] concurrently. [48:04] But if you take the lock at every [48:06] allocation and release it, [48:08] you take and release the lock for every [48:10] allocation and it's just too slow [48:11] anyway. [48:12] And so the idea is that [48:15] you take the lock when you enter Python [48:18] code, let's say, and you start executing [48:20] Python code. [48:22] But you can still release it when you do [48:25] input output for instance, when you're [48:26] going to block for a long time. [48:28] Or when you're calling into C code that [48:31] that [48:32] that is thread safe and is not going to [48:34] use your runtime system. [48:36] Then you can release the lock and some [48:38] other [48:39] Python thread can take it and execute. [48:42] So you get a little bit of concurrency. [48:44] You can overlap computations in your [48:47] high-level language with IO or [48:49] computation is a low-level language in [48:51] another language. [48:53] But you still have mutual exclusion [48:54] between your [48:56] between two threads running Python or [48:59] running OCaml before before multicore [49:01] OCaml. [49:03] So so you get some benefits like [49:07] concurrent IO, but you don't get any [49:08] parallelism. [49:09] Okay, yeah. You don't get a speed up for [49:12] computations. [49:14] And so so yeah, so we used to have this [49:17] this this GIL in in in OCaml as well. [49:20] And [49:22] so you can get rid of it, but in [49:24] general, you need to redesign at least [49:26] the garbage collector and and memory [49:29] allocator. [49:32] There's probably a few places in the [49:34] OCaml runtime system that still use [49:36] locks to [49:38] to to ensure mutual exclusion like in [49:40] the IO subsystem. [49:44] And and some phases of the garbage [49:46] collector, I think that there's a phase [49:48] which is kind of stop the world where [49:50] you need to make sure that everyone [49:53] no no no camel code is is running. [49:56] So for a short time you need to make [49:57] sure that everyone is stopped and then [49:59] do a little bit of work to finish the GC [50:02] and then you can restart everyone. [50:04] Um so yeah, that these are tricky things [50:07] and I don't know what the Python people [50:08] are up to with their GIL if if they [50:10] finally managed to remove it or [50:13] they're still working on it but I I I've [50:15] heard they're making progress. So. [50:17] >> Yeah, you mentioned Python calling into [50:21] C and I've seen that pattern before of a [50:24] higher level language interfacing with a [50:26] lower level one. How does that binding [50:29] typically work? [50:31] >> Oh, it's another can of worms. [50:33] Um [50:36] Um [50:38] Well, there are two aspects. There are [50:39] there are the the control flow and there [50:41] are the [50:42] the data. [50:43] So the control part is is [50:47] not that hard. So yes, you need you need [50:49] a mechanism so that your your Python [50:51] interpreter or your OCaml compiled code [50:53] will actually jump to the C function. [50:57] Uh so for OCaml basically you you tell [50:59] your OCaml compiler that this function [51:01] is not implemented in OCaml, it's [51:03] actually implemented by a C function and [51:05] you give its name and then the compiler [51:07] will emit a call to the C function using [51:09] the C calling conventions which are not [51:11] exactly the same as the OCaml calling [51:13] convention but [51:14] the compiler knows about that. And so it [51:17] will [51:18] call the C function maybe through a [51:19] little bit of glue code or whatever and [51:22] then the C function will execute and and [51:25] return back to the OCaml code. [51:28] Um [51:30] That's relatively easy. Uh now the hard [51:33] part is uh data [51:35] uh like function arguments and function [51:37] results [51:39] because OCaml and C have different data [51:42] representations. [51:43] Uh for instance, a floating point number [51:45] in in OCaml is generally boxed, so it's [51:48] allocated in the heap and handled [51:50] through a pointer. So, it's more like a [51:52] double star in in C [51:55] and it's not a double, which is not [51:57] allocated. [51:59] Just it's in a register. [52:01] Um so [52:03] so typically the C code needs to use a [52:06] so-called foreign function interface, so [52:08] some C function and macros provided by [52:10] OCaml to access the OCaml data, the [52:13] OCaml arguments, you know, extract the [52:15] part that it needs, the the numbers, the [52:19] uh [52:20] uh yeah, another example is arrays. Um [52:23] in OCaml when you have [52:25] a two-dimensional array, it's actually [52:26] an array of arrays. So, viewed from C, [52:29] it's an array of pointers to arrays. [52:31] While in C, an array of arrays is [52:33] there's no intermediate pointer, so it's [52:35] not the same representation. And so, you [52:37] have to explain to C or give C some [52:39] functions and macros to to access uh [52:43] elements in OCaml arrays. Uh it's not [52:45] exactly the same code that that that [52:48] that that you would do to access a C [52:50] array from C. [52:52] Okay, so you need accessors, but now if [52:55] you want to uh [52:57] if your C code wants to return some [52:59] complex results like a list, an array, [53:02] and so on, it needs to allocate it in [53:04] the OCaml heap. So, it needs to ask the [53:08] runtime system to do some heap [53:10] allocation and then fill the uh [53:12] >> [snorts] [53:12] >> heap blocks correctly. And then this [53:15] allocation can can trigger a garbage [53:17] collection, so the C code that also kind [53:20] of cooperate with a garbage collection [53:23] with registration mechanisms, etc., etc. [53:26] So, so there's quite a bit of work to to [53:28] be done. [53:29] And and uh and then different foreign [53:32] function interfaces [53:34] arrange this work differently. So, [53:36] there's a base FFI for OCaml, basically [53:39] uh it's a C code that must do all the [53:41] work. [53:42] But but then it can be very fast and [53:45] quite optimized. [53:46] Uh but there are other FFIs like the C [53:49] types FFI in OCaml where most of these [53:51] data conversion and and mediating [53:53] between two data formats is automated. [53:56] Uh you start basically with a [53:58] description of the the the the the C [54:00] type of the C function and and you can [54:03] automate some of those conversions. But [54:05] sometimes it can be tricky it can be [54:06] expensive. For instance, [snorts] you [54:08] may end up copying the whole array while [54:12] your C code only needs to access two or [54:13] three elements in it. [54:15] Um okay. So there's lots of trade-offs. [54:18] And quite frankly it it's a dirty part [54:22] of of programming language [54:23] implementation. Uh the the OCaml FFI is [54:27] not that clean, but if you look at the [54:29] Java FFI for instance, it's also quite [54:31] complicated. And for Python I've I've [54:34] never tried. Uh so I I don't know what [54:37] it looks like. [54:39] Uh [54:39] but yeah, it's a it's a necessity. [54:42] Uh but but it can be quite hard because [54:44] the data models are different between [54:47] the two languages. [54:49] >> So to kind of get the big picture, on [54:52] the OCaml side, there's an interpreter [54:55] which is a program running in [54:57] application space that is interpreting [55:00] your OCaml code. And then at some point [55:03] in the OCaml code, it says [55:06] do some, you know, load this C program. [55:09] And the C program is a binary somewhere. [55:12] And the OCaml interpreter then starts to [55:16] load those instructions and execute [55:17] them. [55:18] >> Okay. So actually this is the third [55:20] aspect that I didn't touch. [55:22] So so OCaml well, there's an interpreter [55:25] mode, but in general we compile. We [55:28] compile to assembly code and then [55:30] machine code. [55:32] And so [55:33] so in in in compiled mode, [55:36] what what you say is [55:39] how you put together the OCaml code and [55:41] the C code is done by the the linker, [55:44] the C linker. So so [55:46] So basically someone else is doing that [55:48] for us. And and and it's not that [55:51] different from linking together two [55:55] object files produced by C or two object [55:58] files produced by OCaml. [56:00] But you write that for for more [56:02] interpreted [56:04] languages, there's also the question of [56:05] how you load the C code. [56:07] Generally you know you use the dynamic [56:10] loading like interface dlopen for [56:12] instance in in in Unix. [56:17] So and and and then there's a little bit [56:19] of introspection. So so at at run time [56:22] the interpreter will query the C [56:24] libraries and where is the address of a [56:26] function named foo? And then it will [56:29] find the address and use that to [56:30] manufacture a call. So yeah, if you're [56:34] in an interpreted setting or [56:36] or bytecode compiled setting like [56:38] Python, it's there's this additional [56:40] level of complexity on top of it. [56:44] >> I see. I see. Okay, so if I had a mixed [56:48] OCaml C program [56:50] to my computer it's just one binary or [56:54] one one blob. [56:56] >> In in in the simplest case, yes. [57:00] There are also dynamic loading [57:02] facilities in OCaml, but I don't want to [57:04] get into that because I'm a firm [57:06] believer in static linking. I think [57:08] programs should be statically linked so [57:11] that there's no surprise when you run [57:13] them. Okay, like oh, where is this DLL [57:16] or DLL not found for instance problems. [57:19] But [57:21] of course you lose a little bit in [57:22] flexibility. [57:26] But yeah, I think the static static [57:28] linking has a lot to [57:31] is is actually quite useful in in that [57:34] it it guarantees a lot of things. It [57:36] checks a lot of things at link time that [57:37] you [57:38] don't have to check again at run time. [57:41] >> We mentioned earlier in the conversation [57:43] talking a little bit about LLM generated [57:45] code. I thought that might be [57:46] interesting to cover. Um and in one [57:49] interview you talked about the danger of [57:53] almost correct code. So, plausible code [57:55] but it's it's wrong that an LLM can [57:57] produce. And what are your thoughts on [58:01] you know how to address that kind of [58:02] problem? [58:04] >> It's it's it's a tough problem. I mean [58:07] you [58:08] um [58:09] globally I'm a little bit skeptical [58:11] about generative AI. Oh, of course they [58:14] they they [58:15] they can do amazing things that were [58:17] unthinkable like a few years ago. [58:20] But there's also [58:22] there's always some errors. Okay. It's [58:25] it's [58:26] you can't really trust [58:28] oh [58:29] what's what's being produced by by [58:31] generative AI. [58:33] And so [58:35] the the [58:37] uh [58:38] in principle humans should be there to [58:41] check the output and [58:44] and fix errors or ask the LLM to fix its [58:48] own errors [58:49] until the result is actually usable. But [58:52] of course it's very hard because well [58:54] there's a slot problem. Okay. [58:56] AI's produce so much it's so it's so [58:59] easy to produce [59:01] uh [59:02] to produce large number large quantities [59:04] of text of code or pictures or whatever [59:08] that that that in the end [59:10] there's there's there's no human [59:14] no no no human time to to check it all. [59:18] So, [59:20] recently I heard a [59:22] uh well someone working in an AI startup [59:24] who was enthusiastic about [59:27] uh [59:28] AI generated code thing that thanks to [59:30] Genady AI is a cost of programming is [59:33] dropping to zero. [59:35] But well, the cost of writing code [59:37] maybe, but [59:39] what about you know checking it, [59:42] making sure it is correct, um [59:45] that it does what we want, that [59:47] well, that cost is not zero at all. [59:50] >> Uh-huh. [59:50] >> And and for me [59:52] every new line of code is a liability. [59:54] So you you have to test it, you have to [59:57] check it, maybe you have to do formal [59:59] verification. You have to [60:02] evolve it, maintain it later. So so no, [60:05] I don't want huge amounts of code, okay? [60:07] I want I want [60:09] 50 lines of code that have been [60:11] thought that have been polished over the [60:13] years. [60:14] So anyway, I'm not getting that with AI. [60:18] And and and I think that's the problem. [60:22] And this idea that humans will be there [60:24] to check the output of Genady AI is just [60:28] wrong. [60:29] No, they they they are not available for [60:31] that. They [60:32] There's too much of it and it's [60:35] and it's [snorts] not it's not pleasant [60:37] either, okay? I mean, I don't think it's [60:39] a good way to to to split the work [60:41] between machines and and humans. [60:44] So anyway, so maybe there will be some [60:46] social [60:48] solution like big [60:51] >> [snorts] [60:51] >> no to AI slop movements. So we we we're [60:53] trying to see that in some open source [60:56] projects that that refuse AI generated [60:59] contributions because there's just too [61:01] many. [61:02] >> [snorts] [61:02] >> I know that well for for for OCaml and [61:05] especially for Coq Certified have have [61:07] received some uh [61:09] uh issues, a lot of issues that were [61:12] obviously generated by AI. And there was [61:15] maybe one good issue among 10 reports, [61:18] okay? And and and each report was [61:20] several page long and it's, you know, [61:23] very detailed explanations, and repro [61:26] case that in the end doesn't repro [61:28] anything or repro reproduces something [61:30] else. And but but it takes time to to go [61:33] through all those things, and and maybe [61:36] at some point I will say no to to AI [61:38] generated contributions. [61:40] Okay. But maybe there's also a bit of a [61:42] technical solution, [61:44] which is, as as we said earlier, [61:48] to have AI produce proofs, [61:50] so evidence that [61:53] its creation is correct. So, as I said, [61:55] this is starting to work for [61:58] mathematical proofs. Some generally the [62:00] AIs are able to produce proofs both in [62:03] English and in the formal language of [62:06] the Lean prover, for instance. And so, [62:08] you can get [62:11] a Lean to recheck the proof and get some [62:13] confidence. You still need to be very [62:15] careful about the statement, [62:19] because sometimes [62:21] AIs will change the statement or the [62:23] definitions to make the proof easier. [62:27] That happens. [62:29] And [62:31] also, you you should be careful about [62:33] so-called self-formalizations, where the [62:36] the AI also comes up with some [62:38] definitions and some statements [62:42] by parsing a PDF file or whatever, and [62:45] and sometimes it introduces errors at [62:46] that point. [62:48] So, anyway, there's still need need for [62:50] human review, but [62:52] on smaller quantities of of text and and [62:55] mathematical text. [62:58] And maybe one day it will also work for [63:00] program proof. So, when an AI generates [63:03] a program, it might it be able to [63:05] generate some Lean proof or whatever, [63:08] that that the program satisfies some [63:10] specification. [63:12] Um [63:14] So, I I think it is possible. [63:17] Um but now the question will be where [63:19] does the specification come from? [63:22] It's always been a big issue for formal [63:23] methods. [63:26] It's not just that verification is hard, [63:28] but agreeing on the spec can be [63:31] can be difficult, too. [63:33] And well, mathematicians [63:35] have a lot of experience, you know, in [63:38] in stating [63:40] finding a definition that they find [63:41] interesting and stating theorems that [63:44] that that [63:46] that they believe [63:47] should be true or or or that that will [63:50] um [63:51] mean something. [63:53] Computer programmers are less good with [63:56] that. And it's fairly easy to come up [63:58] with specifications that are [64:00] inconsistent for instance or impossible. [64:02] Uh so, remember this this average [64:04] function [64:05] where there was a a precondition of the [64:07] three numbers three arguments saying [64:09] they must not be too big. [64:11] But say [64:13] maybe you you can end up with a [64:15] precondition that that just cannot be [64:17] satisfied. [64:20] And and [64:22] and and at this point, the body of the [64:24] function will always be verified, okay? [64:27] Even if it's completely wrong because [64:28] because the assumption says [64:30] basically this function cannot be [64:32] called. [64:33] Um and and so, you get a false sense of [64:35] confidence. [64:37] Okay, you verified something, but but [64:39] it's actually unusable. [64:42] And and and that that's a fairly [64:44] delicate point [64:46] where I'm not sure LLMs are going to or [64:49] AI is going to help much. [64:51] Uh [64:52] but but it's a problem with formal [64:53] methods in general. And and some [64:56] possibilities include [64:58] uh [64:59] the ability to test specifications for [65:01] instance. [65:03] Um [65:04] so, instead of using your test suite to [65:07] to to see if your code works out, you [65:10] can also use it to see if your spec um [65:13] um [65:14] it checks out. Um [65:17] those kind of things, but um [65:20] yeah, we we're kind of moving some of [65:21] the difficulties from the programming [65:23] phase to the uh specification phase, but [65:26] we still have some problems. [65:30] Anyway, so that might be a way to to [65:32] deal with the um [65:34] uh AI-generated code and and and develop [65:37] some confidence in it. [65:39] >> You know, LLM-generated code is becoming [65:41] extremely popular, and I think there's a [65:43] lot of potential downstream consequences [65:46] on this on the programming language uh [65:49] landscape. [65:51] And I thought it might be interesting to [65:53] hear your thoughts on speculating. Like, [65:55] imagine 10 years from now, if you took [65:58] LLM-generated code and turned it up, [66:01] how might you think that the programming [66:05] language [66:06] landscape might change? [66:08] >> Yeah, a couple of years ago uh someone [66:10] asked me about that, and and there was [66:13] there was a a concern that the training [66:15] data would be um there wouldn't be [66:18] enough training data in OCaml [66:21] uh for for an LLM to really learn how to [66:24] program in OCaml. [66:25] And it's true that there's less OCaml [66:27] code in the wild than uh JavaScript [66:30] code, for instance. [66:31] Uh but apparently [66:34] um uh contemporary LLMs do do do well [66:38] with with uh the amount of uh of OCaml [66:41] code uh [66:43] they have. [66:44] Uh [66:45] maybe because there's enough, maybe [66:47] because learning has become a little [66:48] more efficient, maybe because uh well, [66:51] there's there's there's less OCaml code [66:53] than JavaScript code, but maybe the [66:55] OCaml code is better quality average [66:58] on an average. I don't know. Anyway, uh [67:01] maybe LLMs are getting better also to to [67:03] transfer knowledge from that they've [67:05] learned from one language to another. [67:08] That that could be. Um I have no idea [67:10] how those things work. [67:12] But yeah, so so the latest feedback I've [67:14] got about LLMs and [67:17] well, yeah, [67:18] generative AI and OCaml is that the the [67:20] OCaml code generated is is quite decent [67:24] and quite similar in quality to [67:27] to more popular languages. [67:30] And one thing that seems to help the [67:33] generative AI is a type system. So the [67:36] fact that there's some static checking [67:38] just of the types uh [67:41] uh it's already uh effective in, you [67:43] know, the [67:45] uh avoiding some some errors and maybe [67:49] uh encouraging the LLM to like like [67:52] declare types [67:54] uh first. Um so so give give some type [67:57] structure to the program. [67:59] All right. [68:00] Um [68:01] And now from 10 years from now, [68:04] it's it's it's difficult to guess. So, [68:07] will it be the more the more popular [68:09] languages of today that will be even [68:11] more popular because of generative AI? [68:15] Will it be the safer languages of today [68:18] that will be more popular with AI [68:20] because uh [68:22] well, because there's fewer errors in [68:24] the end? [68:25] Um I'm hoping it will be the the safer [68:27] languages, but uh [68:30] I really don't know. [68:31] >> I've seen in the industry, there's a few [68:33] cases where because it's so easy to [68:36] generate code, uh massive rewrites are [68:41] something that would have been very [68:42] infeasible in the past are very [68:45] realizable now. So, if there's an [68:48] existing project where they chose a [68:51] programming language for whatever reason [68:53] in the past, they could translate the [68:56] entire thing into another language [68:59] with reasonable confidence. Given that [69:01] kind of environment, which programming [69:04] languages would you expect more people [69:07] would switch to because they they want [69:09] to switch to it but they weren't able to [69:11] in the past but now it's cheaper so they [69:12] can. [69:13] >> Well, so today [69:15] it seems I've heard mostly about C and [69:19] C++ to Rust [69:21] translations [69:22] hoping that the generated Rust code will [69:25] be safer. [69:27] He said I've seen at least one project [69:29] when the generated Rust code is entirely [69:32] in unsafe blocks. So so it's really kind [69:34] of line by line translation of the C [69:36] code, you know, it's [69:37] but well, [69:39] but maybe it can still be used as a [69:41] starting point for making it safer [69:43] later. [69:44] So [69:46] yeah, I would say today [69:48] I can imagine [69:50] significant efforts being being done [69:52] with Rust as the as a target language. [69:56] In the functional world, I'm not quite [69:58] sure. Well, maybe or well [70:01] >> [snorts] [70:01] >> maybe functional language to one of [70:05] those proof assistants [70:07] like like Lean or Coq because they they [70:09] also have [70:11] programming languages functional [70:13] programming languages in them much more [70:15] restricted but much more amenable to [70:17] proofs. So [70:19] maybe for a few projects that that could [70:21] be interesting as again as a first step [70:24] towards a formal proof as we as we said [70:27] earlier. [70:28] >> When you compare industry versus [70:30] academia, [70:32] today where would you say most of the [70:34] innovation in programming languages [70:36] comes from? And also has that changed [70:38] over time? [70:41] >> Okay, well, I think the [70:44] most of the innovations [70:46] have come from industry lately. [70:49] And that wasn't the case in the early [70:53] days of computer science. [70:55] If you think of I mean, the the totally [70:58] innovative languages like like Algol, [71:02] Lisp, [71:03] uh [71:04] um [71:06] Prolog, uh Smalltalk were were developed [71:09] in mostly academic settings. Well, [71:11] Smalltalk was Xerox PARC, which was an [71:13] industrial research lab, but very very [71:15] far away from [71:17] uh industrial customers. [71:18] Uh and then there were, you know, much [71:21] more [71:22] uh practical languages and ugly uh [71:25] uglier languages developed typically at [71:27] IBM like Fortran, COBOL, PL/I, etc. [71:32] Um and then um [71:34] so so really the idea that the the the [71:36] nice ideas come from academia and and [71:39] mature there. Uh [71:42] And then uh well, the nice ideas from [71:44] academia started to to be transferred by [71:47] industry much much more quickly. I'm [71:50] thinking of well, C and especially C++ [71:53] and then Java, which really uh took uh [71:57] ideas like object-orientation and uh [72:00] well, garbage collection, automatic [72:02] memory management uh in in [72:04] um in industry. [72:07] All right. Before Java, it was just, you [72:10] know, uh crazy academics in the ivory [72:12] tower that were using garbage collected [72:14] languages, right? It was completely [72:17] impossible to have that in enterprise [72:19] compu- computing. And Java came and 2 [72:21] years later everyone was doing garbage [72:23] collection and [72:25] being very happy about it. [72:26] >> [snorts] [72:26] >> Uh and then there were well, Java also [72:29] popularized type safety um [72:32] bytecode verification. Well, some some [72:34] pretty advanced techniques of the '90s. [72:37] And if you look at further developments, [72:40] uh [72:40] I don't know, Swift for instance [72:42] popularized the idea of algebraic data [72:44] types and pattern matching. Uh and then [72:47] Rust uh and [72:49] uh Uh, well, Rust is even more [72:52] spectacular, I would say, because uh, [72:54] well, algebraic data types, garbage [72:56] collections, etc., those were already [72:57] present in in academic languages like, [73:00] well, Camel, for instance. But, uh, [73:03] Rust really took very recent research [73:05] results of the 2000s and safe low-level [73:08] programming that were basically never [73:10] implemented in any language, and managed [73:14] to do a a consistent whole, [73:16] uh, from that. [73:17] And so, I'm I'm really admiring it. [73:20] And I have the impression that [73:22] well, uh, [73:24] uh, I would have loved if if Rust came [73:27] out of academia, uh, but I'm not sure it [73:29] would have been possible, because it's [73:31] also a huge effort, and you really need [73:34] uh, [73:35] the backing of of a big, uh, company. [73:38] But, still, I'm not I'm not sad because, [73:41] uh, [73:41] I think it's also a very good sign that [73:43] industry is interested in new [73:45] programming languages. [73:47] You know, at at some point, [73:50] in in the '90s, well, pretty much when I [73:51] was hired uh, at INRIA on a research [73:54] position, uh, [73:56] uh, when I was hired as someone who had [74:00] developed uh, [74:01] first versions of OCaml, well, [74:03] predecessor of OCaml, and who was [74:05] working on type systems for programming [74:06] languages, and so on. [74:08] Uh, but then some people told me, but [74:10] there's no future in programming [74:11] language research, right? Industry has [74:13] decided it will be C++ forever. [74:16] So, deal with it. Uh, maybe maybe you [74:19] could do software engineering, and not [74:21] not not PL research. [74:23] Uh, [74:25] and then Java came a few years later, [74:27] and and showing that no, uh, [74:30] industry hasn't [clears throat] decided [74:32] on a functional on a on a particular [74:34] programming language. Industry is still [74:36] in interested in new programming [74:37] languages. Industry still thinks that a [74:41] new programming language can be part of [74:42] the solution to to software problems. [74:45] And and I find it extremely encouraging. [74:47] We are not stuck with with bad languages [74:50] from the past. Well, there's a lot of [74:52] legacy code, of course, but but they're [74:54] still [74:55] uh um [74:57] real interest for for for better [74:59] languages, and I think this will [75:01] continue, and I think it's good for for [75:03] the computing field. [75:06] >> In 2018, there was a interview that you [75:08] did, and they asked you what are the [75:10] most interesting and important problems [75:13] to focus on in the coming years. [75:15] And you called out the difficulty of [75:17] programming, you know, GPUs, cuz they [75:20] were using dialects of C, shoddy tools, [75:23] and also the challenges in verifying [75:26] machine learned code, basically. Um and [75:30] that sounds pretty relevant today, but [75:33] what would you say your answer is today? [75:35] >> So, yeah, I think well, for for the um [75:38] um the question of how we program [75:40] massively parallel hardware, [75:43] I think we we've made a little bit of [75:44] progress recently with things like the [75:47] uh MLIR initiative um [75:51] on the on LLVM, or some domain-specific [75:54] languages uh like Halide, which are [75:57] pretty good. You know, those tensor uh [75:59] domain-specific languages for tensor [76:00] computations are getting a little [76:02] better. [76:03] Um but still, I find it a little bit [76:05] frustrating that I cannot do uh I don't [76:07] know, theorem proving on a GPU. Uh I [76:10] have absolutely no idea how to go about [76:12] that. [76:13] Uh and in part by by by lack of uh an [76:17] appropriate language, okay? Uh [76:19] uh [76:20] So, I'm I'm not ready to program the GPU [76:24] pipelines [76:25] at the very low level myself, so [76:28] So, and and I think it's more general. I [76:30] think we're we're not using uh all these [76:34] GPU and other highly parallel hardware [76:36] as much as we could. Yeah, so verifying [76:39] applications that have been learned or [76:42] generated [76:44] or generated by AI also and it's still a [76:47] pretty [76:48] hot issue. [76:50] Back in 2018 I was more thinking of of [76:53] verifying simple neural networks like [76:56] those used for I don't know computer [76:58] vision [76:59] or self-driving cars or or or some [77:02] numerical computations like you know [77:05] weather prediction and so on. So so [77:07] specialized LLMs but you still want some [77:09] guarantees about [77:11] what they produce that they cannot [77:13] produce completely inconsistent outputs [77:15] for instance. There were some some [77:17] attempts in in in the last years at [77:20] using static analysis tools and [77:23] basically program verification tools [77:26] applied to LLMs [77:27] but well it it it doesn't scale. [77:32] LLMs are big. [77:34] Sorry. [77:35] Neural networks are big. [77:37] And for LLMs there's also [77:40] a distinct lack of specification. Okay. [77:44] You don't really know what's a good [77:46] answer from an LLM. [77:48] Well you know it when you see it but you [77:50] cannot write a mathematical [77:52] specification of it. So so that part is [77:54] probably over. What I would say are the [77:57] big problems for today yeah probably [78:00] maintaining software quality despite [78:02] AI's love despite a lot of pressure to [78:06] throw away traditional software [78:09] development techniques using [78:12] LLMs as an AI as much as we can to do [78:16] mechanized proofs so proofs that can be [78:18] checked by machines. [78:20] Maybe this will be the the decade of [78:22] formal verification of software. We've [78:24] been waiting for that for 50 years so [78:27] maybe it will it will finally take off. [78:31] >> What's your top book recommendation for [78:33] software engineers and why? [78:36] >> Well this this is an old one, the [78:38] Programming Pearls by Jon [78:40] I think I read it when I was a PhD [78:41] student, but I think it's it's nice as [78:45] showing how very talented programmers [78:48] work, [snorts] how they think about [78:51] their programs. So, it's it's it's it's [78:53] a combination of choosing the right [78:54] algorithms, [78:56] expressing them clearly, [78:59] uh knowing when to stop, [79:01] when when to use a simple algorithm, [79:04] where where [79:06] when a more complicated one is not [79:08] needed, [79:09] uh having a sense of elegance in in the [79:12] code you write, um [79:14] uh having a feeling for where the [79:16] problem is when when the the code [79:18] misbehave. So, all all that kind of [79:21] things that are hard to communicate, and [79:22] I think those those pearls [79:24] that are very easy to read, uh [79:27] and and and don't use any complicated [79:30] data structures, don't use any [79:31] complicated language. I mean, it it's [79:33] it's kind of timeless, you know. [79:35] Um [79:37] I think those pearls are are good [79:38] illustration of that. [79:41] Uh so, if you haven't read it, it's it's [79:43] a classic, but [79:45] I think it's a nice reading. [79:46] Nice read. Uh the second one is a little [79:49] more controversial, I guess. [79:51] So, in the How to Design Program, which [79:54] is a fairly ambitious title as well. [79:56] And this comes from the Scheme [79:58] community, okay, Abelson and Findler, [80:01] Flatt, and Krishnamurthi. [80:03] Um and and those people have developed [80:06] uh well, the Scheme community is famous [80:08] for having developed uh pedagogical [80:10] resources that are [80:11] I mean, ways to teach programming uh [80:16] that that go beyond teaching functional [80:18] programming, basically. [80:20] And so, so there was the [80:23] the MIT [clears throat] [80:24] Course Structure and Interpretation of [80:25] Computer Programs, which was quite [80:26] famous, and this is kind of a more [80:28] modern [80:30] twist on on on similar ideas. [80:33] And and and [80:35] I find this book interesting because [80:38] well, it it it really teaches you the [80:40] way of functional programming [80:43] a way to functional programming. It can [80:45] be very irritating sometimes, very [80:47] opinionated, very [80:49] um almost mystical sometimes, but [80:53] but it's also [80:55] another [80:56] great attempt at at trying to [80:58] communicate [81:00] how experienced programmers go about uh [81:03] designing a program [81:06] uh [81:07] even before writing the first line. [81:09] Okay. And and then how [81:11] given a language like Scheme, which is [81:13] pretty flexible, how the code kind of [81:16] follows uh naturally. [81:19] >> You know, knowing what you know now, if [81:21] you could go back to when you just [81:23] started your career and give yourself [81:25] some advice, what would you say? [81:27] >> Sometimes I got that uh maybe I [81:31] specialized a little too early in in in [81:34] um [81:35] in programming language research. [81:37] Uh maybe [81:39] well, there there are some topics that [81:40] are I didn't learn [81:44] because I didn't feel like it. And and [81:46] that I had to relearn later or I still [81:50] have to learn now that I'm almost 60 and [81:55] maybe not not as um [81:57] uh [81:59] not as quick uh [82:01] as I was back in the day. So, yeah, [82:03] maybe I I did specialize a little too [82:06] early. And so, I would encourage [82:07] everyone to get a everyone who's serious [82:10] about working in computing uh to get a [82:15] fairly diverse computer science [82:17] background. Even even for topics that [82:19] look super theoretical and are not very [82:22] uh relevant to [82:24] uh to everyday uh [82:27] jobs. [82:28] Uh well, we mentioned the [82:30] computability for instance things like [82:31] the halting problem and so on. You're [82:33] not going to run into that very often, [82:36] but it still [82:37] gives [82:38] interesting perspectives, I think. [82:42] And then it also helps understanding new [82:44] problems. [82:46] Like [82:48] with quantum computing. [82:50] What can you do with a quantum computer [82:52] that you cannot do with a normal [82:53] computer? [82:55] And and and it's it's time to to revisit [82:58] all of the classic complexity theory I [83:01] learned earlier and when when I was [83:04] young. And and so yeah, I think I think [83:07] it's good to have those this kind of [83:09] background even if [83:12] it's not obvious you will be using it [83:14] everyday. [83:15] And and sometimes I wish I had taken [83:18] time to accumulate a little more of this [83:20] background [83:22] before specializing in in programming [83:24] languages. [83:25] >> Awesome. Well, thank you so much for [83:26] your time Professor Liwei. I appreciate [83:28] it. [83:28] >> Thank you Aaron. That was nice. [83:31] >> Hey, thank you for watching this [83:32] podcast. If you liked it and you want to [83:34] see the show grow, please support with a [83:36] comment or a like. [83:38] Also, if you have any recommendations [83:40] for people you want me to bring on, [83:42] please drop a comment. Guests like [83:44] Barbara Liskov, Mike Stonebraker, Mark [83:46] Brooker, these were all people that I [83:48] brought on because someone left a [83:50] comment. On another note, aside from the [83:53] podcast, I'm working on building the [83:54] ergonomic keyboard that I wish existed. [83:57] Here's a glance at the prototype. It's a [83:59] split keyboard, so there's two sides. [84:02] Um this is in the case. But yeah, we [84:03] launched on Kickstarter and we hit our [84:05] goal within 8 hours of launching. I [84:07] really appreciate it if you were one of [84:09] the people who grabbed one of the early [84:10] units. Um we're now working on the long [84:13] journey of building the tooling now. And [84:15] so if you still want to pick one up, [84:16] I've left the late pledges open on [84:18] Kickstarter, so you can grab one there. [84:21] I'll put a link in the description. [84:23] Thank you again for watching the podcast [84:25] and I'll see you in the next episode.