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

Xavier Leroy (creator of OCaml) is an expert in compilers, formal verification of software and functional programming. This interview should be an approachable resource if you're curious about formal verification of software since I was learning that on the fly during it. • My ergonomic keyboard project I mentioned, you can follow along here: https://read.compose.llc/ • The Kickstarter page for it: https://www.kickstarter.com/projects/ryanlpeterman/compose-simple-ergonomics-beautifully-done Podcast links: • YouTube: https://youtu.be/9Cswiqrq6So • Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835 • Transcript: https://www.developing.dev/p/creator-of-ocaml-functional-programming Thank you to this episode's sponsor for supporting my work: • WorkOS: makes your app Enterprise Ready with easy to use APIs to add SSO, SCIM, RBAC, and more in just a few lines of code, check them out at https://workos.com/ Timestamps: (00:00) Intro (00:43) What sets OCaml apart (04:39) OCaml vs Rust (07:57) Why is manual memory management more performant (11:21) Javascript vs OCaml (14:00) Famous Rob Pike quote (16:05) Type inference and how it works (22:12) What is formal verification and how does it work (40:07) What made multicore support difficult for OCaml (50:17) How programming languages interface and call each other (57:41) The danger of almost-correct LLM code (01:05:39) How LLMs will change programming languages (01:10:26) Industry vs academia (01:15:05) Most interesting unsolved problems (01:18:30) Top book recommendations for engineers (01:21:17) Advice for his younger self (01:23:31) Outro Where to find Xavier: • Wikipedia: https://en.wikipedia.org/wiki/Xavier_Leroy • Website: https://xavierleroy.org/ Where to find Ryan: • Newsletter: https://www.developing.dev/ • X/Twitter: https://x.com/ryanlpeterman • LinkedIn: https://www.linkedin.com/in/ryanlpeterman/ • Threads: https://www.threads.com/@ryanlpeterman • Instagram: https://www.instagram.com/ryanlpeterman • TikTok: https://www.tiktok.com/@ryanlpeterman Referenced in this episode: • CompCert verified C compiler: https://compcert.org/ • seL4 microkernel: https://sel4.systems/ • Programming Pearls (book, not an affiliate link): https://www.amazon.com/dp/0201657880 • How to Design Programs (book): https://htdp.org/

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:00Speaker 00

  Testing can only show the presence of bugs, but not their complete absence.

• 0:04Ryan Peterman?

  This is the creator of the OCaml programming language, and I asked him all about programming language design and formal verification.

• 0:11Speaker 00

  Oh, my God. I'm not a big fan of JavaScript. And Rust is the finest language for manual memory management. Manual memory management is not always faster. Maybe this will be the decade of formal verification of software.

• 0:27Ryan Peterman?

  If you took LM-generated code and turned it up, what languages would become more popular? What languages might fade away?

• 0:35Speaker 00

  Oof.

• 0:37Ryan Peterman?

  Here's the full episode.

• 0:43Ryan Peterman?

  What sets OCaml apart from other programming languages?

• 0:47Speaker 00

  It is a fine functional language. Okay, you can write functions by case over inductive types and recursion and combine them with combinator and higher order functions and everything. So it's really a fine functional language, but it's also a fairly decent systems programming language. And so it has full imperative power. It has lots of interesting control structures, exceptions, threads, handlers for user-defined effects, which we added recently. And it has a very predictable cost model, execution model. So when you write your code,

• 1:32Speaker 00

  you have a pretty good idea what will take time and what will be fast and what will be slow. And that's not the case for all functional languages. Some are pretty unpredictable. And then the implementation is also pretty performant. Okay, so there's a fairly decent compiler, not the best in its class, but the code is pretty efficient. There's a very good allocator on garbage collector with low latency, so you don't have much poses. You don't have long poses, and that's quite important when you do things like network programming. And so you can write systems applications in a mostly functional style and with all the benefits of functional programming.

• 2:16Speaker 00

  And so initially, Okamel wasn't designed for those kind of applications. Okay, it was more for things like theorem proving or implementing domain-specific languages. And then we got some of our first users who were from the systems community, in particular, the Ensembl project in the late 90s at Cornell University. So it was a network stack for, a network protocol stack for reliable multicast and those kind of, you know, collaborative distributed applications, like collaborative editing or multiplayer video games.

• 2:57Speaker 00

  And their first code was in C, of course, they were systems people, right? And it worked, but it was unmaintainable and they couldn't extend it anymore. And someone had the idea to try Okamel. And so first, the code became a lot nicer and easier to evolve. And the performance was a lot less good as a C code. And in particular, they had this brilliant trick of running the garbage collector while packets are in flight. Okay, well, once you've sent a packet, you're idle for a few microseconds. And so you can run some GC. It costs nothing. And so they were very happy with that.

• 3:40Speaker 00

  And then there were some other projects like this using Okamel for systems applications, like the Mirage, Uni-Turinals. And yeah, and another benefit or consequence of this Ensembl project is that one of the PhD students working on that was Jan Minsky, who then went to Jane Street and implemented their trading infrastructure in Okamel. So that is still today one of our big users. And again, it's, well, they do automatic trading, so it must be fast and reliable and no long pauses. But they also want the elegance of functional programming.

• 4:24Speaker 00

  They want non-programmers to be able to read and their code like financial engineers or quantitative analysts. And so, yeah, so Okamel is a fairly good match for those kind of applications.

• 4:39Ryan Peterman?

  I thought it might be interesting to ground some of the conversation here by making comparisons across programming languages, maybe ones that people know more. When you think about Rust versus OCaml, what are the big differences and the pros and cons of the various design decisions in those languages?

• 4:59Speaker 00

  The big dividing line is between Rust and OCaml is, well OCaml has automatic memory management, garbage collection, and Rust is definitely a language for manual memory management. It's the finest language that I know for manual memory management. It manages to make it mostly safe with the discipline of borrowing, etc., and tracking ownership and so on. So it's infinitely safer than C or C++, but it's still a language where you allocate and free memory yourself.

• 5:42Speaker 00

  And on the one hand, it gives more control over what the program is doing. On the other hand, it's still a big responsibility. It's significantly harder to write programs when you have to manage your memory, even with the help of Rust's types. So yeah, so for me, that's kind of the main dividing line. Otherwise Rust has, well Rust has many of the high-level features of functional languages, in particular in data structures and the ability to do pattern matching and so on. So it's a very interesting design because it really managed to,

• 6:26Speaker 00

  some kind of fusion between, you know, C or C++ style low-level programming and some of the high-level facilities of functional programming. But still, that divide, garbage collection versus manual memory management, remains.

• 6:43Ryan Peterman?

  So it sounds like this is a performance trade-off, where you give more to the programmer in exchange for higher performance.

• 6:53Speaker 00

  That's mostly true. They said manual memory management is not always faster. Or you need to be a very good programmer so that it's always faster. There's been some, mostly C++ code, for instance, that does a lot of copying of objects. Just because you're not quite sure you're the only owner. So you make a copy and now you're the only owner. But the copying is quite costly in time and in memory bloat. And for those kind of applications, garbage collected language is better. And likewise, with a GC,

• 7:36Speaker 00

  you can work with shared, sharing in data structures. Okay, and it's perfectly safe.

• 7:43Speaker 00

  While sharing is kind of limited with Rust's ownership discipline. There are more constraints. And so you may end up unsharing and so using more memory.

• 7:57Ryan Peterman?

  It is surprising to me that manual memory management would, in many cases, be more performant than automatic. Because, for instance, in other patterns in computer science, like let's say, letting the compiler optimize things for you instead of optimizing things yourself. I would have thought that letting some system manage memory for you rather than manually managing it would also be better. So why is there a difference there?

• 8:27Speaker 00

  Well, because garbage collection takes place at runtime. So indeed, from time to time, the program is no longer computing, executing what you wrote. It is actually scanning memory, trying to find memory that is no longer used. So there is a runtime overhead. And it can be, depending on applications, 10%, 20%, maybe sometimes 30%. But again, that doesn't mean the whole program is 30% slower than if you had written it with manual memory management. Because there may have been other costs, as you said,

• 9:11Speaker 00

  of manual memory management. But yes, there's...

• 9:17Speaker 00

  Well, there's been a lot of research on trying to do more, let's say, compile time, automatic memory management. And you can do that to some extent, but it's for some programming styles where it's easy to track the lifetime of objects and data blocks. But in general, you still have quite a bit of work to do at runtime.

• 9:40Ryan Peterman?

  I think a lot of people, for garbage collection, they might think of it as a binary thing, or it's either you have it or you don't. But I wonder, in OCaml, is there some way to like turn down the memory management and do some manual, so kind of like a mixture to have the benefits of both?

• 10:00Speaker 00

  So that's one of the things that the Jane Street people are looking at. So they have their OX-CAML variants, oxidized OCAML, which is kind of OCAML with some inspiration from Rust. So it's still very experimental, but yeah, they've been playing with things like stack allocation of some data structures so that they're automatically deallocated when the function returns. It's quite cheap. Yeah, there are a few things you could try, but I'm not sure they are going to make such a big difference. I remember doing, with a student, some experiments with stack allocation of data structures a long time ago, and you don't win as much as you would think.

• 10:43Speaker 00

  Basically, garbage collection or heap allocation is pretty cheap for objects that have a very short lifetime. Okay, if they die before the next garbage collector, they will cost very little in garbage collection time. But it's more expensive for long-lived data structures, okay, because those will be scanned and analyzed multiple times. And stack allocation works for the first kind of objects, things that have short lifetime anyway. So you don't win as much as you think.

• 11:20Ryan Peterman?

  One of the most popular programming languages, JavaScript. Curious, when you think about the difference between JavaScript and OCaml, what's the main thing that comes to mind?

• 11:31Speaker 00

  Yeah, I'm not a big fan of JavaScript. Well, so JavaScript is, well, first, it's very dynamic. So type checking is entirely dynamic, but it's more than that. I mean, pretty much everything can be redefined at runtime, including, I don't know, the semantics of method invocation, for instance. So really, some pretty fundamental aspects of the language are very flexible. So some people say, oh, that's great. We can do lots of meta programming, et cetera. And to me, it also, it's a big weakness. I mean, it makes programs that can be very fragile and also have some security issues.

• 12:13Speaker 00

  So yeah, so JavaScript is a ultimate dynamic language, in my opinion. While OCaml is very static, static typing, static binding. Pretty much everything is fixed at compile time. Okay.

• 12:26Speaker 00

  And then, well, I guess it's a kind of a different data model. JavaScript is a little more object oriented in the way it presents data. Maybe that's not that important. And to say one good thing about JavaScript is that it also contains a decent functional language inside. You know, there's a little bit of a little core of JavaScript, which is basically Lisp and can be used to do functional programming if you want. And actually, the designer of JavaScript, I think, was a former Lisp person. I can't remember his name, but...

• 13:05Ryan Peterman?

  Brendan Icke, maybe?

• 13:07Speaker 00

  Yeah, Brendan Icke, yeah. There's a little bit of heritage from Lisp to JavaScript.

• 13:14Speaker 00

  But a very dynamic kind of Lisp.

• 13:17Ryan Peterman?

  You said you weren't the biggest fan. Is that just because of the dynamics? Or is there some other aspect?

• 13:22Speaker 00

  Yeah, mostly the dynamics. I think they really went overboard with that. This kind of meta meta object protocol where you can really find the semantics of very basic operations like method invocation. The fact that a method can, there's a lot of introspection. A method can look at its own call stack, look at its colors, look at the code of its colors, which is a security nightmare. All those things, I think, are completely unnecessary and not conducive to good programs.

• 13:57Speaker 00

  Easily abused, no, easily abused.

• 14:00Ryan Peterman?

  I think on the topic of functional languages compared to imperative languages, there's this thought that functional languages are kind of harder to learn or maybe they have more perceived complexity. And actually, when I'm on my research, there's this popular quote from the designer of Go, Rob Pike. And he's talking about what they intended to do with Go. And he said, you know, the key point here is the programmers are Googlers. They're not researchers, you know, they they're young, fresh out of school. They're not capable of understanding a brilliant language. And I think, you know, that that thought of a brilliant language is often attributed to functional languages.

• 14:44Ryan Peterman?

  What do you think about, is a language like OCaml harder for programmers to grasp than imperative languages?

• 14:51Speaker 00

  I think functional programming is not fundamentally harder, especially if you have a little bit of mathematics background. So coming back to the quote by Rob Pike, I think it described very much how they go about hiring at Google. Okay, they they hire a lot of engineers who are fresh out of of college. Some of them have master's degree, but and then they train them internally. Other companies, I think, try to to hire people with more education and perhaps more diverse backgrounds.

• 15:28Speaker 00

  And yeah, so Jane Street, for instance, and some others use OCaml as a filter on who they want to hire. Yes, they have fewer applicants, but in general, they have more interesting backgrounds.

• 15:44Speaker 00

  And perhaps one last thing I would like to say, Python is 50% functional language. Okay, a lot of good Python code looks like functional code with comprehensions. So I think people are already halfway through functional programming when they are comfortable with Python.

• 16:05Ryan Peterman?

  Yeah, when I was learning OCaml in college, I think one thing that really stood out to me, and I thought was interesting, was this concept of type inference, where the compiler is kind of, it knows the types of everything implicitly in the way that the code is written. Can you explain type inference and what the advantages are?

• 16:27Speaker 00

  Well, the basic idea that you don't have to declare the type of every variable you introduce, every function parameter, every local variable, because quite often the type can be deduced from the uses of the variable. Okay, like if you do, I don't know, x equals string length of s, then you kind of know that s is a string and x is an integer, because that's what the string length function, that's the type of string length, and it tells you that.

• 17:00Speaker 00

  So that's a basic idea. Now, the actual realization is a little more complicated. Basically, you need to collect a number of, the compiler needs to collect a number of constraints, and then try to solve them. See, well, if there's no solution, then it's a type error. But sometimes there are several solutions, and you must find good criteria to choose one. Otherwise, you're, I mean, it also needs to be predictable for programmers. And often also, you can, you can still put type annotation. As a programmer, you can still put type annotations if that makes the code clearer. So I think the main advantage is precisely to have less verbose code, less verbose code, where you don't

• 17:46Speaker 00

  You don't need to put types everywhere, but only where they help a documentation and documenting the code and making it easier to read. Okay. But quite often, you for like small local functions, for short-lived temporary variables, you the type is obvious from the context. So let's just omit it.

• 18:13Ryan Peterman?

  If I'm trying to figure out how this type inference works, the intuitive example you said makes sense. But you mentioned it seems to be some sort of system of equations that you solve or something like that. Can you give a concrete example? Maybe, you know, what does that look like to the compiler?

• 18:29Speaker 00

  Okay, well, for a slightly more complex example, say you have a function with two parameters, x and y, and then you do if x equals y. So that tells you that x and y have the same type, but that still doesn't tell you which type it is, assuming a polymorphic equality comparison. So you've learned something about x and y, that they have the same type, but you still don't know what the type is. And later, maybe you will learn something about the type of x. And now you will have determined the type of y as well. So that's the kind of constraints you accumulate and solve, a little bit like, you know, Sudoku or those kind of puzzles.

• 19:12Speaker 00

  And then there's the interesting case where you don't have enough constraints to find a unique type. So maybe in the end, x and y will be, you know, they have the same type, but it's still unconstrained. And then that's where you automatically get polymorphism for free. Okay, the type checker says, okay, those types are unconstrained, so it can work for any type. So my function can take an x of any type and a y of the same type, again, any type, and it's a polymorphic function. So there's this beautiful, I think, phenomenon that polymorphism can be discovered just by running type inference and noticing that, oh, there are no constraints, so it must

• 19:57Speaker 00

  be polymorphic. And that was a guide insight by Robin Milner, the British computer scientist pioneer, who invented this ML family of languages and this kind of type inference in the 70s. Polymorphism was not very well understood at the time. And so the fact that he could have, he could introduce polymorphism so easily in his language just as a consequence of type inference was a beautiful discovery.

• 20:27Ryan Peterman?

  So for type inference, it seems like the benefit is, you know, the code is going to be a lot more concise because we don't need to write out all the types, which seems nice. But what are the trade-offs of adding type inference to a programming language?

• 20:43Speaker 00

  Well, as I said, error messages can be, type error messages can be very confusing because they not always point to the actual source of the type error. The system may have done some wrong inferences and will report some of those inferences instead of reporting the source, the actual source of the type error. So it's been, it's been a subject of much research and there's no very well-defined idea of the source of a type error, basically. So, yeah, so errors can be an issue. Some features of type systems are easy to combine with type inference, to handle with

• 21:28Speaker 00

  type inference, and some are harder. For instance, when it comes to genericity, so I mentioned the polymorphic, parametric polymorphism, which is very well handled, but subtyping, the kind of thing you have in objective anti-language is actually harder to combine with type inference for super-technical reasons that I'm not going to go into. So sometimes you have to make a choice, either you have type inference but it is less powerful.

• 22:02Speaker 00

  Or you have a full type inference, but a more restrictive type system. And that choice is part of the language design, actually.

• 22:14Ryan Peterman?

  You mentioning this solver kind of reminds me of the topic of formal verification. Could you explain what formal verification is?

• 22:23Speaker 00

  Well, the idea that for some programs, you want strong guarantees that the program is correct and guarantees that are hard to get just with testing and reviews, code reviews. You know, there's this famous quote by Deichstra, the Dutch computer pioneer, which goes something like, "Testing can only show the presence of bugs, but not their complete absence." Because in general, there's infinitely many inputs to your program and you cannot test them all. So you're only testing a sample and then sometimes you have surprises.

• 23:07Speaker 00

  So what if you want to make sure that the program is correct for an infinite number of inputs? And that's where you need to turn to the so-called formal methods. So you're using mathematical reasoning, you're using static analysis algorithms on your program to really analyze all possible executions of a piece of code and making sure that it matches a specification. The specification can be very simple, like the code will never crash, given well-formatted inputs. So that's a fairly simple property, but still extremely useful because code that crashes is always code that can be attacked. It's often a security hole.

• 23:54Speaker 00

  So for instance, all accesses within, all array accesses are within bounds.

• 24:01Speaker 00

  That's a very simple property. And it's very hard to ensure just by a type system or just by testing. So that's where you need some more advanced formal verification. And then there are much more powerful, much more precise specifications that you may want to check. That can be where the program always terminates. It can be the program doesn't leak confidential data. It can even be where the program computes this mathematical function with an error, floating point error, and I don't know, 10 to the minus 6. Okay, something like that, something very precise like that.

• 24:42Speaker 00

  And so it's been a really hot topic in software sciences since the, at least the 70s, I would say. There's lots of techniques, some are just fully automatic, like static analysis. But they're already pretty good at finding bugs and making sure that some bugs, like out of bounds, are not there. And some are a lot more interactive and require a lot more program assistance to write specifications and then do so-called program proofs, so proving mathematical statements about the program.

• 25:19Ryan Peterman?

  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?

• 25:30Speaker 00

  So yeah, so Lean is an example, an instance of the so-called provers or proof assistance. So originally, those were developed to do mathematics on the computer. So not, 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. Well, originally, everyone focused on automatic theorem proving, so having the machine find proofs all by itself. But that's very, very difficult.

• 26:12Speaker 00

  And not necessarily what mathematicians need. And so those proof assistants are more like, well, formal languages, like programming languages, but where you can write mathematic definitions, 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 R or Isabel or one of those tools, and it is rechecked

• 26:57Speaker 00

  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 kinds of problems you can have with a pencil and paper proof. And so in the end, you get proofs that are extremely reliable, extremely credible.

• 27:21Speaker 00

  And 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.

• 27:41Speaker 00

  I think there's a recent example with a weak Goldbar conjecture. So part of the proofs involve checking a whole lot of inequalities, 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:07Speaker 00

  And 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. Okay, but then they have to be checked by humans. Unless the 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:38Speaker 00

  So yeah, so 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 of programs.

• 28:55Speaker 00

  And so I spent many years proving the correctness of a compiler, C compiler, using one of those tools, the RAC proof assistant.

• 29:10Speaker 00

  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 faithful to the C code. So there's no miscalculation. The compiler didn't introduce a bug in the program that wasn't there originally. And 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.

• 29:49Speaker 00

  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. Okay, you 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.

• 30:23Speaker 00

  So yeah, so it's really a programming taken to a higher level.

• 30:28Speaker 00

  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.

• 30:41Speaker 00

  Yeah, and I should also mention another great example of verified software. It's a micro kernel, the SEL4 micro kernel, developed in Australia, and which is used as an 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. And it's been proved correct. Every line has been proved correct, and that's a very big achievement.

• 31:20Ryan Peterman?

  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?

• 31:46Speaker 00

  Let's say you have a function that takes three numbers, x, y, z, and returns the average of those numbers. Okay.

• 31:58Speaker 00

  Only, 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. Okay, so not exactly the formula for the average.

• 32:22Speaker 00

  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 want a language like C, you can have arithmetic overflows. Okay, when you compute x plus y or plus z, you can overflow the range of representable integers. And in C, it's a bug, it's an undefined behavior.

• 33:07Speaker 00

  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, 0 and 1 million, for instance, but no bigger than that." And 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,

• 33:50Speaker 00

  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. Okay, so basically you're stating a contract for your function. A pre- hypothesis on the arguments, guarantees on the results. And you want to prove, analyze the function body to show that this contract is respected.

• 34:23Speaker 00

  I hope it's a little more concrete.

• 34:25Ryan Peterman?

  So it 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.

• 34:38Speaker 00

  Yes, maybe not Lean by itself. Well, a program prover, 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. Okay, that what does a plus means, what does assignment means, okay? Lean Lean is mathematics. You don't assign in mathematics. You don't say x equals x plus one, or or or you're just comparing x and x plus y, and it's always false. There are no assignment in mathematics. There's assignment in many programs. So you need to make it explicit that

• 35:19Speaker 00

  there are three different states for the t variable, three different values, and and and relate those values to, well, the program defines where those values are. And then a prover like Lean can can reason about those three successive values. Because now you're in part, you're in mathematics. And and that that's kind of a bridge between programs and their mathematical meaning is called semantics, that the field of semantics of programming languages, it's been a big topic in in PL research since the the 60s at least.

• 35:56Ryan Peterman?

  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?

• 36:08Speaker 00

  Absolutely. Yeah, you're 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 so you need a way to to reason about termination. And also, yeah, sometimes, the arithmetic you get in the programming language is not

• 36:51Speaker 00

  integer arithmetic, or it's not reals, you know, it's floating point, it's not reals. 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 CompSure, 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:22Ryan Peterman?

  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?

• 37:39Speaker 00

  Okay, so what the computability theory says is that there is no algorithm that will always, that can always say, this program terminates, or this program doesn't terminate.

• 37:52Speaker 00

  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.

• 38:06Speaker 00

  So it will not work.

• 38:09Speaker 00

  But still, for many programs, you can succeed, okay? 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 your mathematician. Okay, 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, okay?

• 38:52Speaker 00

  They are pretty much all undecidable. So you know that there is no static analyzer that will always find all problems, all problems in all programs. But still, you can try. Okay, 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:19Ryan Peterman?

  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. You can check them out at workos.com to learn more and get started.

• 40:01Ryan Peterman?

  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. And 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?

• 40:30Speaker 00

  Well, there were engineering challenges, that's for sure. There were also some language design issues. So but let's talk about the engineering challenges first. So it's true that when you have a language with an runtime system, a memory allocator or garbage collector. Well, at least the one of for OCaml was really designed with sequential executions in mind. So if you have, if you add 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 you could always, you know, take take a look at at every operation in the heap.

• 41:16Speaker 00

  But then you would sequentialize your programs. Basically, they they they would run as slowly as a single processor. So so that's not interesting. So, yeah, so there were engineering challenges. And yeah, I was at least initially quite quite reluctant to basically re-implement a complete garbage collector and and memory allocator and large parts of the runtime system. That's what we did eventually with, well, it was done mostly by the team at O Camel Labs in at Cambridge University. But, yes, it was a really big rewrite.

• 41:54Speaker 00

  But then I said there was also a language design issue, which is that for for the longest time, well,

• 42:04Speaker 00

  now, when 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. You 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 notice. You know, and I I've never liked this model of of communication.

• 42:38Speaker 00

  I mean, it's a bit like if you want to communicate with your neighbor, then then you you you break into their houses and their house. And then you move the furniture around. And then when they are back, they say, oh, something, 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 and that would be things like message passing, which is a completely different form of communication, much higher level. So, yeah, so for the longest time, I was really interested in message passing concurrency.

• 43:12Speaker 00

  And there's, for instance, a functional language called Erlang, that was built on those ideas and 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, so to get the same effect, so you will pay more for it.

• 43:53Speaker 00

  Anyway, 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 threads want to access the same location, and maybe they want to modify it in different ways. And so sometimes, parts of the C/C++ 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,

• 44:37Speaker 00

  which says, "Well, what happens is like an interleaving of reads and writes of your program." You don't know which interleaving, but there is an interleaving.

• 44:47Speaker 00

  But that doesn't work with modern processors, multi-core 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 programmers some guarantees about the ordering of reads and writes, concurrent reads and writes, while not constraining the hardware too much.

• 45:17Speaker 00

  And it's very difficult. So Java went through like five different iterations of the memory model. Some were too straight, some were too lax, some were inconsistent, where 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, when the, 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

• 46:01Speaker 00

  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. And sometimes I feel sorry, our users are exposed to that. Okay. So that explains why it took so long. Solving the engineering challenges, but also having, agreeing on a memory model and what kind of guarantees we are going to give to programmers. Oh yeah, I forgot to say one thing, which is that, so C and C++ there's a lot of things you can say, oh, it's just undefined behavior, anything can happen.

• 46:46Speaker 00

  In type safe languages like Java and OCaml, you want to give stronger guarantees. Okay. Maybe many things can happen, but your data should, should remain well typed. Okay. Typically, you don't want to expose an object to another thread before it's been fully initialized, for instance. And, and that's, 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, to, to guarantee this. So yeah, type safety in the presence of shared memory concurrency is, is not obvious at all.

• 47:27Speaker 00

  So that's why it took so long.

• 47:30Ryan Peterman?

  So in Python, I know there's the famous Gil or the global interpreter lock. What is that lock protecting? Is it the cleanup of objects on the heap? Or is it something else?

• 47:42Speaker 00

  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 side safe, as we said, you can protect the non-side 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. And 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,

• 48:26Speaker 00

  when you're going to block for a long time, or when you're calling into C code that is side 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 in another language. But you still have mutual exclusion between your, between two threads running Python or running OCaml before multi-core OCaml.

• 49:04Speaker 00

  So you get some benefits, like concurrent I/O, but you don't get any parallelism. Okay, you don't get a speedup 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.

• 49:32Speaker 00

  There's probably a few places in the OCaml runtime system that still use locks to ensure mutual exclusion, like in the I/O subsystem.

• 49:43Speaker 00

  And some phases of the garbage collector, I think that has a phase which is kind of stop the world where you need to make sure that everyone, no, no, no OCaml code is, is running. For, for 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. So yeah, that, these are tricky things. And I don't know what the Python people are up to with their gear, if, if they finally managed to remove it or they are still working on it, but I, I, I've heard they are making progress, so.

• 50:17Ryan Peterman?

  Yeah, 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?

• 50:30Speaker 00

  Oh, it's another can of worms. Well, there are two aspects, there, there are the, the control flow and there are the, the data. So the control part is, is not that hard. So yes, you need, you need a mechanism so that your, your Python interpreter or your OCaml compiled code will actually jump to the C function. So for OCaml, basically you, 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 OCaml calling conventions, but the, the compiler

• 51:15Speaker 00

  knows about that. And so it will call the C function, maybe through a little bit of glue code or whatever, and then the C function will execute and, and return back to the OCaml code. That'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, 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, in C and it's not a double, which is not allocated, it sits in register.

• 52:01Speaker 00

  So typically, the C code needs to use a so-called foreign function interface, so some C function and macros provided by OCaml to access OCaml data, OCaml arguments, you know, extract the part that it needs, the numbers. The, yeah, 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.

• 52:44Speaker 00

  It's not exactly the same code that you would do to access a C array from C. Okay, so you need accessors. But now, if you want to, 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 OCaml 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 be your garbage collection. So the C code must also kind of cooperate with the garbage collection, with boot registration mechanisms, et cetera, et cetera. So there's quite a bit of work to be done.

• 53:29Speaker 00

  And then different foreign function interfaces arrange this work differently. So the base FFI for OCaml, basically, it's a C code that must do all the work. But then it can be very fast, 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 the description of the C type of the C function, and you can automate some of those conversions. But sometimes it can be tricky, it can be expensive. For instance, you may end up copying a whole array,

• 54:11Speaker 00

  while your C code only needs to access two or three elements in it. Okay, so there's lots of trade-offs. And quite frankly, it's a dirty part of programming language implementation. The OCaml FFI is... Not that clean, but if you get the Java FFI, for instance, it's also quite complicated. And for Python, I've I never tried, so I don't know what it looks like. But yeah, it's it's a necessity, but but it can be quite hard because the data models are different between the two languages.

• 54:49Ryan Peterman?

  So to kind of get the big picture, on the OCaml side, there's an interpreter, which is a program running in 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. And the C program is a binary somewhere. And the OCaml interpreter then starts to load those instructions and execute them.

• 55:18Speaker 00

  OK, 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 so in in in compiled mode, what what you say is how you put together the OCaml code and the C code is done by the linker, the C linker. So so so basically, someone else is doing that for us. And and and it's not that different from linking together two object files produced by C or two objects transported by OCaml.

• 56:00Speaker 00

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

• 56:17Speaker 00

  So and and and then there's a little bit of introspection. So at some time, the interpreter with 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, it's there's this additional level of complexity on top of it.

• 56:44Ryan Peterman?

  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.

• 56:55Speaker 00

  Yes, in the simplest case, yes.

• 57:00Speaker 00

  There are also dynamic loading facilities in OCaml, 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. Okay, like, oh, where is this DLL? Or DLL not found, for instance, problems.

• 57:21Speaker 00

  But of course, you lose a little bit in flexibility.

• 57:25Speaker 00

  But yeah, I think the static linking has a lot to... It 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:41Ryan Peterman?

  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 LLM can produce. And what are your thoughts on, you know, how to address that kind of problem?

• 58:04Speaker 00

  It's a tough problem. I mean,

• 58:09Speaker 00

  globally, I'm a little bit skeptical about generative AI. Of course, they can do amazing things that were unthinkable like a few years ago. But there's also, there's always some errors. It's, you can't really trust what's being produced by generative AI. And so the...

• 58:37Speaker 00

  In principle, humans should be there to check the output and and fix errors or ask the L L M to fix its own errors. Until the result is actually usable. But of course, it's very hard because there's a slop problem. Okay, A I is produce so much. It's so it's so easy to produce. Uh, to produce a large number, large quantities of text, of code, pictures, whatever. That that that in the end, there's there's no human. Uh, no, no, no human time to to check it all. So, yeah, recently I heard.

• 59:22Speaker 00

  Uh, when someone working in an A I startup who was enthusiastic about. Uh, uh, yeah, genetic code saying that thanks to genetic A I, the cost of programming is dropping to zero. But well, the cost of writing code maybe, but um, what about, you know, checking it? Uh, making sure it is correct. Um, that it does what we want that um, well, that that cost is not zero at all. Uh, and and for me, uh, every new line of code is a liability. You know, you you have to test it, you have to check it, maybe you have to do formal verification. You have to uh, evolve it, maintain it uh, later. So so, no, I don't want huge amounts of code.

• 1:00:07Speaker 00

  Okay, I want there was fifty lines of code that have been thought that have been polished over the years. So anyway, uh, I'm not getting that with A I. Um, uh, and and and I think that's a problem. Uh, uh, and this idea that humans will be there to check. Uh, the output of genetic A I is just, oh, no. They they they are not available for that. They, uh, there's too much of it and it's and it's not, it's not pleasant either. Okay, I mean, I don't think it's a good way to to to split the work between machines and and humans. So anyway, uh, so maybe there will be some.

• 1:00:47Speaker 00

  Societal uh uh solution like a big uh no to AI slop uh movement. So we we we're trying to see that in some open source uh projects that that refuse. I generated uh contributions because there's just too many. Uh I know that well for for for OCaml and especially for Concert have have received um uh uh issues. Uh I part of issues that were obviously generated by AI. And there was maybe one good issue among ten reports, okay? And and and each report was several page long and with, you know, very detailed explanations and repro case that in the end doesn't repro anything or or repro reproduces something else.

• 1:01:31Speaker 00

  And but but it takes time to to go through all those things and and maybe at some point I will say no to to AI-generated uh contributions. Okay, but maybe there's also a bit of a technical solution, which is, as as we said earlier, um how to have AI produce proofs. Uh so evidence that uh its creation is correct. So as I said, this is starting to work for uh mathematical proofs. Some generally VIs are able to produce proofs both in English and in the formal language of the Lean Prover, for instance. And so you can get uh a lean to recheck the proof and get some confidence.

• 1:02:13Speaker 00

  You still need to be very careful about uh the statement. Uh because sometimes uh AIs will change the statement or the definitions to make the proof easier. Uh that that happens. Um uh and also you you should be careful about uh so-called self-formalizations, where the the AI also comes up with some definitions uh and some statements by parsing a PDF file or whatever. And and sometimes it introduces errors at that point. So anyway, there are still need uh a need for human review, but on smaller quantities of uh of text and and mathematical uh text.

• 1:02:58Speaker 00

  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 that the program satisfies some specification.

• 1:03:15Speaker 00

  So 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 can be difficult too. And well, mathematicians have a lot of experience, you know, in stating finding definitions that they find interesting and stating the theory and said that that they believe should be true or that that will mean something. Or computer programmers are less good with that.

• 1:03:57Speaker 00

  And it's fairly easy to come up with specifications that are inconsistent or impossible. So remember this average function of when there was a precondition of the three numbers, three arguments, saying they must not be too big. But say maybe you can end up with a precondition that that just cannot be satisfied.

• 1:04:20Speaker 00

  And

• 1:04:22Speaker 00

  and at this point, the body of the function will always be verified. Okay, even if it's completely wrong, because because the assumption says basically this function cannot be called.

• 1:04:34Speaker 00

  And and so you get a false sense of confidence. You verified something, but but it's actually unusable. And and and that's a fairly delicate point. Where I'm not sure LLMs are going to or AI is going to help much. But but it's a problem with formal methods in general. And and some possibilities include

• 1:04:59Speaker 00

  the ability to test specifications, for instance.

• 1:05:04Speaker 00

  So instead of using your test suite to to to see if your code works out, you can also use it to see if your spec

• 1:05:14Speaker 00

  checks out.

• 1:05:17Speaker 00

  Those kind of things, but yeah, we we are kind of moving some of the difficulties from the programming phase to the specification phase. But we still have some problems.

• 1:05:30Speaker 00

  Anyway, so that might be a way to to deal with the AI-generated code and and and develop some confidence in it.

• 1:05:39Ryan Peterman?

  You know, 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. Like, 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?

• 1:06:08Speaker 00

  Yeah, a couple of years ago, someone asked me about that, and and there was there was a concern that the training data would be, there wouldn't be enough training data in OCaml for for an LLM to really learn how to program in OCaml. And it's true that there is less OCaml code in the wild than JavaScript code, for instance.

• 1:06:32Speaker 00

  But apparently, contemporary LLMs do do do well with with the amount of OCaml code they have. Oh, maybe because there's enough, maybe because learning has become a little more efficient, maybe because, well, there's there's there's less OCaml code than JavaScript code, but maybe the OCaml code is better quality average on average. I don't know. Anyway, maybe LLMs are getting better also to to transfer knowledge from that they've learned from one language to another. That that could be. I have no idea how those things work.

• 1:07:12Speaker 00

  But yeah, so so the latest feedback I've got about LLMs and, well, yeah, generative AI and OCaml is that the the OCaml code generated is is quite decent and quite similar in quality to to to more popular languages. And one thing that seems to help the generative AI is the type system. So the the fact that there are some static checking just of the types.

• 1:07:41Speaker 00

  It it's already effective in, you know, the avoiding some some errors and maybe encouraging the LLM to like like declare types first. So so give give some type structure to the program. All right. And now from 10 years from now, it's it's it's difficult to guess. So will it be the more 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 uh uh well, because there's fewer errors in the end.

• 1:08:25Speaker 00

  Um, I'm hoping it will be the safer languages, but I really don't know.

• 1:08:31Ryan Peterman?

  I've seen in the industry, there's a few cases where because it's so easy to generate code, uh 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 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:13Speaker 00

  Well, so today, uh it's in well, I've heard mostly about C and C++ to Rust uh translations, uh hoping that the generated Rust code will be safer. Uh, they said I've seen at least one project when the generated Rust code is entirely in unsafe blocks. So so it's really kind of line by line translation of the C code, you know, is uh but well, uh but maybe it can still be used as a starting point for making it safer later.

• 1:09:45Speaker 00

  Uh, so yeah, I would say today, uh I I can imagine significant efforts being being done with Rust as the as the target language. In the functional world, I'm not quite sure. Well, maybe, oh, well, uh, maybe a functional language to one of those proof assistants, uh like like Lean or Hark, because they they also have uh. Programming languages, 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.

• 1:10:28Ryan Peterman?

  When you compare industry versus academia today, where would you say most of the innovation in programming languages comes from? And also, has that changed over time?

• 1:10:41Speaker 00

  Okay, well, I think the most of the innovations have come from industry lately. And that wasn't the case in the early days of computer science.

• 1:10:56Speaker 00

  If you think of, I mean, the truly innovative languages like Algor, Lisp, Prolog, Smalltalk, were developed in mostly academic settings. Well, Smalltalk was Xerox PARC, which was an industrial research lab, but very, very far away from industrial customers. And then there were, you know, much more practical languages, and uglier languages developed typically at IBM, like Fortran, COBRA, PL1, et cetera. And then, so really the idea that the nice ideas come from academia and nature there.

• 1:11:42Speaker 00

  And then, well, the nice ideas from academia started to be transferred by industry much, much more quickly. I'm thinking of C, and especially C++, and then Java, which really took ideas like object orientation and, well, garbage collection, automatic memory management in industry. Before Java, it was just, you know, crazy academics in the ivory tower that were using garbage collected languages. It's 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.

• 1:12:27Speaker 00

  And Java also popularized type safety, back code 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. And, well, Rust is even more spectacular, I would say, because, well, algebraic data types, garbage collections, etc. Those were already present in academic languages, like, well, Cmel, for instance, but Rust really took very recent research results of the 2000s on safe low-level programming that were basically

• 1:13:10Speaker 00

  never implemented in any language and managed to do a consistent haul from that. And so I'm really admiring, 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 INRA on a

• 1:13:53Speaker 00

  research position, when I was hired as someone who had developed first versions of Cmel, well, predecessor of Cmel, and who was working on type systems for programming languages and so on. But then some people told me, but there's no future in programming language research, right? Industry has decided it will 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 functional, on a particular programming language.

• 1:14:35Speaker 00

  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 they're still real interest for better languages, and I think this will continue, and I think it's good for the computing field.

• 1:15:06Ryan Peterman?

  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?

• 1:15:35Speaker 00

  So, yeah, I think, well, 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 L L V M, or some domain-specific languages like Hylite, which are pretty good, you know, those tensor, domain-specific languages for tensor computations are getting a little better.

• 1:16:04Speaker 00

  But still, I find it a little bit frustrating that I cannot do, I don't know, theorem proving on a GPU. I have absolutely no idea how to go about that, and in part by lack of an appropriate language. Okay.

• 1:16:20Speaker 00

  So I'm not ready to program the GPU pipelines at a very low level myself. So, and I think it's more general. I think we are not using all these GPU and other highly parallel hardware as much as we could. Yeah, so verifying applications that have been learned or generated, 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, I don't know, computer vision, self-driving cars,

• 1:17:01Speaker 00

  or some numerical computations like, you know, weather prediction and so on. So specialized L L Ms, but you still want some guarantees about what they produce, that they cannot produce completely inconsistent outputs, for instance. There were some attempts in the last years at using static analysis tools and basically program verification tools.

• 1:17:26Speaker 00

  Applied to L L M's, but well, it it it doesn't scale. Uh, L L M's are bigs, uh, sorry, uh, neural networks are big. And for L L M's, uh, there are also a a distinct act of specification. Okay, you you don't really know what what's a good answer from an L L M. Well, you you know it when you see it, but you cannot write a mathematical specification of it. So so that part is probably over. What I would say are the big problems for today. Yeah, probably maintaining software quality despite A I slope, despite a lot of pressure to throw away traditional software development techniques.

• 1:18:10Speaker 00

  Using L L M's as an A I as much as we can to do mechanized proofs. So proofs that can be checked by machines. Maybe this will be the the decade of formal verification of software. We've been waiting for that for fifty years, so maybe it will it will finally take off.

• 1:18:30Ryan Peterman?

  What's your top book recommendation for software engineers and why?

• 1:18:36Speaker 00

  Well, this this is an old one, The Programming Purs by Bentley. I think I read it when I was a PhD student, but I think it's it's nice as um, showing how very talented programmers work, how they think about their programs. So it's it's it's a combination of choosing the right algorithms, expecting them clearly, knowing when to stop, when when to use a simple algorithm where where when a more complicated one is not needed, uh, having a sense of elegance in in the code you write. Um, uh, having a feeling for where the problem is when when the the code misbehaves.

• 1:19:19Speaker 00

  So all those kind of things that are hard to communicate. And I think those those pearls that are very easy to read and and and don't use any complicated data structures, don't use any complicated language. I mean, it is is kind of timeless, you know. Um, uh, I think those pearls are are good illustration of that.

• 1:19:41Speaker 00

  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 "How to Design a Program", which is a fairly ambitious title as well. And this comes from the Scheme community. Okay, Finaisen, Finler, Flat and Christian Murphy. And those people have developed, well, the Scheme community is famous for having developed pedagogical resources that are, I mean, ways to teach programming that go beyond teaching functional programming, basically. And so there was the MIT course "The Interpretation of Computer Programs",

• 1:20:26Speaker 00

  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, 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. Okay.

• 1:21:10Speaker 00

  And then how, given a language like Scheme, which is pretty flexible, how the code kind of follows naturally.

• 1:21:19Ryan Peterman?

  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?

• 1:21:27Speaker 00

  Sometimes I regard that maybe I specialized a little too early in programming language research, or maybe...

• 1:21:39Speaker 00

  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 sixty.

• 1:21:55Speaker 00

  Maybe not as

• 1:21:59Speaker 00

  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 to get a everyone who's serious about working in computing to get a fairly diverse computer science background, even even for topics that look super theoretical and not very relevant to to everyday

• 1:22:27Speaker 00

  jobs. Well, 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.

• 1:22:42Speaker 00

  And then it also helps understanding new problems.

• 1:22:47Speaker 00

  Like with quantum computing, what can you do with a quantum computer that you cannot do with a normal computer? Oh, and and and it's it's time to to revisit all of the classic complexity theory I learned earlier and when I was young. And and so, yeah, I think I think it's good to have those this kind of background, even if it's not obvious you will be using it every day. And and sometimes I wish I had taken time to accumulate a little more of this background before specializing in programming languages.

• 1:23:25Ryan Peterman?

  Awesome. Well, thank you so much for your time, Professor Leewer. I appreciate it.

• 1:23:28Speaker 00

  Thank you, Ian. That was nice.

• 1:23:31Ryan Peterman?

  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 Lizkoff, 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. 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

• 1:24:14Ryan Peterman?

  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.