Formal verification may scale with AI

Brought to You By:

• Statsig — ⁠ The unified platform for flags, analytics, experiments, and more.

• Sonar – The makers of SonarQube, the industry standard for automated code review

• WorkOS – Everything you need to make your app enterprise ready.

—

Martin Kleppmann is a researcher and the author of Designing Data-Intensive Applications, one of the most influential books on modern distributed systems. As of this month, the second, heavily updated edition of the book is out.

In this episode of Pragmatic Engineer, we discuss Martin’s career in tech building startups, how he ended up writing this iconic book, and what he’s focused on now after moving into academia.

We talk about the tradeoffs behind modern infrastructure, how the cloud has changed what it means to scale, and the thinking behind Designing Data-Intensive Applications, including what’s changing in the second edition.

Martin reflects on lessons from building startups like Rapportive, which he sold to LinkedIn, and shares how his experience in both academia and industry shaped his perspective.

We also explore what’s ahead: why formal verification may become more important in an AI-assisted world, the challenges of building local-first software, and his recent research into using cryptography to improve transparency in supply chains without exposing sensitive data.

—

Timestamps

(00:00) Early career

(05:46) Building Rapportive

(10:47) Working at LinkedIn

(14:09) Writing Designing Data-Intensive Applications

(23:00) Reliability, scalability, and repeatability 

(26:24) DDIA: the second edition

(30:50) Tradeoffs of using cloud services 

(39:02) How the cloud changed scaling 

(42:53) The trouble with distributed systems

(49:02) Ethics for software engineers 

(52:45) Formal verification

(1:00:12) Academia vs. industry 

(1:03:50) Local-first software 

(1:09:50) Computer science education

(1:18:32) Martin’s current research and advice

—

The Pragmatic Engineer deepdives relevant for this episode:

• Building Bluesky: a distributed social network

• Inside Uber’s move to the cloud

• The history of servers, the cloud, and what’s next

• The past and future of modern backend practices

• How Kubernetes is built

—

Production and marketing by ⁠⁠⁠⁠⁠⁠⁠⁠https://penname.co/⁠⁠⁠⁠⁠⁠⁠⁠. For inquiries about sponsoring the podcast, email podcast@pragmaticengineer.com.