The Peterman Pod
The Peterman Pod
Ryan Peterman
Creator of OCaml: Functional Programming, Formal Verification, Programming Languages | Xavier Leroy
1 hour 24 minutes Posted Jul 20, 2026 at 10:00 am.
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:
Intro
What sets OCaml apart
OCaml vs Rust
Why is manual memory management more performant
Javascript vs OCaml
Famous Rob Pike quote
Type inference and how it works
What is formal verification and how does it work
What made multicore support difficult for OCaml
How programming languages interface and call each other
The danger of almost-correct LLM code
How LLMs will change programming languages
Industry vs academia
Most interesting unsolved problems
Top book recommendations for engineers
Advice for his younger self
0:00
1:24:27
Download MP3
Show notes
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/