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-done

Podcast 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-programming

Thank 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) Outro

Where 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/@ryanlpeterman

Referenced 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/

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

The Peterman Pod

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