In this episode of ACM ByteCast, Harald Störrle hosts ACM Fellow and Software System Award recipient Xavier Leroy, professor at Collège de France and member of the Académie des Sciences. Best known for his role as a primary developer of the OCaml programming language, Xavier is an internationally recognized expert on functional programming languages and compilers, focusing on their reliability and security, and has a strong interest in formal methods, formal proofs, and certified compilation. He is the lead developer of CompCert, the first industrial-strength optimizing compiler with a mechanically checked proof of correctness, with applications to real-world settings as critical as Airbus aircraft. In the past, he was a senior scientist at INRIA, a leading French research institute in computer science, where he is currently a member of the Cambium research team. His honors and recognitions also include the ACM SIGPLAN Programming Languages Achievement Award and the Milner Award from the Royal Society.
Xavier shares the evolution of Ocaml, which grew out of Caml, an early ML (Meta Language) variant, and how it came to be adopted by Jane Street Capital for its financial applications. He also talks about his interest in formal verification, whose adoption in the software industry is still low due to high costs and the need for mathematical specifications. Harald and Xavier also dive into a discussion of AI tools like Copilot and the current limitations of AI-generated code in software engineering. The conversation also touches on ACM’s efforts to become a more global and diverse organization and opportunities to bridge the gap between academia and industry.