The Peterman Pod

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/

David Patterson is a Turing Award winner famous for his contributions to computer architecture. I interviewed him about his past work, thoughts on GPU/TPUs and career advice from half a century of experience.

• 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/Pn4ZwlEh5nw
• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835
• Transcript: https://www.developing.dev/p/turing-award-winner-tpu-vs-gpu-vs?r=n49ky

Timestamps:

(00:00) Intro
(00:42) RISC vs CISC
(12:51) Compilers
(17:38) GPUs
(23:07) GPU vs TPU vs CPU
(32:12) Is Moores law dead?
(38:04) GPU benchmarks
(41:40) How to have a bad career
(49:59) Courage and optimism
(55:56) Advice for his younger self
(58:15) Outro

Where to find David:

• Wikipedia: https://en.wikipedia.org/wiki/David_Patterson_(computer_scientist)

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:

• AlexNet paper: https://proceedings.neurips.cc/paper_files/paper/2012/file/c399862d3b9d6b76c8436e924a68c45b-Paper.pdf
• David Patterson's “How to Have a Bad Career” talk: https://www.youtube.com/watch?v=Rn1w4MRHIhc
• “Life Lessons from the First Half-Century of My Career”: https://cacm.acm.org/opinion/life-lessons-from-the-first-half-century-of-my-career/
• The 7 Habits of Highly Effective People (book): https://en.wikipedia.org/wiki/The_7_Habits_of_Highly_Effective_People
• Working (book): https://en.wikipedia.org/wiki/Working_(Terkel_book)

Martin Hellman is a Turing Award winner who helped to invent public-key cryptography against the NSA's wishes. I interviewed him all about his work and why it broke the law at the time.

• 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/AZLOETBCQM4
• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835
• Transcript: https://www.developing.dev/p/turing-award-winner-nsa-public-key

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:34) Why his work broke the law
(08:39) How people did encryption before
(18:51) The crypto wars
(26:22) The story behind Diffie Hellman key exchange
(36:48) Signatures vs key exchange
(43:05) RSA patent wars
(48:08) Why inventions happen at similar times
(50:29) What he worked on after cryptography
(57:31) His thoughts on death
(59:40) Advice for his younger self
(01:00:45) Outro

Where to find Martin:

• Wikipedia: https://en.wikipedia.org/wiki/Martin_Hellman
• Website: https://ee.stanford.edu/~hellman/

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:

• Martin Hellman's “The Evolution of Public Key Cryptography”: https://www.youtube.com/watch?v=Tev3tVzH91s
• Keys Under Doormats: https://cacm.acm.org/opinion/keys-under-doormats/
• Cryptography's Role in Securing the Information Society (CRISIS report): https://nap.nationalacademies.org/catalog/5131/cryptographys-role-in-securing-the-information-society
• Secure Communications Over Insecure Channels: https://doi.org/10.1145/359460.359473
• New Directions in Cryptography: https://doi.org/10.1109/TIT.1976.1055638

Ryan Williams is a professor at MIT and the winner of the Gödel Prize in theoretical computer science. I interviewed him all about his work starting by asking him a popular Leetcode question (3 SUM).

Correction: In this podcast I say "lower bound" when I mean "upper bound" and vice versa. Was speaking using the intuition that lower is better for running time. In reality, the accurate usage is:

"Lower bound" = A proven floor for a problem e.g. "no algorithm can possibly be faster"
"Upper bound" = A proven ceiling for a specific solution e.g. "there exists an algorithm this fast"

Professor Williams answers as if I spoke accurately so the error didn't impact the flow of conversation. Just a correction for the record

• 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/AaK1SL2i_4Y
• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835
• Transcript: https://www.developing.dev/p/mit-complexity-theorist-on-leetcode

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:41) Asking him a popular Leetcode question
(03:54) Doing better than the popular optimal solution
(08:26) Fine grained complexity
(17:00) A severe strengthening of P vs NP
(24:38) SAT problems and solvers
(34:51) Hot takes on famous open questions
(46:57) Simulating space with time
(01:01:02) Why he solves hard problems
(01:02:35) How to pick good research direction
(01:07:14) Technical book recommendations
(01:08:31) Advice for his younger self
(01:11:56) Outro

Where to find Ryan:

• Wikipedia: https://en.wikipedia.org/wiki/Ryan_Williams_(computer_scientist)
• Website: https://people.csail.mit.edu/rrw/
• LinkedIn: https://www.linkedin.com/in/r-ryan-williams-a1b534a/
• X/Twitter: https://twitter.com/rrwilliams

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:

• Some Estimated Likelihoods for Computational Complexity: https://people.csail.mit.edu/rrw/likelihoods.pdf
• Simulating Time with Square-Root Space: https://arxiv.org/abs/2502.17779
• Cook and Mertz's tree evaluation paper: https://dl.acm.org/doi/10.1145/3618260.3649664

Charlie Marsh is the founder of Astral, the Python devtool startup that was acquired by OpenAI. I inteviewed him about how software engineering is changing and learnings from starting his own company as an engineer.

• 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/Iw65FD4MGgs
• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835
• Transcript: https://www.developing.dev/p/openai-eng-and-dev-tools-founder

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:40) Origin story
(06:04) The front page of Hacker News
(14:35) Why he chose Rust
(20:10) Full codebase migration from Zig to Rust
(28:40) LLM generated code and open source
(35:34) Performance optimizations
(44:54) Optimization with AI and combating slop
(01:02:08) Learnings as an eng starting a company
(01:17:55) Top technical talk recommendation
(01:18:56) Advice for his younger self
(01:22:00) Outro

Where to find Charlie:

• LinkedIn: https://www.linkedin.com/in/marshcharles/
• GitHub: https://github.com/charliermarsh
• X/Twitter: https://x.com/charliermarsh

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:

• Python tooling could be much, much faster: https://notes.crmarsh.com/python-tooling-could-be-much-much-faster
• The coolest PR he's ever seen: https://github.com/astral-sh/uv/pull/789
• Andrew Kelley’s data-oriented design talk: https://www.youtube.com/watch?v=IroPQ150F6c
• Ruff: https://github.com/astral-sh/ruff
• uv: https://github.com/astral-sh/uv
• ty: https://github.com/astral-sh/ty
• Salsa: https://github.com/salsa-rs/salsa