Formal methods with Hillel Wayne

**Gergely Orosz** (0:00)
There's a popular theory going around that AI will finally make formal verification go mainstream because when machines write the code, humans will need mathematical proof that is correct. Today, I'm talking with one of the best people to respond to this, Hillel Wayne, a formal methods consultant. He's taught TLA+, a popular formal specifications language across the industry, wrote the book Logic for Programmers, and will soon be joining Antisys. In today's conversation, we discuss The Crossover Project. Hillel's research interviewing 15 plus traditional engineers answered the question, can software engineers also be considered real engineers? How Aws use TLA+, an overview of how Amazon found a rare bug inside of DynamoDB using this formal specifications language. A deep dive into property-based testing and why this is the middle ground that most engineers should probably adopt, and many more. If you want to understand more about formal verification and get a sense of whether this approach could go mainstream with AI, this episode is for you. In today's episode, we'll get to the question, does it make sense to use formal methods to verify AI-written code? As a spoiler, the answer will be proper formal methods are an overkill for this. But lightweight formal methods can actually be helpful.
This is where I need to mention our presenting sponsor, Antisys.
Antisys verifies your system's correctness by running your whole system in hostile simulation and finding bugs. It does this by using an approach called deterministic simulation testing or DST, which 80 of his distinguished engineer Mark Brooker and Ankur Desai have described as lightweight formal methods.
Setting aside Antisys for a minute. If you, as an engineer, want to get more serious in verifying that your system works as intended, your best bet would be to use lightweight formal methods. Now back to Antisys. Antisys is turbochargers testing by running your whole system under agressive fault injection. Imagine Antisys as hundreds or thousands of versions of the Mario game running, each instance aggressively trying to break the game, with increasingly weird input combinations. With Antisys, you can specify properties at the whole system level, and Antisys will actively try to disprove them. So you can be confident that if your system holds up in Antisys, it will hold up in production. There's good reason teams like Jane Street, fly.io and the etcd community rely on Antisys. Head to antisys.com/pragmatic to learn more.
So Hillel, welcome to the podcast.

**Hillel Wayne** (2:15)
Thank you so much. I'm really excited to be here.

**Gergely Orosz** (2:17)
It's so nice to have you here. I was curious, you're very well known for formal methods, for programming, for logic, for all of these topics, but how did you get into tech?

**Hillel Wayne** (2:27)
So to start, I never really saw myself as a technical person. I liked computers growing up and I did a tiny bit of programming. My father was a programmer, he taught me visual basic. But I always wanted to do physics and math. That was like my dream. I put in my college application, I want to listen to the heartbeat of the universe.
Don't ever take advice from like a high schooler for writing, that's just saying. But after about three years of doing this in college, I realized that I kind of liked the idea of physics, but I didn't enjoy doing it and I couldn't see myself doing it for 50 years. What part I did enjoy though was the programming in the labs. That was the most fun part to me.
So I thought, well, if this is what I enjoy, I want to try to do it full time. So after college, I left for San Francisco and became a developer, a Ruby on Rails developer in education technology. After some time, I went back to Chicago and then in the course of the next job I was working also in education technology, I fell into my current niche, which is formal verification and formal methods.

**Gergely Orosz** (3:21)
The first time I came across your writing, because you write a blog, a pretty regular one, and I really enjoy your writing, the first time was with The Crossover Project. This was a project where you attempted to answer, are we as software engineers actually engineers?

**Hillel Wayne** (3:38)
Yes.

**Gergely Orosz** (3:38)
Can we talk about this project?

**Hillel Wayne** (3:40)
Absolutely.
So I guess I should probably start with the motivation, which was, I've read a lot of books on software, and I've read a lot of online articles about software. And one of the favorite things that software developers do is argue about whether it should be engineering or not, right?
And there's the camp of people that say, well, we don't deserve to call ourselves engineers, we should not. They are so far above us, we shouldn't even consider ourselves in the same space. And then there are the people who are like, what we do is so special and so unique, engineering doesn't have anything on us, they can't hold a candle to what we do. You see books like Software Craftsmanship, which talk about how like, oh, engineering is this really boring, slow field, and software is this incredibly creative, special, wonderful thing. I was very firmly in camp one. I thought we were not engineers, we didn't deserve to call ourselves engineering, anything like that. What I do for work is really carefully analyzing software systems, and I thought, ah, this is real engineering, and everything else is not engineering. Then I found this talk by Glenn Vanderbird, where what he did was he read a bunch of engineering books and compared them to what we do in software, and he said, actually, this looks really similar to what we do in software. And I thought, that can't be right. I need something more rigorous. I'm going to have to talk to people who did both engineering and software development and see what they say, and they all agreed with him. So I was wrong. We're engineers.