Formal methods with Hillel Wayne

Stream the latest episode

Listen and watch now on YouTube, Apple and Spotify. See the episode transcript at the top of this page, and timestamps for the episode at the bottom.

Brought to You by

• Antithesis — Turbocharge testing of your systems by running your whole system under aggressive fault injection. There’s good reason teams like Jane Street, Fly.io, and the etcd community rely on Antithesis. Learn more.

• WorkOS – make your app and agents Enterprise Ready, with SSO, SCIM, RBAC, and more. Get started.

• turbopuffer – A vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable. I met their team in San Francisco, and am a fan of their “hardcore and whimsical” engineering culture, and how pragmatic their engineering philosophy is. Check them out.

In this episode

There’s a popular theory that AI will finally make formal verification mainstream because mathematical proof of correctness will be needed when machines write most or all of the code. But will this happen? Today, I’m talking with one of the best people to tackle the prediction. Hillel Wayne is a formal methods consultant, educator, and author (his most recent book being Logic for Programmers), who’s deeply interested in software history.

In this episode of The Pragmatic Engineer podcast, I sit down with Hillel to compare software engineering with traditional engineering, discuss where formal methods fit into modern software development, and we explore why they are essential for some of the world’s most complex systems. We cover the formal specification language, TLA+, walk through several formal verification tools, examine why distributed systems are so difficult to reason about, and look into whether AI will make formal methods accessible to more engineering teams.

Takeaways from the conversation with Hillel

1. Are we “real” engineers? After thorough research, Hillel has an answer. For The Crossover Project, Hillel interviewed ~20 people in different fields of…