
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-donePodcast 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-programmingThank 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) OutroWhere 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/@ryanlpetermanReferenced 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/
Podzilla Summary coming soon
Sign up to get notified when the full AI-powered summary is ready.
Free forever for up to 3 podcasts. No credit card required.

Turing Award Winner: Early AI, LLM Predictions, Causality | Judea Pearl

Turing Award Winner: TPU vs GPU vs CPU, Computer Architecture, RISC vs CISC | David Patterson

Turing Award Winner: NSA, Public Key Cryptography, Crypto Wars | Martin Hellman

MIT Complexity Theorist: Why You Can Do Better Than “Optimal” On Leetcode & SAT | Ryan Williams
Free AI-powered recaps of The Peterman Pod and your other favorite podcasts, delivered to your inbox.
Free forever for up to 3 podcasts. No credit card required.