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

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