Creator of OCaml: Functional Programming, Formal Verification, Programming Languages | Xavier Leroy

25:19Xavier Leroy:I hear about it a lot more now, which is Lean and these theorem provers. What are those in this context and how are they used? So, yeah, so Lean is an example, an instance of the so-called provers or proof assistants. So originally those were developed to do mathematics on the computer. So nothing with not formal verification of programs, but they can also be used for formal verification of programs. But the initial motivation was really to do mathematics with the help of the computer. where originally everyone focused on automatic theorem proving, so having the machine find proofs all by itself.

26:08But that's very, very difficult. And not necessarily what mathematicians need. And so those proof assistants are more like formal languages, like programming languages, but where you can write mathematical definitions, mathematical statements, and they will help you prove. So some small proof steps they will do automatically. And for others, the user still has to guide the prover through the major steps. But the good thing is that the proof is recorded also in a format that the machine can understand and recheck. So when you complete a proof in Lean or Rock or Isabelle or one of those tools, and it is rechecked, and the computer makes sure that all inferences are justified, that you didn't forget any case, that you didn't use a conclusion as a hypothesis, or all kind of problems you can have with a pencil and paper proof.

27:12And so in the end, you get proofs that are extremely reliable, extremely credible. and it's been, so those tools have been used a little bit for some big mathematical results where the proofs are so big that they can't be done just by humans. You really need computer assistance. I think there's a recent example with a weak Goldbach conjecture. So part of the proof involved checking a whole lot of inequality, maybe a thousand inequalities involving several real variables and blah, blah, blah. And so computer assistance was really needed to make sure that everything was checked and there was no human mistakes left.

28:07and maybe we'll talk about generative AI later, but there's also now a lot of interest in conjunction with generative AI. AI is pretty good at coming up with plausible proofs, but then they have to be checked by humans. Unless AI writes a proof in one of those formal languages, like Lean, in which case it can be checked by a machine, and that's much more effective.

28:38Xavier Leroy:So yeah, it's the idea of using the machine to help you write proofs and recheck proofs that you've written yourself or maybe with some help from an AI. And now those tools can also be used to prove properties about programs. And so I spent many years proving the correctness of a compiler using one of those tools, the Rok proof assistant. So basically, what I'm proving about the compiler, so it takes C code, it produces assembly code, and proving that the assembly code is phase four to the C code. So there's no miscompilation. The compiler didn't introduce a bug in the program that wasn't there originally.

29:28And it's a fairly big proof because compilers do complicated things about programs, and then you have to define exactly what it means to preserve the semantics of a program. So you have to define the semantics of your programming languages. And so it's all a very good use of those machine, of those proof assistants. The same work could be done on paper, but, I mean, this would be a proof of several thousand pages and nobody would want to read it. Nobody would trust it. It's just too big. and it would be very hard to evolve. One good thing about those mechanized verifications of programs is that it can also help you evolve the program.

30:13You can add new features and so on and adapt your proofs and be really sure that you haven't introduced a regression or things like that. So, yeah, so it's really programming taken to a higher level and today is quite expensive. It takes a lot more time to prove a program than to find it in the first place, but maybe this is getting a little better. Yeah, and I should also mention another great example of verified software. It's a microkernel, the SEL4 microkernel developed in Australia and which is used as a hypervisor in some applications. And so it's really like 8 ,000 lines of extremely technical C code that manipulates processes and capabilities and security tokens and so on.

31:14And it's been proved correct. Every line has been proved correct. And that's a very big achievement.

31:20Xavier Leroy:When you mentioned the example of verifying a mathematical proof, That makes sense to me. When you talk about proving something about a program, it's a little bit more abstract to me or having some trouble visualizing. Could you give a concrete example, like maybe some trivial program and we're trying to prove something about it and how that theorem prover would work? Let's say you have a function that takes three numbers, X, Y, Z, and returns the average of those numbers. OK.

31:58Only, yeah, and maybe you're using a not completely obvious formula, like t equals x plus y, and then t equals t plus z, and then t equals t divided by 3, and then return t. OK, so not exactly the formula for the average.

32:22Xavier Leroy:And you want to prove that the function is correct. So you want to prove that it returns x plus y plus z divided by 3. And maybe you will have to make it clear whether you're rounding up or rounding down. If you're using integers or floating-point numbers, you know, it's not an exact arithmetic. So yeah, you will have to say exactly what you mean by divided by 3. And then if you're in a language like C, you can have arithmetic overflows. When you compute X plus Y plus Z, you can overflow the range of representable integers, and in C, it's a bug. It's an undefined behavior. So typically, you will want to put a so-called precondition on your function, saying, okay, if you call me, call me with numbers that are between, I don't know, zero and one million, for instance, but no bigger than that.

33:20And then the prover will check that no overflow can occur in this case. Okay. And so basically you have the precondition that says, okay, these are safety guarantees that must hold of the parameters, otherwise anything can happen. And then there will be a little bit of kind of symbolic execution of the function body It says, okay, when you do t equals x plus y, then t plus equals z, then t slash equals 3, then in the end t is x plus y plus z divided by 3, provided no overflow occurred. And then you put that with a precondition that says there cannot be any overflow, and you get your final result.

34:05Okay, so basically you're stating a contract for your function, hypothesis and the arguments, guarantees and the results, and you want to prove, analyze the function body to show that this contract is respected. I hope it's a little more concrete.

34:25Xavier Leroy:So it sounds like Lean will help you basically take in some invariance about a program and kind of propagate them through line by line and uphold them. And so you can say something about... Yes. Maybe not Lean by itself. A program prover will do exactly what you say. And for Lean to be able to do it, you still need to teach it a little bit about the semantics of your programming language. What does plus mean? What does assignment mean? Lean is mathematics. You don't assign in mathematics. You don't say x equals x plus 1. Or you're just comparing x and x plus y and it's always false. There are no assignments in mathematics.

35:13There are assignments in many programs. So you need to make it explicit that there are three different states for the t variable, three different values, and relate those values to – well, the program defines what those values are. And then a prover like Lean can reason about those three successive values because now you're in mathematics. And that kind of bridge between programs and their mathematical meaning is called semantics, that the field of semantics of programming languages has been a big topic in peer research since the 60s, at least.

35:56Xavier Leroy:Am I understanding then that like a pure functional programming language, that gap between mathematics and the actual symbols is much smaller than an imperative? Absolutely. Yeah, you're absolutely right. And that's one of the reasons why people who do formal methods don't like assignment, don't like imperative features. Purely functional style is much closer to mathematical style, so much easier to reason about. There can still be a few discrepancies between the program and the math. For instance, functional programs may not terminate. They may loop forever. Mathematics doesn't like that. So you need a way to reasonable termination.

36:44And also, yeah, sometimes, for instance, the arithmetic you get in the programming language is not integer arithmetic or it's not real, you know, it's floating point, it's not real, so you still have to account for that gap. But you're absolutely right that the gap is much shorter for functional programming. And in the experience of ComServe, my verified compiler, I think the first decision was to write it in a purely functional style so that it would be easier to reason about it later.

37:21Xavier Leroy:You mentioned the specifications that we could prove, and one of them was proving that the program terminates. But I thought that's a famously difficult or impossible, I forgot exactly, the halting problem, right? So how is that something that you could prove? Okay, so what the computability theory says is that there is no algorithm that can always say this program terminates or this program doesn't terminate. So there will always be some very weird programs for which your analyzer, your automatic termination analyzer will produce a wrong result or will not terminate itself. So it will not work.

38:10But still, for many programs, you can succeed. You can write automatic termination analyzers that will work for a large class of programs. And then the termination analysis, termination proof, can also be done by hand, by a mathematician. OK, so perhaps a human can see through those weird Turing programs that are hard to prove to terminate and recognize the trick. But anyway, so yeah, it's a hard problem and all program verification tasks are difficult problems. They are pretty much all undecidable. So you know that there is no static analyzer that will always find all problems in all programs.

39:03But still, you can try. You can try for specific problems, for specific programs, and get some very useful results out of that. You only need to be able to do it for the cases that are of interest to you, the programs you really care about.

39:20Xavier Leroy:OpenAI, Anthropic, Cursor, and Vercel all use this product to make their lives better. And the problem it solves is when you're building SaaS or an AI product and you want to sell to other companies, there's all these requirements you need to meet. There's SSO, there's SCIM, there's RBAC, there's audit logs. These are all things that take time to integrate, but aren't the main focus of your app. WorkOS is an API layer that lets you meet all of these requirements in just a few lines of code. So let's say you have a new SaaS product and you want to sell to other companies, WorkOS will solve all of these critical feature gaps for you.

39:57Xavier Leroy:You can check them out at workos.com to learn more and get started. And I appreciate them for supporting my work and sponsoring this podcast. One thing I saw when I was researching OCaml is that in 2022, OCaml added multi-core support. But from my memory, I remember multi-core processors became standard much earlier than that. And so I figured there might be some unique engineering challenge in adding that support. So yeah, what happened there and what made it difficult? Well, there were engineering challenges, that's for sure. There were also some language design issues. But let's talk about the engineering challenges first.

40:40So it's true that when you have a language with a runtime system, a memory allocator, garbage collector, well at least the one for Camel was really designed with sequential executions in mind. So if you have, if you had the shared memory concurrency, then you need a garbage collector and a memory allocator that can work concurrently, and that's actually quite difficult, at least if you want them to be fast. Of course, you could always take a look at every operation in the heap, but then you would sequentialize your programs. Basically, they would run as slowly as a single processor, so that's not interesting.

41:24So, yeah, so there were engineering challenges. And, yeah, I was at least initially quite reluctant to basically implement a complete garbage collector and memory allocator on large parts of the runtime system. That's what we did eventually. Well, it was done mostly by the team at OCaml Labs at Cambridge University. But, yes, it was a really big rewrite. But then I said there's also a language design issue, which is that for the longest time, well, now when you say multi-core processors and so on, pretty much everyone, and language support for multi-core processors, everyone thinks about language support for shared memory concurrency.

42:19You know, this model where you have several threads of control and they access the same memory, and basically the threads communicate by modifying the memory, and someone else is going to know this. I've never liked this model of communication. I mean, it's a bit like if you want to communicate with your neighbor, then you bike into their house, and then you move the furniture around, and then when they are back, they say, oh, something was moved. So it's probably Ryan who's trying to tell us something. Maybe you could just meet your neighbors, you know. And that would be things like message passing, which is a completely different form of communication, much higher level.

43:05So, yeah, so for the longest time, I was really interested in message passing concurrency. And there's, for instance, a functional language called Erlang that was built on those ideas that I found quite interesting. However, I never got to have a decent language design, and everyone was saying, no, but it's too costly. It's not effective. There's too much copying of data. With shared memory, you can share some kind of huge database in memory. If you don't modify it too much, then basically the sharing, the concurrency is free. While with message passing, we'll have to exchange a lot of data to get the same effect, so you will pay more for it.

43:53Anyway, so, okay, so starting with Java, I guess, and then C, C++ 2011, there was this idea that, okay, we need to expose shared memory concurrency to the programmers. But then comes the problem of the memory model, which is that what happens when there's a race, for instance, when two sides want to access the same location and maybe they want to modify it in different ways. And so sometimes part of the CC++ standard says it's undefined behavior. Anything can happen. But still you need to give a little more guarantees. At the other end of the spectrum, there's so-called sequential consistency which says, well, what happens is like an interleaving of reads and writes of your program.

44:43You don't know which interleaving, but there is an interleaving. But that doesn't work with modern processors, multicore processors. They reorder memory accesses in very clever ways to get more performance. And so viewed from the program, it's very hard to predict what they are actually doing. And so you need to give your programmers, when you're designing a language with shared memory concurrency, you need to give your programmer some guarantees about the ordering of reads and writes, concurrent reads and writes, while not constraining the hardware too much. And it's very difficult. So Java went through like five different iterations of the memory model.

45:23Some were too strict, some were too lax, some were inconsistent. We're making predictions, impossible predictions, where the past depends on the future. Crazy, really crazy stuff. Then C++11 did a little better, but still extremely complex memory model. And so when we wanted to add, especially the OCaml Labs people wanted to add shared memory concurrency to OCaml, we had to also agree on a memory model that would be exposed to the programmers. And that also took quite a bit of a design, quite a bit of time to come up with a good design. And I think it's better and easier to understand and use than the one of Java, but the OCaml memory model is still quite complicated.

46:14And sometimes I feel sorry our users are exposed to that. So that explains why it took so long. Solving the engineering challenges, but also agreeing on a memory model and what kind of guarantees we're going to give to programmers.

46:36Xavier Leroy:Oh, yeah, I forgot to say one thing, which is that in C and C++, there's a lot of things you can say, oh, it's just undefined behavior, anything can happen. In type-safe languages like Java and OKML, you want to give stronger guarantees. Maybe many things can happen, but your data should remain well-typed. Typically, you don't want to expose an object to another thread before it's been fully initialized, for instance. And that's actually very hard to guarantee in your memory model. And then you have to implement that memory model, so your compiler also needs to take extra precautions to guarantee this.

47:19So yeah, type safety in the presence of shared memory concurrency is not obvious at all. So that's why it took so long.

47:30Xavier Leroy:So in Python, I know there's the famous GIL, the global interpreter lock. What is that lock protecting? Is it the cleanup of objects on the heap or is it something else? Among other things, yes. So yeah, we had the same thing in OCaml before, before multi-core OCaml was merged in. So, yeah, well, basically the idea that when your runtime system is not thread-safe, as we said, you can protect the non-thread-safe functions by your lock so that they will never be executed concurrently. But if you take the lock at every allocation and release it, you take and release the lock for every allocation, that is just too slow anyway.

48:12And so the idea is that you take the lock when you enter Python code, let's say, and you start executing Python code, but you can still release it when you do input-output, for instance, when you're going to block for a long time, or when you're calling into C code that is thread-safe and is not going to use your runtime system. Then you can release the lock, and some other Python thread can take it and execute. So you get a little bit of concurrency. You can overlap computations in your high-level language with I.O. or computation is a low-level language in another language. But you still have mutual exclusion between two threads running Python or running OKML before multicore OKML.

49:03Xavier Leroy:So you get some benefits like concurrent I.O., but you don't get any parallelism. You don't get a speed-up for computations. And so, yeah, so we used to have this guild in OCaml as well. And so you can get rid of it, but in general, you need to redesign at least a garbage collector and memory allocator. There's probably a few places in the OCaml runtime system that still use locks to ensure mutual exclusion, like in the IO subsystem. And some phases of the garbage collector, I think, are the phase which has kind of stopped the world where you need to make sure that everyone, no camel code is running.

49:55For a short time, you need to make sure that everyone is stopped and then do a little bit of work to finish the GC and then you can restart everyone.

50:05Xavier Leroy:So yeah, these are tricky things. And I don't know what the Python people are up to with their gil, if they finally managed to remove it or they're still working on it. But I've heard they're making progress. You mentioned Python calling into C, and I've seen that pattern before of a higher level language interfacing with a lower level one. How does that binding typically work? Oh, it's another can of worms.

50:38Well, there are two aspects. There are the control flow and there are the data.

50:43Xavier Leroy:So the control part is not that hard. So yes, you need a mechanism so that your Python interpreter or your OCaml compiled code will actually jump to the C function. So for OCaml, basically, you tell the OCaml compiler that this function is not implemented in OCaml. It's actually implemented by the C function, and you give its name. And then the compiler will emit a call to the C function using the C calling conventions, which are not exactly the same as the OKML calling conventions, but the compiler knows about that. And so it will call the C function, maybe through a little bit of glue code, whatever.

51:21And then the C function will execute and return back to the OKML code.

51:30That's relatively easy. Now, the hard part is data. like function arguments and function results, because OCaml and C have different data representations. For instance, a floating point number in OCaml is generally boxed, so it's allocated in the heap and handled through a pointer. So it's more like a double star in C, and it's not a double which is not allocated, just sits in a register.

52:03So typically, the C code needs to use a so-called firing function interface, so some C function and macros provided by OCaml to access the OCaml data, the OCaml arguments, extract the part that it needs, the numbers. Another example is arrays. In OCaml, when you have a two-dimensional array, it's actually an array of arrays. So view from C is an array of pointers to arrays, while in C, an array of arrays is, there's no intermediate pointer. So it's not the same representation. And so you have to explain to C or give C some functions and macros to access elements in OCaml arrays. It's not exactly the same code that you would do to access a C array from C.

52:52Xavier Leroy:Okay, so you need access source. but now if your C code wants to return some complex results, like a list, an array, and so on, it needs to allocate it in the OKML heap. So it needs to ask the runtime system to do some heap allocation and then fill the heap blocks correctly. And then this allocation can trigger a garbage collection. So the C code must also kind of cooperate with garbage collection, with both registration mechanisms, et cetera, et cetera. So there's quite a bit of work to be done. And then different fine function interfaces arrange this work differently. So there's a base FFI for OCaml.

53:38Basically, it's a C code that must do all the work. But then it can be very fast and quite optimized. But there are other FFIs, like the C types FFI in OCaml, where most of this data conversion and mediating between two data formats is automated. You start basically with a description of the C type of the C function, and you can automate some of those conversions. But sometimes it can be expensive. For instance, you may end up copying a whole array while your C code only needs to access two or three elements in it.

54:16Xavier Leroy:Okay, so there's lots of trade-offs. And quite frankly, it's a dirty part of programming language implementation. The Okaml FFI is not that clean, but if you look at the Java FFI, for instance, it's also quite complicated. And for Python, I've never tried, so I don't know what it looks like. But yeah, it's a necessity, but it can be quite hard because the data models are different between the two languages. So to kind of get the big picture, on the OCaml side, there's an interpreter, which is a program running an application space that is interpreting your OCaml code. And then at some point in the OCaml code, it says, do some, you know, load this C program.

55:09Xavier Leroy:And the C program is a binary somewhere. and the OCaml interpreter then starts to load those instructions and execute them. Okay. So actually, this is the third aspect that I didn't touch. So OCaml, well, there's an interpreter mode, but in general, we compile. We compile to assembly code and then machine code. And so in compiled mode, what you say is how you put together the OCaml code and the C code is done by the linker, the C linker. So basically someone else is doing that for us. And it's not that different from linking together two object files produced by C or two object files produced by OCaml.

55:59Okay. But you're right that for more interpreted languages, there's also the question of how you load the C code. In general, you use a dynamic loading interface, DL open, for instance, in Unix.

56:18And then there's a little bit of introspection. So at runtime, the interpreter always queries, the C libraries, and what is the address of a function named foo? and then it will find the address and use that to manufacture a call. So yeah, if you're in an interpreted setting or bytecode compiled setting like Python, there's this additional level of complexity on top of it.

56:43Xavier Leroy:I see, I see. Okay, so if I had a mixed OCaml C program to my computer, it's just one binary or one blob. In the simplest case, yes. There are also dynamic loading facilities in OKML, but I don't want to get into that because I'm a firm believer in static linking. I think programs should be statically linked so that there's no surprise when you run them. Like, oh, where is this DLL or DLL not found, for instance, problems. But of course, you lose a little bit in flexibility. But yeah, I think static linking is actually quite useful in that it guarantees a lot of things. It checks a lot of things at link time that you don't have to check again at runtime.

57:41Xavier Leroy:We mentioned earlier in the conversation talking a little bit about LLM-generated code. I thought that might be interesting to cover. And in one interview, you talked about the danger of almost correct code. So plausible code, but it's wrong that an LM can produce. And what are your thoughts on how to address that kind of problem? It's a tough problem. I mean, globally, I'm a little bit skeptical about GeneralEv. Of course, they can do amazing things that were unthinkable like a few years ago. But there's also, there's always some errors. OK, you can't really trust what's being produced by generative AI.

58:33And so, in principle, humans should be there to check the output and fix errors or ask the LLM to fix its own errors until the result is actually usable. usable, but of course it's very hard because there's a slop problem. AI is produced so much, it's so easy to produce large number large quantities of text, of code, pictures, whatever, that in the end, there's no human time to check it all. So, yeah, recently I heard when someone working in an AI startup who was enthusiastic about AI-generated code, saying that thanks to generative AI, the cost of programming is dropping to zero. But, well, the cost of writing code, maybe, but what about, you know, checking it, making sure it is correct, that it does what we want, that, well, that cost is not zero at all.

59:50And for me, every new line of code is a liability. You have to test it. You have to check it. Maybe you have to do formal verification. You have to evolve it, maintain it later. So, no, I don't want huge amounts of code. I want 50 lines of code that have been thought, that have been polished over the years. So, anyway, I'm not getting that with AI. And I think that's a problem. And this idea that humans will be there to check the output of general AI is just, oh, no, they are not available for that. There's too much of it, and it's not present either. I mean, I don't think it's a good way to split the work between machines and humans.

1:00:44So anyway, maybe there will be some societal solution, like a big no-to-AI-slop movement. So we're trying to see that in some open-source projects that refuse and generate contributions because there's just too many. I know that for OCaml and especially for ComCert, I've received some issues, a report of issues that were obviously generated by AI. And there was maybe one good issue among 10 reports. And each report was several pages long with very detailed explanations and a repro case that in the end doesn't repro anything or reproduces something else. But it takes time to go through all those things, and maybe at some point I will say no to AI-generated contributions.

1:01:40Okay, but maybe there's also a bit of a technical solution, which is, as we said earlier, to have AI produce proofs. So evidence that its creation is correct. So as I said, this is starting to work for mathematical proofs. Some general AI's are able to produce proofs both in English and in the formal language of the Lean Prover, for instance. And so you can get Lean to recheck the proof and get some confidence. You still need to be very careful about the statement because sometimes AI's will change the statement or the definitions to make the proof easier. that happens and also you should be careful about so-called self-formalizations where the AI also comes up with some definitions and some statements by parsing a PDF file or whatever

1:02:44Xavier Leroy:and sometimes it introduces errors at that point so anyway there is still a need for human review but on smaller quantities of text and mathematical text. And maybe one day it will also work for program proof. So when an AI generates a program, it might be able to generate some lean proof or whatever that the program satisfies some specification.

1:03:14So I think it is possible. But now the question will be, where does the specification come from? It's always been a big issue for formal methods. It's not just that verification is hard, but agreeing on the spec can be difficult too. And well, mathematicians have a lot of experience, you know, in stating, finding definitions that they find interesting and stating theorems that they believe should be true or that that will mean something. Computer programmers are less good with that, and it's fairly easy to come up with specifications that are inconsistent or impossible. So remember this average function, there was a precondition of the three numbers, the argument saying they must not be too big.

1:04:10But say, maybe you can end up with a precondition that just cannot be satisfied. and at this point the body of the function will always be verified, even if it's completely wrong because the assumption says basically this function cannot be called and so you get a false sense of confidence you've verified something but it's actually unusable and that's a fairly delicate point where I'm not sure LLMs or AI is going to help much, but it's a problem with formal methods in general. And some possibilities include the ability to test specifications, for instance. So instead of using your test suite to see if your code works out, you can also use it to see if your spec checks out.

1:05:17Those kind of things. But yeah, we're kind of moving some of the difficulties from the programming phase to the specification phase. But we still have some problems. Anyway, so that might be a way to deal with the AI-generated code and develop some confidence in it.

1:05:39Xavier Leroy:LLM-generated code is becoming extremely popular. And I think there's a lot of potential downstream consequences on this, on the programming language landscape. And I thought it might be interesting to hear your thoughts on speculating. Imagine 10 years from now, if you took LLM generated code and turned it up, how might you think that the programming language landscape might change? Yeah, a couple of years ago, someone asked me about that, and there was a concern that the training data would be, there wouldn't be enough training data in OCaml for an LLM to really learn how to program in OCaml.

1:06:25And it's true that there's less OCaml code in the world than the JavaScript code, for instance. but apparently

1:06:35Xavier Leroy:contemporary LLMs do well with the amount of OCaml code they have maybe because there's enough maybe because learning has become a little more efficient, maybe because there's less OCaml code than JavaScript code but maybe the OCaml code is better quality I don't know So anyway, maybe LLMs are getting better also to transfer knowledge that they've learned from one language to another. That could be. I have no idea how those things work. But yeah, so the latest feedback I've got about LLMs and generative AI and OCaml is that the OCaml code generated is quite decent and quite similar in quality to more popular languages.

1:07:29And one thing that seems to help the generative AI is a type system. So the fact that there's some static checking just of the type, it's already effective in, you know, avoiding some errors and maybe encouraging the LLM to, like, declare types first. So give some type structure to the program. All right. And now, 10 years from now, it's difficult to guess. So will it be the more popular languages of today that will be even more popular because of generated AI? Will it be the safer languages of today that will be more popular with AI because there are fewer errors in the end? I'm hoping it will be the safer languages, but I really don't know.

1:08:31Xavier Leroy:I've seen in the industry, there's a few cases where because it's so easy to generate code, massive rewrites are something that would have been very infeasible in the past, are very realizable now. So if there's an existing project where they chose a programming language for whatever reason in the past, they could translate the entire thing into another language with reasonable confidence. Given that kind of environment, which programming languages would you expect more people would switch to? Because they want to switch to it, but they weren't able to in the past, but now it's cheaper, so they can.

1:09:13Well, so today, I've heard mostly about C and C++ to Rust translations, hoping that the generated host code will be safer. As I said, I've seen at least one project when the generated host code is entirely in unsafe blocks. So it's really kind of line by line translation of the C code. But maybe it can still be used at a starting point for making it safer later. So yeah, I would say today I can imagine I've seen significant efforts being done with Rust as a target language.

1:09:55Xavier Leroy:In the functional world, I'm not quite sure. Well, maybe a functional language to one of those proof assistants, like Lean or Rock, because they also have functional programming languages in them, much more restricted, but much more amenable to proofs. So maybe for a few projects that could be interesting, again, as a first step towards a formal proof, as we said earlier. When you compare industry versus academia today, where would you say most of the innovation and programming languages comes from? And also, has that changed over time? Okay. Well, I think most of the innovations have come from industry.

1:10:48lately. And that wasn't the case in the early days of computer science. If you think of, I mean, the truly innovative languages like Algol, Lisp,

1:11:06Xavier Leroy:Prolog, Smalltalk were developed in mostly academic settings. Well, Smalltalk was Xerox PARC, which was an industrial research lab, but very far far away from industrial customers. And then there were, you know, much more practical languages, uglier languages developed typically at IBM, like Fortran, Cobalt, PL1, etc. And then, so really the idea that the nice ideas come from academia and nature there. And then, well, the nice ideas from academia started to be transferred by industry much more quickly. I'm thinking of, well, C and especially C++ and then Java, which really took ideas like object orientation and garbage collection, automatic memory management in industry.

1:12:07before Java, it was just crazy academics in the ivory tower that were using garbage collected languages. It was completely impossible to have that in enterprise computing. And Java came, and two years later, everyone was doing garbage collection and being very happy about it. And Java also popularized type safety, bytecode verification, Well, some pretty advanced techniques of the 90s. And if you look at further developments, I don't know, Swift, for instance, popularized the idea of algebraic data types and pattern matching, and then Rust. Well, Rust is even more spectacular, I would say, because algebraic data types, garbage collections, etc., those were already present in academic languages, like, well, CAMEL, for instance.

1:13:01But Rust really took very recent research results of the 2000s on safe low-level programming that were basically never implemented in any language and managed to do a consistent whole from that. And so I'm really admirative. And I have the impression that, well, I would have loved if Rust came out of academia, but I'm not sure it would have been possible because it's also a huge effort and you really need the backing of a big company. But still, I'm not sad because I think it's also a very good sign that industry is interested in new programming languages. You know, at some point in the 90s, well, pretty much when I was hired at Inria on a research position, when I was hired as someone who had developed first versions of OCaml, well, predecessor of OCaml and who was working on type systems or programming languages and so on.

1:14:08But then some people told me, but there's no future in programming language research. Industry has decided it would be C++ forever. so deal with it. Maybe you could do software engineering and not PL research. And then Java came a few years later and showing that no, industry hasn't decided on a particular programming language. Industry is still interested in new programming languages. Industry still thinks that a new programming language can be part of the solution to software problems. and I find it extremely encouraging. We are not stuck with bad languages from the past. Well, there's a lot of legacy code, of course, but there's still real interest for better languages and I think this will continue and I think it's good for the computing field.

1:15:06Xavier Leroy:In 2018, there was an interview that you did and they asked you what are the most interesting and important problems to focus on in the coming years. And you called out the difficulty of programming, you know, GPUs because they were using dialects of C, shoddy tools, and also the challenges in verifying machine learned code, basically. And that sounds pretty relevant today, but what would you say your answer is today? So, yeah, I think for the question of how we program massively parallel hardware, I think we've made a little bit of progress recently with things like the MLIR initiative on LLVM or some domain-specific languages like Allied, which are pretty good.

1:15:57You know, those domain-specific languages for tensor computations are getting a little better. but still I find it a little bit frustrating that I cannot do I don't know, say I'm proving on a GPU I have absolutely no idea how to go about that and in part by lack of an appropriate language so

1:16:21Xavier Leroy:I'm not ready to program the GPU pipelines at a very low level myself and I think it's more general, I think We are not using all these GPU and highly parallel hardware as much as we could. Yeah, so verifying applications that have been learned or generated by AI or so on is still a pretty hot issue. Back in 2018, I was more thinking of verifying simple neural networks like those used for computer vision, self-driving cars, or some numerical computations like weather prediction and so on. So specialized LLMs, but you still want some guarantees about what they produce, that they cannot produce completely inconsistent outputs, for instance.

1:17:16There were some attempts in the last years at using static analysis tools and basically program verification tools applied to LLMs, but, well, it doesn't scale. LLMs are big. Sorry. Neural networks are big. And for LLMs, there are also a distinct lack of specification.

1:17:42Xavier Leroy:Okay. you don't really know what's a good answer from an LLM. Well, you know it when you see it, but you cannot write a mathematical specification of it. So that part is probably over. What I would say are the big problems for today, probably maintaining software quality despite AI slope, despite a lot of pressure to throw away traditional software development techniques. using LLMs as an AI as much as we can to do mechanized proofs. So proofs that can be checked by machines. Maybe this will be the decade of formal verification of software. We've been waiting for that for 50 years. Maybe it will finally take off.

1:18:30Xavier Leroy:What's your top book recommendation for software engineers and why? This is an old one. They're programming Perth by Bentley. I think I read it when I was a PhD student. But I think it's nice as showing how very talented programmers work, how they think about their programs. It's a combination of choosing the right algorithms, expressing them clearly, knowing when to stop, when to use a simple algorithm where a more complicated one is not needed, having a sense of elegance in the code you write, having a feeling for where the problem is when the code misbehave. So all those kind of things that are hard to communicate, and I think those pearls that are very easy to read and don't use any complicated data structures, don't use any complicated language.

1:19:32I mean, it's kind of timeless, you know. I think those pearls are a good illustration of that. So if you haven't read it, it's a classic, but I think it's a nice reading. Nice read. The second one is a little more controversial, I guess. So in the How to Design Program, which is a fairly ambitious title as well. And this comes from the scheme community. Okay, Finneisen, Findler, Flat, and Krishnamurthy. And those people have developed, well, the skin community is famous for having developed pedagogical resources that are, I mean, ways to teach programming that go beyond teaching functional programming, basically.

1:20:20And so there was the MIT course, Structural Interpretation of Computer Programs, which was quite famous. and this is kind of a more modern twist on similar ideas. And I find this book interesting because, well, it really teaches you the way of functional programming, or a way to functional programming. It can be very irritating sometimes, very opinionated, very almost mystical sometimes, But it's also another great attempt at trying to communicate how experienced programmers go about designing a program even before writing the first line. And then how, given a language like Scheme, which is pretty flexible, how the code kind of follows naturally.

1:21:19Xavier Leroy:you know knowing what you know now if you could go back to when you just started your career and give yourself some advice what would you say sometimes i got that uh maybe i specialized a little too early in in in um in programming language research or maybe well there are some topics that i didn't learn because i didn't feel like it and that I had to relearn later or I still have to learn now that I'm almost 60 and maybe not as quick as I was back in the day. So yeah, maybe I did specialize a little too early and so I would encourage everyone who's serious about working in computing to get fairly diverse computer science background, even for topics that look super theoretical and not very relevant to everyday jobs.

1:22:28Well, we mentioned computability, for instance, things like the halting problem and so on. You're not going to run into that very often, but it still gives interesting perspectives. I think. And then it also helps understanding new problems, like with quantum computing. What can you do with a quantum computer that you cannot do with a normal computer? And it's time to revisit all of the classic complexity theory I learned earlier when I was young. And so, yeah, I think it's good to have this kind of background even if it's not obvious you will be using it every day. And sometimes I wish I had taken time to accumulate a little more of this background before specializing in programming languages.

1:23:25Xavier Leroy:Awesome. Well, thank you so much for your time, Professor Liwar. I appreciate it. Thank you, Arian. That was nice. Hey, thank you for watching this podcast. If you liked it and you want to see the show grow, please support with a comment or a like. Also, if you have any recommendations for people you want me to bring on, please drop a comment. Guests like Barbara Liskov, Mike Stonebreaker, Mark Brooker. These were all people that I brought on because someone left a comment. On another note, aside from the podcast, I'm working on building the ergonomic keyboard that I wish existed. Here's a glance at the prototype.

1:23:58Xavier Leroy:It's a split keyboard. So there's two sides. This is in the case. But yeah, we launched on Kickstarter and we hit our goal within eight hours of launching. I really appreciate it if you were one of the people who grabbed one of the early units. We're now working on the long journey of building the tooling now. And so if you still want to pick one up, I've left the late pledges open on Kickstarter. So you can grab one there. I'll put a link in the description. Thank you again for watching the podcast and I'll see you in the next episode.