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

Xavier Leroy discusses the creation of OCaml, the development of the CompCert verified compiler, and the role of formal verification in software.

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: read.compose.llc/ • The Kickstarter page for it: kickstarter.com/projects/ryanlpeterman/compose-simple-ergono… 𝗣𝗼𝗱𝗰𝗮𝘀𝘁 𝗹𝗶𝗻𝗸𝘀: • Spotify: open.spotify.com/episode/7cdatlBEkAjx4XplVLjFxN?si=T0dXjBf2T… • Apple: podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835 • Transcript: developing.dev/p/creator-of-ocaml-functional-programming 𝗧𝗵𝗮𝗻𝗸 𝘆𝗼𝘂 𝘁𝗼 𝘁𝗵𝗶𝘀 𝗲𝗽𝗶𝘀𝗼𝗱𝗲'𝘀 𝘀𝗽𝗼𝗻𝘀𝗼𝗿 𝗳𝗼𝗿 𝘀𝘂𝗽𝗽𝗼𝗿𝘁𝗶𝗻𝗴 𝗺𝘆 𝘄𝗼𝗿𝗸: • 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 workos.com/ 𝗧𝗶𝗺𝗲𝘀𝘁𝗮𝗺𝗽𝘀: 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 𝗪𝗵𝗲𝗿𝗲 𝘁𝗼 𝗳𝗶𝗻𝗱 𝗫𝗮𝘃𝗶𝗲𝗿: • Wikipedia: en.wikipedia.org/wiki/Xavier_Leroy • Website: xavierleroy.org/ 𝗪𝗵𝗲𝗿𝗲 𝘁𝗼 𝗳𝗶𝗻𝗱 𝗥𝘆𝗮𝗻: • Newsletter: developing.dev/ • X/Twitter: x.com/ryanlpeterman • LinkedIn: linkedin.com/in/ryanlpeterman/ • Threads: threads.com/@ryanlpeterman • Instagram: instagram.com/ryanlpeterman • TikTok: tiktok.com/@ryanlpeterman 𝗥𝗲𝗳𝗲𝗿𝗲𝗻𝗰𝗲𝗱 𝗶𝗻 𝘁𝗵𝗶𝘀 𝗲𝗽𝗶𝘀𝗼𝗱𝗲: • CompCert verified C compiler: compcert.org/ • seL4 microkernel: sel4.systems/ • Programming Pearls (book, not an affiliate link): amazon.com/dp/0201657880 • How to Design Programs (book): htdp.org/