Latest / The Pragmatic Engineer / Formal methods with Hillel Wayne

Transcript

Formal methods with Hillel Wayne · The Pragmatic Engineer

0:00
SPEAKER_00: There's a popular theory going around
0:01
SPEAKER_00: that AI will finally make formal verification go mainstream because
0:05
SPEAKER_00: when machines write the code, humans will need mathematical proof that is correct.
0:09
SPEAKER_00: Today, I'm talking with one of the best people to respond to this,
0:12
SPEAKER_00: Hillel Wayne, a formal methods consultant.
0:15
SPEAKER_00: He's taught TLA+,
0:16
SPEAKER_00: a popular formal specification language across the industry,
0:19
SPEAKER_00: wrote the book Logic for Programmers, and will soon be joining Antisys.
0:23
SPEAKER_00: In today's conversation,
0:24
SPEAKER_00: we discuss The Crossover Project,
0:26
SPEAKER_00: Hilo's research interviewing 15-plus traditional engineers to answer the question.
0:30
SPEAKER_00: If you want to understand more about formal verification and get a sense of
0:33
SPEAKER_00: whether this approach could go mainstream with AI, this episode is for you.
0:55
SPEAKER_00: In today's episode,
0:56
SPEAKER_00: we'll get to the question,
0:58
SPEAKER_00: does it make sense to use formal methods to verify AI written code?
1:01
SPEAKER_00: As a spoiler,
1:02
SPEAKER_00: the answer will be proper formal methods are an overkill for this,
1:06
SPEAKER_00: but lightweight formal methods can actually be helpful.
1:09
SPEAKER_00: This is where I need to mention our presenting sponsor, Antizizis.
1:12
SPEAKER_00: Antisysys verifies your system of correctness by running your whole system
1:16
SPEAKER_00: in hostile simulation and finding bugs.
1:18
SPEAKER_00: It does this by using an approach called deterministic simulation testing, or DST,
1:23
SPEAKER_00: which ADW's distinguished engineer Mark Brooker and Ankur Desai have described
1:26
SPEAKER_00: as lightweight formal methods.
1:29
SPEAKER_00: Setting aside Entisysys for a minute.
1:31
SPEAKER_00: If you as an engineer want to get more serious in verifying that your system works
1:34
SPEAKER_00: as intended, your best bet would be to use lightweight formal methods.
1:38
SPEAKER_00: Now back to Entisysys.
1:40
SPEAKER_00: Entisysys turbocharges testing by running your whole system
1:43
SPEAKER_00: under aggressive Imagine Antithesis as hundreds or thousands of versions of
1:47
SPEAKER_00: the Mario game running,
1:49
SPEAKER_00: each instance aggressively trying to break the game
1:51
SPEAKER_00: with increasingly weird input combinations.
1:54
SPEAKER_00: With Antithesis,
1:55
SPEAKER_00: you can specify properties at the whole system level,
1:57
SPEAKER_00: and Antithesis will actively try to disprove them,
2:00
SPEAKER_00: so you can be confident that if your system holds up in Antithesis,
2:03
SPEAKER_00: it will hold up in production.
2:05
SPEAKER_00: There's good reason teams like Janestreet, Fly.io, and the etcd community rely on Antithesis.
2:10
SPEAKER_00: Head to antithesis.com slash pragmatic to learn more.
2:13
SPEAKER_00: So hello, welcome to the podcast.
2:15
SPEAKER_00: Thank you so much.
2:16
SPEAKER_00: I'm really excited to be here.
2:17
SPEAKER_00: It's so nice to have you here.
2:19
SPEAKER_00: I was curious,
2:20
SPEAKER_00: you're very well known for formal methods,
2:22
SPEAKER_00: for programming, for logic, for all of these topics, but how did you get into tech?
2:27
SPEAKER_01: So to start, I never really saw myself as a technical person.
2:32
SPEAKER_01: I liked computers growing up and I did a tiny bit of programming.
2:35
SPEAKER_01: My father was a programmer.
2:36
SPEAKER_01: He taught me Visual Basic.
2:37
SPEAKER_01: But I always wanted to do physics and math.
2:39
SPEAKER_01: That was like my dream.
2:40
SPEAKER_01: I put in my college application, I want to listen to the heartbeat of the universe.
2:44
SPEAKER_01: Don't ever take advice from like a high schooler for writing, just saying.
2:49
SPEAKER_01: But after about three years of doing this in college,
2:51
SPEAKER_01: I realized that I kind of liked the idea of physics, but I didn't enjoy doing it.
2:55
SPEAKER_01: And I couldn't see myself doing it for 50 years.
2:57
SPEAKER_01: What part I did enjoy, though, was the programming in the labs.
3:00
SPEAKER_01: That was the most fun part to me.
3:02
SPEAKER_01: So I thought, well, if this is what I enjoy, want to try to do it full time.
3:06
SPEAKER_01: So after college,
3:07
SPEAKER_01: I left for San Francisco and became a developer,
3:10
SPEAKER_01: a Ruby on Rails developer in education technology.
3:12
SPEAKER_01: After some time, I moved back to Chicago.
3:14
SPEAKER_01: And then in the course of the next job I was working in,
3:17
SPEAKER_01: also in education technology,
3:18
SPEAKER_01: I fell into my current niche, which is formal verification and formal methods.
3:21
SPEAKER_00: The first time I came across your writing because you write a blog,
3:25
SPEAKER_00: a pretty regular one, and I really enjoy your writing.
3:28
SPEAKER_00: The first time was with the crossover project.
3:31
SPEAKER_01: This was a project where you attempted to answer,
3:33
SPEAKER_00: are we as software engineers actually engineers?
3:38
SPEAKER_01: Yes.
3:38
SPEAKER_00: Can we talk about this project?
3:40
SPEAKER_01: Absolutely.
3:41
SPEAKER_01: So I guess I should probably start with the motivation,
3:44
SPEAKER_01: which was,
3:45
SPEAKER_00: I've read a lot of books on software and I've read a lot of online articles
3:49
SPEAKER_00: about software.
3:50
SPEAKER_01: And one of the favorite things that software developers do is argue about
3:53
SPEAKER_01: whether it should be engineering or not, right?
3:56
SPEAKER_01: And there's the cap of people that say, well...
3:59
SPEAKER_01: We don't deserve to call ourselves engineers.
4:01
SPEAKER_01: We should not.
4:02
SPEAKER_01: They are so far above us.
4:03
SPEAKER_01: We shouldn't even like consider ourselves in the same space.
4:05
SPEAKER_01: And then there are the people who are like, what we do is so special and so unique.
4:11
SPEAKER_01: Engineering doesn't have anything on us.
4:12
SPEAKER_01: They can't hold a candle to what we do.
4:14
SPEAKER_01: You see books like Software Craftsmanship,
4:16
SPEAKER_01: which talk about how like, oh,
4:17
SPEAKER_01: engineering is this really boring,
4:19
SPEAKER_01: slow field and software is this incredibly creative, special, wonderful thing.
4:23
SPEAKER_01: I was very firmly in camp one.
4:25
SPEAKER_00: I thought we were not engineers.
4:26
SPEAKER_00: We didn't deserve to call ourselves engineering, anything like that.
4:29
SPEAKER_01: What I do for work is really carefully analyzing software systems.
4:32
SPEAKER_01: And I thought, ah, this is real engineering and everything else is not engineering.
4:35
SPEAKER_01: Then I found this talk by Glenn Vanderberg,
4:37
SPEAKER_01: where what he did was he read a bunch of engineering books and compared them
4:40
SPEAKER_01: to what we do in software.
4:42
SPEAKER_01: And he said, actually, this looks really similar to what we do in software.
4:45
SPEAKER_01: And I thought, that can't be right.
4:47
SPEAKER_01: I need something more rigorous.
4:49
SPEAKER_01: I'm going to have to talk to people who did both engineering
4:52
SPEAKER_01: and software development and see what they say.
4:54
SPEAKER_01: And they all agreed with him.
4:56
SPEAKER_01: So I was wrong.
4:56
SPEAKER_01: We're engineers.
4:58
SPEAKER_01: Can we go a little bit into it?
4:59
SPEAKER_00: So as I started talking to the first people,
5:03
SPEAKER_00: I realized that this was a much deeper project than I ever expected.
5:06
SPEAKER_01: And I decided I needed to have as comprehensive a look at traditional engineering
5:10
SPEAKER_01: as I could possibly get.
5:11
SPEAKER_00: There are many kinds of engineering.
5:13
SPEAKER_01: There's not just building bridges, but there's designing circuits.
5:16
SPEAKER_01: There's figuring out chemical processes.
5:18
SPEAKER_01: There's industrial engineering,
5:20
SPEAKER_01: which is figuring out the layouts of factories and how we organize kinds of labor.
5:25
SPEAKER_01: There's just so many different kinds.
5:26
SPEAKER_01: And I wanted to see every single kind's view into what engineering looked like.
5:31
SPEAKER_01: To compare them all to software,
5:32
SPEAKER_01: which when you think about it,
5:34
SPEAKER_01: when we say like, oh, software isn't like building a bridge, maybe it isn't.
5:36
SPEAKER_01: But is it like designing a circuit?
5:38
SPEAKER_01: Is it like figuring out a chemical flow?
5:40
SPEAKER_01: Maybe those are much more closer to the kinds of engineering we do.
5:42
SPEAKER_01: I needed to know.
5:44
SPEAKER_01: I think in the end,
5:45
SPEAKER_01: I talked to about 15 or 20 people in total across about six
5:48
SPEAKER_01: or seven different fields.
5:50
SPEAKER_00: And what were the similarities that you found that software engineering has
5:54
SPEAKER_00: with either specific types of engineering or across the board?
5:58
SPEAKER_01: If I had to summarize what I found in general, I'd put it like this.
6:03
SPEAKER_02: Everybody hates waterfall.
6:07
SPEAKER_01: No way.
6:07
SPEAKER_01: The core tension of engineering is between how expensive it is to make a mistake
6:13
SPEAKER_01: and how quickly you can iterate.
6:15
SPEAKER_01: The faster you can iterate, the less planning you need to do before you iterate.
6:19
SPEAKER_01: And the more expensive it is, the more planning you need to do.
6:22
SPEAKER_01: That's why,
6:23
SPEAKER_01: for example,
6:23
SPEAKER_01: when you're building a building where you can't build it multiple times
6:27
SPEAKER_01: and see what happens, you have to do a lot of planning up front.
6:30
SPEAKER_01: But even then, you are looking for ways to iterate on the plan.
6:34
SPEAKER_01: You do things like build scale models,
6:35
SPEAKER_01: you use software to simulate the building, you do CAD models, etc.
6:40
SPEAKER_01: And in other fields,
6:41
SPEAKER_01: like in,
6:41
SPEAKER_01: for example,
6:42
SPEAKER_01: electrical engineering,
6:43
SPEAKER_01: you have the ability to come up with a design,
6:44
SPEAKER_01: test it, and then throw it to the fab and get something back.
6:47
SPEAKER_01: So they will iterate a lot more than civil engineering does.
6:50
SPEAKER_00: Ah, interesting enough.
6:51
SPEAKER_00: I heard the term smoke test originated from electrical
6:54
SPEAKER_01: engineering, actually.
6:56
SPEAKER_01: I did not look into that, but I could believe it.
6:58
SPEAKER_00: Yeah, apparently it's when you have a test circuit and you just hook it up.
7:01
SPEAKER_00: And if it does, if it smokes, it's already bad.
7:04
SPEAKER_00: That is very interesting.
7:05
SPEAKER_00: So even within engineering,
7:07
SPEAKER_00: when we say traditional engineering,
7:08
SPEAKER_00: there's just layers of engineering or differences, right?
7:11
SPEAKER_01: Layers of iteration, I'd say.
7:13
SPEAKER_01: One of the first people I talked to was actually a mining engineer.
7:15
SPEAKER_01: He designed mines and Okay, so I guess we all hate waterfalls.
7:42
SPEAKER_00: Or the idea of waterfall.
7:43
SPEAKER_01: Yeah.
7:44
SPEAKER_00: What are some of the interesting differences that you came across?
7:46
SPEAKER_00: Either where engineering is ahead of us or traditional engineering does have things
7:51
SPEAKER_00: on us,
7:51
SPEAKER_00: which you were hoping to find,
7:53
SPEAKER_00: or places where actually software engineering is ahead in some ways.
7:56
SPEAKER_01: There's both differences in how we practice it,
7:58
SPEAKER_01: but also differences in the shape of our material.
8:02
SPEAKER_01: Because every engineering concerns a different material, they have different constraints.
8:06
SPEAKER_00: While it's true that everybody tries to iterate as fast as they can,
8:09
SPEAKER_01: often turning to software to do that, software is the best at it.
8:12
SPEAKER_01: The best comparison is chemical engineering,
8:14
SPEAKER_01: where I talk to people saying that they would set up their experiment,
8:17
SPEAKER_01: run it overnight, and get the results the next day.
8:19
SPEAKER_01: And that was fast.
8:20
SPEAKER_01: With us, we can basically press F11 and get the result, right?
8:24
SPEAKER_01: And that allows us to basically iterate much faster than even those fields can.
8:29
SPEAKER_01: I think we all kind of know this.
8:31
SPEAKER_01: One thing that we might not realize as software engineers is that our work is
8:34
SPEAKER_01: a lot more consistent than other fields.
8:36
SPEAKER_01: The example I always do sometimes because I've given a talk
8:38
SPEAKER_01: about this is I would pull out like a CPU chip or like a stick of RAM
8:43
SPEAKER_01: and I'd say like, hey, here's the spec sheet.
8:45
SPEAKER_01: And if I look at the spec sheet,
8:47
SPEAKER_01: it says this resistor has a resistance that is within 20% of 100 ohms as long
8:53
SPEAKER_01: as you keep it between 20 and 50 degrees centigrade.
8:56
SPEAKER_01: So they're basically saying that if they make a thousand of these,
8:58
SPEAKER_01: there's going to be a variance of 20% across all 1000.
9:01
SPEAKER_01: And the only way to know is to test them.
9:03
SPEAKER_01: And then if you run it for too long or you heat it up too much, it's going to change again.
9:09
SPEAKER_01: With software,
9:10
SPEAKER_01: assuming no like CPU bugs or anything like that,
9:12
SPEAKER_01: the same program, if it runs on this computer or on your computer, exact same.
9:17
SPEAKER_01: Sort this list the exact same with the sorting algorithm.
9:19
SPEAKER_00: Does this also mean that we might not account for variability as much
9:24
SPEAKER_00: as other engineering disciplines do?
9:26
SPEAKER_01: I'd say so.
9:27
SPEAKER_01: The variation we have to deal with is kind of And how did you see the similarities
9:31
SPEAKER_01: or differences of
9:55
SPEAKER_00: Software engineers,
9:56
SPEAKER_00: for example, often interact with customers, with end users who use the software.
10:00
SPEAKER_00: In other engineering fields,
10:01
SPEAKER_00: is this also a thing where as an engineer,
10:03
SPEAKER_00: you will talk or know your customer or just...
10:07
SPEAKER_00: Not knowing them at all.
10:09
SPEAKER_01: I think it depends because different engines I talked to had different experiences.
10:14
SPEAKER_01: Some said that they felt that with software, they felt much closer to the customer.
10:18
SPEAKER_01: With other ones, they said they felt much further.
10:20
SPEAKER_01: So I think it's hard to really tell there.
10:22
SPEAKER_00: One thing I remember vividly is a difference that you pointed out,
10:25
SPEAKER_00: which was very different and almost makes software engineering a bit higher status
10:30
SPEAKER_00: or better place is open source.
10:32
SPEAKER_00: The concept of open source.
10:34
SPEAKER_01: Yes.
10:34
SPEAKER_01: So...
10:35
SPEAKER_01: That is one thing that seems very special about software versus any other field.
10:41
SPEAKER_01: Like the reason I'm here in Hungary right now with you is because I'm going
10:45
SPEAKER_01: to be speaking at craft conference, right?
10:48
SPEAKER_01: Most other fields of engineering,
10:51
SPEAKER_01: or in fact,
10:51
SPEAKER_01: any other field of like human labor has two kinds of conferences,
10:56
SPEAKER_01: academic conferences where they talk about research and trade shows where they try
10:59
SPEAKER_01: to sell, where vendors try to sell to like companies.
11:02
SPEAKER_01: Software is kind of unique in having the third kind of the practitioner conference
11:06
SPEAKER_01: where we are just meeting to get better at what we do.
11:09
SPEAKER_01: We also are really the only kind to really focus heavily on like open source
11:13
SPEAKER_01: and making our knowledge freely available.
11:15
SPEAKER_01: For any language, you can probably find out how to learn language online, right?
11:17
SPEAKER_01: You don't have to buy a book.
11:18
SPEAKER_01: You don't have to like talk to the vendor to learn it.
11:21
SPEAKER_01: That's something really special about software.
11:22
SPEAKER_00: I wonder why this might be both the fact that we do share a lot of the information
11:28
SPEAKER_00: or the craft or how we build things.
11:30
SPEAKER_00: Even some of the largest companies, I think, are like an Uber or Airbnb.
11:34
SPEAKER_00: These are $100 billion companies.
11:36
SPEAKER_00: They will not particularly hide how they built that piece of software Uber publishes
11:42
SPEAKER_00: and does talks about their app that is used by all these people,
11:45
SPEAKER_00: how exactly they built it or approximately.
11:48
SPEAKER_00: I wonder why this...
11:52
SPEAKER_00: I'm going to switch to
12:01
SPEAKER_01: speculation for a second.
12:02
SPEAKER_01: This isn't something that I could really speak on with full authority,
12:05
SPEAKER_01: but my guess is that part of it is cultural.
12:09
SPEAKER_01: But another part of it is that the material we work with is the same as our product, right?
12:16
SPEAKER_01: We are using software to write software versus using tools and lathes
12:20
SPEAKER_01: to build things or using software to design circuits.
12:24
SPEAKER_01: And I personally think that that similarity,
12:27
SPEAKER_01: basically,
12:27
SPEAKER_01: that we are using the same materials on both ends is what makes it so much easier
12:31
SPEAKER_01: for us to talk about things like open source.
12:34
SPEAKER_00: Interesting how I like this thinking of materials used in each engineering
12:39
SPEAKER_00: and how our material is software.
12:42
SPEAKER_00: Of course, the hardware engineering, and we know that's a bit different, of course.
12:45
SPEAKER_00: But already there's a divide between hardware engineering and software engineers
12:48
SPEAKER_00: on how much they share, how much we know about them, and so on.
12:52
SPEAKER_01: I kind of wonder,
12:54
SPEAKER_01: I've got some friends who do like 3D printing,
12:55
SPEAKER_01: and it seems like,
12:56
SPEAKER_01: and I haven't looked into this,
12:57
SPEAKER_01: but it seems like they also have like a very open space
12:59
SPEAKER_01: of like sharing things freely.
13:01
SPEAKER_01: And I wonder if that's the same because it is so easy to share and because like
13:05
SPEAKER_01: the unit of value is the schematic there, if that kind of leads to the same thing.
13:09
SPEAKER_00: I also wonder if hacker culture might play a thing in places where it's easy enough
13:13
SPEAKER_00: to afford to get started on a thing,
13:16
SPEAKER_00: for example,
13:17
SPEAKER_00: ham radios,
13:18
SPEAKER_00: which is not entering,
13:19
SPEAKER_00: but there's a thriving community where they share the setup,
13:22
SPEAKER_00: the things, they talk with each other.
13:25
SPEAKER_00: Small electronics might be,
13:27
SPEAKER_00: but ultimately software started in the 70s when it was affordable
13:31
SPEAKER_00: and anyone could buy a computer, maybe the internet.
13:34
SPEAKER_00: I'm also just speculating.
13:35
SPEAKER_01: Yeah, definitely something worth doing a follow-up project on, right?
13:39
SPEAKER_00: Well, you've already spent a bunch of time on it.
13:41
SPEAKER_01: Don't give me so many rabbit holes.
13:42
SPEAKER_01: There's already too many rabbit holes in my life.
13:45
SPEAKER_00: One more thing that you brought up is version control and the fact that in software,
13:51
SPEAKER_00: we just take it for granted.
13:52
SPEAKER_00: We have version control everywhere.
13:53
SPEAKER_00: And you said that this is super unique across most of engineering.
13:57
SPEAKER_01: Yeah, I interviewed like 20 people on this.
13:59
SPEAKER_01: I think all 20 mentioned version control as the thing they wish they had in their old field.
14:03
SPEAKER_01: Wow.
14:03
SPEAKER_01: Yeah.
14:04
SPEAKER_01: Now, to be clear, they do have things like change management in like other fields.
14:07
SPEAKER_01: But I think version control as we have it,
14:10
SPEAKER_01: is so much more sophisticated than anything they have.
14:12
SPEAKER_01: It's like comparing like a modern car to a Model T.
14:15
SPEAKER_00: What do you think there are things that now having talked with so many people
14:20
SPEAKER_00: and learned about the different engineering cultures,
14:23
SPEAKER_00: like actual traditional engineering cultures, what could we learn from them?
14:27
SPEAKER_00: What are some kind of inspiration that might be useful here or there?
14:30
SPEAKER_01: Yeah, this is a harder question because while everybody I talked
14:32
SPEAKER_01: to mentioned those two things of openness and version control,
14:36
SPEAKER_01: I got a much more scattering set of answers when
14:39
SPEAKER_00: talking to people
14:39
SPEAKER_00: about what we could learn from their old fields.
14:42
SPEAKER_01: The two things I kind of gleaned out is that one,
14:44
SPEAKER_01: while we are a lot better at iterating than other fields,
14:48
SPEAKER_01: we're worse at the planning part.
14:49
SPEAKER_01: Like we still need to do some kind of planning before we iterate.
14:52
SPEAKER_01: And we just aren't as good as those other fields,
14:55
SPEAKER_01: in part because we can get away with not doing it as much.
14:58
SPEAKER_01: But we could get some sort of fusion of the two and get even better
15:00
SPEAKER_01: than we currently are, which, hey, plug for what I do.
15:03
SPEAKER_01: The other thing that I think is more interesting in terms of being
15:06
SPEAKER_01: a bit more shocking to me is that while we're better at being open about all
15:10
SPEAKER_01: of our materials,
15:12
SPEAKER_01: We seem to be worse at compiling information about the specifics of our job.
15:19
SPEAKER_01: And that's a bit loosey-goosey,
15:21
SPEAKER_01: but the example I keep coming back to is that one of the engineers that I talked
15:24
SPEAKER_01: to had two favorite books,
15:26
SPEAKER_01: The Design of Everyday Things,
15:27
SPEAKER_01: which he recommends every engineer read, and the Snapfit Handbook.
15:31
SPEAKER_01: Are you familiar with Snapfits?
15:32
No.
15:33
SPEAKER_01: Looking around here to see if there's like one, if I can just show it.
15:35
SPEAKER_01: But like,
15:36
SPEAKER_01: you know,
15:36
SPEAKER_01: like how remotes,
15:37
SPEAKER_01: they have that little clicky thing in the back that you use that hold the battery
15:39
SPEAKER_01: in?
15:39
SPEAKER_02: Yeah.
15:40
SPEAKER_01: That's a Snapfit.
15:41
SPEAKER_01: It is a physical device that basically clicks into another device to keep them fused.
15:46
SPEAKER_01: And this was a 500-page book all about Snapfits,
15:49
SPEAKER_01: their engineering, appropriate shapes, materials, etc.
15:52
SPEAKER_01: And that kind of compiling of information about
15:55
SPEAKER_01: the materials is something other fields do that we don't do.
15:58
SPEAKER_01: An analogy that I would think of in software would be something like a 500-page book
16:02
SPEAKER_01: on how to version an API.
16:03
SPEAKER_00: We could all use that.
16:04
SPEAKER_00: Yes, we could.
16:06
SPEAKER_00: And we don't have it.
16:07
SPEAKER_00: We can learn it from engineering.
16:08
SPEAKER_00: We should have that.
16:09
SPEAKER_00: You started this project asking, are we really engineers?
16:11
SPEAKER_00: And your personal inclination, which you didn't say at the time, was that we're probably not.
16:15
SPEAKER_00: In the closing of this series, you said you're still a bit unsure of how to answer it.
16:19
SPEAKER_00: This was five years ago.
16:21
SPEAKER_00: This many years later, what is your inclination?
16:23
SPEAKER_00: Are we actually engineers?
16:25
SPEAKER_01: I think so.
16:25
SPEAKER_01: I think this project and writing about it and thinking about it has firmly moved
16:29
SPEAKER_01: from the camp of we are definitely not to we probably are.
16:33
SPEAKER_01: I do want to caveat that I wrote this before LLMs were a thing,
16:37
SPEAKER_01: and this has probably changed our field as we know it,
16:39
SPEAKER_01: and it's probably also changed those other branches, and I don't know how.
16:42
SPEAKER_01: So that could have changed the calculus between two spaces.
16:45
SPEAKER_01: But as of now,
16:47
SPEAKER_01: I think excluding LLMs and how they're changing things,
16:50
SPEAKER_01: what we do now is very similar to what those people in those other fields did,
16:54
SPEAKER_01: according to my interviews.
16:56
SPEAKER_00: It's such a cool project and it's still a very good read.
16:59
SPEAKER_00: I'll also link it in the show notes below.
17:01
SPEAKER_00: I do recommend going into it.
17:03
SPEAKER_00: So let's talk about formal methods.
17:05
SPEAKER_00: How did you get exposed to them?
17:07
SPEAKER_00: And for those of us who are not deep into it, What are they?
17:12
SPEAKER_01: I'm going to give you a function in max, right?
17:14
SPEAKER_01: Which should, given a list, return the largest number.
17:16
SPEAKER_01: What would be a test you'd write for that?
17:18
SPEAKER_00: I'd write a test that I do a list of like two items.
17:20
SPEAKER_00: It returns the largest one that I know.
17:22
SPEAKER_00: I give a very long list.
17:24
SPEAKER_00: I try to stress test it.
17:26
SPEAKER_00: I give a list where I give like similar numbers.
17:28
SPEAKER_00: I try to come up with some edge cases.
17:31
SPEAKER_00: I'll probably write like five tests.
17:34
SPEAKER_00: Try to think about integer overflows, potentially try some tricky one.
17:38
SPEAKER_00: Maybe I'll take it to maybe eight if I'm feeling super ambitious and then I'm done.
17:42
SPEAKER_01: Okay.
17:43
SPEAKER_01: So we take one of those tests.
17:44
SPEAKER_01: How do you know what the right answer is supposed to be?
17:46
SPEAKER_00: I just know because I have a, I learned math.
17:50
SPEAKER_00: So in school, I know which number is bigger.
17:54
SPEAKER_00: Honestly, I look at it.
17:55
SPEAKER_00: I have this,
17:56
SPEAKER_00: I guess,
17:57
SPEAKER_00: ingrained knowledge and it feels very basic knowledge that I don't even have
18:01
SPEAKER_00: to explain.
18:02
SPEAKER_01: Right.
18:02
SPEAKER_01: You have some ingrained knowledge that you don't have to explain,
18:04
SPEAKER_01: such that you can look at, say, the max of two and three and know it's three, right?
18:11
SPEAKER_01: That's interesting.
18:12
SPEAKER_01: There's some sort of implicit mechanism in your brain that can see that
18:15
SPEAKER_01: and know what the function is supposed to do.
18:16
SPEAKER_01: Step one of what I do with formal methods is asking,
18:19
SPEAKER_01: can we take that implicit knowledge and make it explicit?
18:22
SPEAKER_01: Can we figure out what a function is supposed to actually be doing and write
18:25
SPEAKER_01: that down in a way that can be shown to anybody?
18:28
SPEAKER_01: So I would basically,
18:29
SPEAKER_01: in this process,
18:30
SPEAKER_01: say like the max of a list is an element that is in the list such
18:35
SPEAKER_01: that every other element is smaller than that element.
18:38
SPEAKER_01: That is a way that we can formally say what the maximum of a list is.
18:42
SPEAKER_01: So that's part one,
18:43
SPEAKER_01: just learning how to look at functions and say, okay, I know what this is doing.
18:46
SPEAKER_01: How would I explain what this is doing in a way that is clear and unambiguous?
18:51
SPEAKER_01: Then step two is asking,
18:53
SPEAKER_01: every single test you've written is basically some Facet of it is an element
18:58
SPEAKER_01: the list and it is the number of that list such that every other number
19:02
SPEAKER_01: the list is smaller than it.
19:03
SPEAKER_01: Now that we have that,
19:04
SPEAKER_01: what's the best way to show that our function actually satisfies that specification?
19:10
SPEAKER_01: Tests are one way.
19:11
SPEAKER_01: Those are basically taking individual values and showing how those comport in specification.
19:15
SPEAKER_01: Types are another way.
19:17
SPEAKER_01: We could basically say, OK,
19:18
SPEAKER_01: in every single case,
19:19
SPEAKER_01: we are putting in a list of elements and we're getting out a single element.
19:22
SPEAKER_01: So we have to make sure that every time we call it, that's what's true.
19:24
SPEAKER_01: So basically,
19:25
SPEAKER_01: coming up with the properties of the thing,
19:27
SPEAKER_01: like what it actually is, is the specification of it.
19:30
SPEAKER_01: And then showing the function matches that specification is the verification.
19:34
SPEAKER_01: And what phone methods ask is,
19:35
SPEAKER_01: can we use mathematics to show that it works not just for the cases that you asked
19:38
SPEAKER_01: for, but every single possible list you pass in?
19:42
SPEAKER_01: And that is done through proof.
19:44
SPEAKER_01: Coming up with some sort of mathematical argument that this code matches this spec.
19:49
SPEAKER_00: And then in proof...
19:50
SPEAKER_00: Again, from university,
19:51
SPEAKER_00: I still remember the maths proofs where we would proof an equation,
19:56
SPEAKER_00: you do rigid Transformations, you know what you're allowed to do.
20:01
SPEAKER_00: Sometimes you can bring in tricks, but those tricks are also inside of your rigid list.
20:06
SPEAKER_00: And every time,
20:07
SPEAKER_00: you know, you typically start from a complicated equation and you keep changing it.
20:11
SPEAKER_00: And in the end, you shape it in a way that it's now trivial or you transform.
20:16
SPEAKER_00: Those are one of the tools we do.
20:17
SPEAKER_00: Is this what formal methods also does to some extent?
20:20
SPEAKER_01: Yes, but you know how to basically add two tangent numbers by hand, right?
20:24
SPEAKER_01: Do you do that by hand or do you just use a calculator?
20:27
SPEAKER_00: I now use a calculator.
20:28
SPEAKER_00: If it's easy enough, I use my brain as a calculator.
20:30
SPEAKER_00: Otherwise, I just punch it into the calculator.
20:32
SPEAKER_01: Yeah.
20:32
SPEAKER_01: So similarly,
20:33
SPEAKER_01: a lot of problem methods,
20:34
SPEAKER_01: that math of transformation,
20:36
SPEAKER_01: while you can do it by hand with like what's called a theorem prover,
20:40
SPEAKER_01: often in industry that is being done for the most part with tools
20:44
SPEAKER_01: that basically automate huge parts of this process.
20:46
SPEAKER_01: So you don't have to do every single transformation yourself.
20:49
SPEAKER_01: You can, for example, say, OK, we have these things are true at the beginning.
20:53
SPEAKER_01: I want this to be true at the end.
20:55
SPEAKER_01: And can you figure this out?
20:56
SPEAKER_01: And it'll be like,
20:57
SPEAKER_01: either yes, I can prove these things match, or no, I need a little bit more help.
21:00
SPEAKER_01: And then you say like, okay, at this point, I'm going to also let you know that this is true.
21:04
SPEAKER_00: And it's like, okay, I can verify that's true.
21:06
SPEAKER_01: And it helps me get to the end.
21:07
SPEAKER_01: And you just keep doing that until you actually have enough that the computer
21:10
SPEAKER_00: can do
21:10
SPEAKER_00: the proof for you.
21:11
SPEAKER_00: Yeah.
21:12
SPEAKER_00: So with form and methods, this, I mean, this sounds all logical.
21:14
SPEAKER_00: I think it's easy to follow.
21:17
SPEAKER_00: In practice,
21:17
SPEAKER_00: what techniques,
21:19
SPEAKER_00: technologies,
21:20
SPEAKER_00: tools do What does the industry use,
21:22
SPEAKER_00: the tech industry use to actually prove that, you know, some stuff works?
21:27
SPEAKER_01: To get to that, we need to ask another question.
21:30
SPEAKER_01: Why isn't this being done for everything?
21:31
SPEAKER_00: Okay, let me ask that question.
21:33
SPEAKER_00: That's a good question.
21:34
SPEAKER_00: Yeah, this all sounds sensible.
21:36
SPEAKER_00: It will be nice to not have to write out those five or eight tests.
21:39
SPEAKER_00: And I know that those tests might not cover all edge cases.
21:42
SPEAKER_00: Been there, done that, where you miss.
21:44
SPEAKER_00: And I didn't think that I didn't do a formal proof.
21:47
SPEAKER_00: I thought like, well, I missed a test case.
21:49
SPEAKER_00: That's on me.
21:49
SPEAKER_00: Sorry.
21:50
SPEAKER_00: Let me put in that test case.
21:51
SPEAKER_00: I now have nine tests.
21:52
SPEAKER_00: And now I go and think I did a great job.
21:55
SPEAKER_00: Why are we not doing formal testing for everything?
21:57
SPEAKER_01: Instead of finding the largest number in a list,
21:59
SPEAKER_01: why don't we try to find the file in a directory that has the most lines in it?
22:05
SPEAKER_00: Well, now I'm thinking of writing a program that in kind of an imperative style,
22:09
SPEAKER_00: it goes to a four list each file.
22:11
SPEAKER_00: I list how long the lines are.
22:13
SPEAKER_00: I count the lines.
22:15
SPEAKER_00: I cannot tell it easily.
22:16
SPEAKER_01: Okay, are we talking about ASCII lines or UTF at new lines?
22:19
SPEAKER_01: What happens when the files, you don't have the file permissions to read it.
22:21
SPEAKER_01: Should you basically ignore it or should you say, hey, my function might be wrong?
22:26
SPEAKER_01: What if one of the files is a shortcut to another file?
22:30
SPEAKER_01: What if it's actually a directory?
22:31
SPEAKER_00: What if it's
22:32
SPEAKER_01: a binary?
22:32
SPEAKER_01: You're now simulating real world.
22:34
SPEAKER_01: Yes, and that's the problem we have,
22:36
SPEAKER_01: is that when you start talking about most interesting domain problems,
22:39
SPEAKER_01: you have to pull in so much context that basically even writing what
22:42
SPEAKER_01: the function is supposed to do becomes a nightmare.
22:45
SPEAKER_01: The imperative program you write that will get it correct 99% of
22:47
SPEAKER_01: the time is probably good enough to use in almost all cases.
22:50
SPEAKER_01: And if you want something that works 100% of the cases,
22:52
SPEAKER_01: you've got to figure out, okay, which file system are we using?
22:54
SPEAKER_01: You have to figure out everything.
22:55
SPEAKER_01: Yeah.
22:56
SPEAKER_01: And that's why it's not done.
22:57
SPEAKER_00: And it would just not be practical.
22:59
SPEAKER_00: It would be for 99% of people, why are you wasting your...
23:03
SPEAKER_00: It's like premature optimization, right?
23:05
SPEAKER_00: Yeah.
23:05
SPEAKER_01: Especially when, as you say, writing 10 tests might get you most of what you need.
23:10
SPEAKER_00: What are practical technologies that you have seen used in some part of the industry
23:15
SPEAKER_00: that even though they will,
23:17
SPEAKER_00: I'm assuming,
23:18
SPEAKER_00: will be somewhat heavyweight because it sounds like pretty heavyweight,
23:20
SPEAKER_00: It might be the return,
23:22
SPEAKER_00: the return of investment of using this heavyweight stuff is worth it that teams
23:26
SPEAKER_00: in industry are using it today.
23:28
SPEAKER_01: Right.
23:29
SPEAKER_01: And here we can basically start to break this down into different parts of the landscape.
23:33
SPEAKER_01: So one part is to look at the stuff that actually does need to be verified to that degree.
23:39
SPEAKER_01: And the usual term here is nukes in NASA, like nuclear power plants and like NASA.
23:45
SPEAKER_01: But I can tell you for the first hand experience,
23:46
SPEAKER_01: nuclear power plants do not care about this stuff.
23:49
SPEAKER_00: They're actually just fine with thorough testing.
23:51
SPEAKER_00: Okay.
23:52
SPEAKER_01: Okay.
23:52
SPEAKER_01: So then category two is like really focused cores of programs
23:56
SPEAKER_01: where they need like one specific part of the program to be like really verified and
24:00
SPEAKER_01: the rest of it, they can use informal methods.
24:02
SPEAKER_01: And this is usually things that are like small parts of databases
24:06
SPEAKER_01: or like cryptographic primitives.
24:08
SPEAKER_01: I believe that the HTTPS stack in Firefox is verified as part
24:11
SPEAKER_01: of something called Project Everest,
24:12
SPEAKER_01: but I might be getting some details of those wrong.
24:14
SPEAKER_00: Would an operating system kernel fall into this or maybe just
24:18
SPEAKER_00: a very key specific part of a kernel like memory allocation or something like that?
24:21
SPEAKER_01: Yeah.
24:22
SPEAKER_01: Parts of an operating system kernel are good uses for this.
24:26
SPEAKER_01: A couple of examples I can think of is I believe Microsoft used some proliferation
24:30
SPEAKER_01: of parts of their Bista kernel for the driver loading.
24:32
SPEAKER_01: Famously,
24:33
SPEAKER_01: there is an operating system called SCL4 that has been end-to-end verified in
24:37
SPEAKER_01: a language called Isabel.
24:38
SPEAKER_01: It's a microkernel.
24:39
SPEAKER_01: It's very small.
24:40
SPEAKER_01: It's mostly used for automotive and military applications,
24:42
SPEAKER_01: but it is a fully verified operating system with a caveat meaning that it's matching
24:47
SPEAKER_01: the specification.
24:48
SPEAKER_01: So it might do the wrong thing,
24:50
SPEAKER_01: but of the things that you specify that it has to do right,
24:52
SPEAKER_01: it will do those specific things right in the right circumstances.
24:55
SPEAKER_01: The last category is the kind I work in,
24:57
SPEAKER_01: which is asking, OK,
24:59
SPEAKER_01: what if instead of verifying the entire real world system,
25:02
SPEAKER_01: which is a nightmare,
25:04
SPEAKER_01: as we just discussed, we create a simplified version of the system and verify that?
25:08
SPEAKER_01: Then the actual system might still have bugs,
25:12
SPEAKER_01: but we can iron out the issues in the abstraction such
25:15
SPEAKER_01: that we don't actually build them in the real system.
25:18
SPEAKER_00: And so that's a topic where you are planning a system and you want to stress test it
25:23
SPEAKER_00: to iron out.
25:24
SPEAKER_01: Yeah, stress test the plan.
25:26
SPEAKER_00: What kinds of plans would these be roughly?
25:29
SPEAKER_00: Is it planning like a database or some sort of distributed system?
25:35
SPEAKER_01: In my work, it's mostly been databases and distributed systems for technology companies.
25:40
SPEAKER_01: But I've had some other interesting gigs.
25:41
SPEAKER_01: I've had one gig that was involving formally verifying firmware of a device kernel.
25:47
SPEAKER_01: And honestly,
25:48
SPEAKER_01: one of the coolest products I ever worked on was verifying the transponders of
25:53
SPEAKER_01: a train system.
25:54
SPEAKER_01: To make sure that they wouldn't cause problems to trains going over those transponders.
25:57
SPEAKER_01: That was a lot of fun.
25:58
SPEAKER_01: We found a really old bug in that one too.
26:00
SPEAKER_01: That was kind of exciting.
26:02
SPEAKER_00: This whole episode is about a question that only gets more important
26:05
SPEAKER_00: as AI writes more of your code.
26:07
SPEAKER_00: How do you know if it's correct?
26:09
SPEAKER_00: And for some parts of a code base, you really don't want an AI model to be taking guesses at.
26:13
SPEAKER_00: Auth is on top of that list.
26:15
SPEAKER_00: And this is where I need to mention our season sponsor, WorkOS.
26:19
SPEAKER_00: If you're building any SaaS, especially an AI product, you'll need Auth for apps and agents.
26:24
SPEAKER_00: This is the layer where close enough is just not good enough.
26:27
SPEAKER_00: So don't let this layer get improvised by AI.
26:30
SPEAKER_00: WorkerWise gives you the proven implementation, SSO, skim,
26:33
SPEAKER_00: and fine-grade authorization built for how agents operate and in a way that's easy
26:37
SPEAKER_00: for them to integrate with an implementation that you can trust.
26:40
SPEAKER_00: Check it out at WorkerWise.com.
26:42
SPEAKER_00: I also want to talk about our season sponsor, TurboPuffer.
26:45
SPEAKER_00: But this time,
26:46
SPEAKER_00: I don't want to talk about how they are fast,
26:48
SPEAKER_00: cheap, and extremely scalable search engine built on object storage.
26:51
SPEAKER_00: Instead, I'd like to talk about their team.
26:53
SPEAKER_00: I interviewed Simon,
26:54
SPEAKER_00: the co-founder and CEO on stage at AI Engineers World Fair,
26:57
SPEAKER_00: and also hung out with their team for a few days in person.
27:00
SPEAKER_00: Here's a few of the interesting things I learned about them.
27:02
SPEAKER_00: The company is full remote, yet feels pretty connected.
27:05
SPEAKER_00: They have a Slack-first culture.
27:07
SPEAKER_00: For example,
27:08
SPEAKER_00: all of their customers have a dedicated Slack channel,
27:10
SPEAKER_00: and engineers are in these channels,
27:11
SPEAKER_00: seeing feedback from these customers, often fixing their bugs.
27:14
SPEAKER_00: The team gets together for annual summits at least twice a year
27:17
SPEAKER_00: and campfires form several times a month anytime several remote employees gather in
27:22
SPEAKER_00: the same city.
27:24
SPEAKER_00: Simon describes their engineering culture as hardcore and whimsical.
27:27
SPEAKER_00: They focus on solving difficult problems but also try to have fun.
27:30
SPEAKER_00: A good example is The Pragmatic Engineer landing page that they built.
27:33
SPEAKER_00: We agreed to have a custom landing page and then their team decided to build
27:36
SPEAKER_00: a cool logo that animates on mouse movement.
27:39
SPEAKER_00: Another interesting thing is their team composition.
27:41
SPEAKER_00: Pretty much everyone currently working at the company has 10-15 years of experience.
27:45
SPEAKER_00: For a startup, they are an unusually seasoned team.
27:48
SPEAKER_00: Finally, I really appreciate how pragmatic their engineering philosophy is.
27:52
SPEAKER_00: Simon and the team strongly believe in how simplicity scales,
27:55
SPEAKER_00: and this is a reason that object storage is TurboPuffer's only dependency.
27:59
SPEAKER_00: The team do seemingly silly things like build their job queue in a single file
28:03
SPEAKER_00: on object storage because they understand the core primitives
28:06
SPEAKER_00: and they know how they scale.
28:08
SPEAKER_00: To check out the whimsical animation,
28:10
SPEAKER_00: or if you're building AI products, head to turbopuffer.com slash pragmatic.
28:14
SPEAKER_00: And with this, let's get back to how TLA Plus works with a demo from Hillel.
28:19
SPEAKER_01: Can we see a demo?
28:20
SPEAKER_01: Okay, sure.
28:20
SPEAKER_01: So I've got a couple languages with me, the kinds that I've worked in.
28:23
SPEAKER_01: So the most popular technology right now for that kind
28:25
SPEAKER_01: of planning is this language called TLA Plus.
28:28
SPEAKER_01: It was invented by Leslie Lamport,
28:29
SPEAKER_01: the same guy who made LaTeX, the typesetting language, actually.
28:33
SPEAKER_01: Oh, yeah.
28:33
SPEAKER_00: All the PDFs behind the scenes are LaTeX.
28:35
SPEAKER_01: Yeah, PDFs behind the scenes are LaTeX.
28:38
SPEAKER_01: He wanted a language that could be used to model distributed systems.
28:42
SPEAKER_01: So he basically created this thing called TLA Plus, Temporal Logic of Actions Plus.
28:46
SPEAKER_01: Everybody always asks about the name.
28:48
SPEAKER_01: You don't need to know the name.
28:49
SPEAKER_01: You just know it as TLA Plus.
28:50
SPEAKER_01: And what it does is it basically represents the state machine of a system.
28:54
SPEAKER_01: Every possible state it can be in and every possible state it can transition to.
28:59
SPEAKER_01: Then...
29:00
SPEAKER_01: We can use a brute force model checking where we basically find every initial state
29:04
SPEAKER_01: and every state that can evolve from those and check if they have properties.
29:07
SPEAKER_01: TLA plus is unique in some ways
29:09
SPEAKER_01: because it has certain properties like checking liveness and refinement
29:12
SPEAKER_01: that we won't get into.
29:13
SPEAKER_01: But let's actually see a demo right now.
29:15
SPEAKER_01: So this is one of the demos I like to use to showcase this.
29:18
SPEAKER_01: And in this demo, we have a simple model of a trading platform.
29:25
SPEAKER_01: Each person on the platform has a set of items.
29:28
SPEAKER_01: And they want to trade these to other people.
29:31
SPEAKER_01: The way that we're going to show the simplified system is that each item is assigned
29:36
SPEAKER_01: to a person.
29:37
SPEAKER_01: There's also a set of outstanding offers.
29:39
SPEAKER_01: We're only going to model sending items to people, not swapping items.
29:44
SPEAKER_01: If you propose an item, you have to own that item.
29:48
SPEAKER_01: And it's basically added to the set of offers.
29:50
SPEAKER_01: And then you can accept an offer.
29:53
SPEAKER_01: If that offer is available, you remove it from the set of offers.
29:57
SPEAKER_01: And the owner transfers.
30:00
SPEAKER_01: If you reject the offer, it's just removed from the set.
30:04
SPEAKER_01: Then we define what can happen next.
30:08
SPEAKER_01: A next state,
30:09
SPEAKER_01: as in one of the ways this system can evolve,
30:11
SPEAKER_01: is we pick some two people that are different,
30:15
SPEAKER_01: that's what this from dash equals two means,
30:17
SPEAKER_01: and some random item,
30:18
SPEAKER_01: and either you propose that item,
30:21
SPEAKER_01: accept a proposal for that item,
30:22
SPEAKER_01: which must already exist, or reject an existing proposal.
30:26
SPEAKER_01: Below we have a property that a valid change is one where if the owner changes,
30:33
SPEAKER_01: it is because the new person accepted an offer from the old person.
30:38
SPEAKER_01: So if the item goes from you to me, it's because you offered it to me and I accepted that offer.
30:43
SPEAKER_01: And then finally we have a change invariant,
30:45
SPEAKER_01: some property of the system saying every change is a valid change.
30:52
SPEAKER_01: Now what's the bug in this?
30:54
SPEAKER_00: Well, first of all, this has a learning curve.
30:56
SPEAKER_01: Yes, it has a learning curve.
30:57
SPEAKER_01: And that's why this is fairly niche.
31:00
SPEAKER_01: And I should probably point out right now that when Leslie Dunbar made this in 1990,
31:04
SPEAKER_01: like before he was thinking of it mostly, he was a mathematician, right?
31:07
SPEAKER_01: So he was using his mathematical like So you have things like quint and p.
31:28
SPEAKER_01: Which are languages that look more like programming languages and are easier
31:31
SPEAKER_01: for people to grok.
31:32
SPEAKER_01: The reason a lot of us use TLA plus was because like
31:35
SPEAKER_01: the first really high profile demonstration of this kind of work in practice was
31:39
SPEAKER_01: an Amazon paper.
31:41
SPEAKER_01: The use of formal methods in Amazon Web Services in 2014.
31:44
SPEAKER_01: And they use TLA plus for this.
31:46
SPEAKER_01: So that's what a lot of us just have originally started on.
31:49
SPEAKER_00: So going back to this, there is a bug in this one with all the associations.
31:55
SPEAKER_00: And how can we figure out what the bug is?
31:57
SPEAKER_00: Will the system help tell us or we now need to think through what case we missed?
32:03
SPEAKER_01: Well, if we had to think through it ourselves, we wouldn't be using this nasty syntax, would we?
32:08
SPEAKER_00: Nope.
32:10
SPEAKER_01: So what I've done is I've also written a quick configuration file saying,
32:14
SPEAKER_01: take a specification,
32:16
SPEAKER_01: take these three people, Alice, Bob, Carl, and have them trade around a stick.
32:21
SPEAKER_01: And then I tell it, make sure this property that the change in variant always holds.
32:25
SPEAKER_01: Always holds, yep.
32:26
SPEAKER_01: Now I just have to run this.
32:31
SPEAKER_01: I'm also having it output the state space for you so you can see what that looks like.
32:34
SPEAKER_01: And it just puts out the error for us.
32:36
SPEAKER_01: It says the property has been violated.
32:38
SPEAKER_01: It took 53 states to find it.
32:41
SPEAKER_01: And the way it works is it's on a small screen, so it's being word wrapped.
32:46
SPEAKER_01: But if I see it kind of looks like this.
32:48
SPEAKER_01: Essentially, the error is as follows.
32:50
SPEAKER_01: And let's actually see if the error, I can show it to you with the .file.
32:57
SPEAKER_02: .viz, .viz, not .viz, what am I saying?
33:03
SPEAKER_02: So this is just a preview of the state space it's generating.
33:10
SPEAKER_01: So you can see it's basically generating every possible state it can find.
33:13
SPEAKER_01: This isn't the whole state space.
33:14
SPEAKER_01: Usually because the state spaces end up being like 100 million states in
33:18
SPEAKER_01: the state space, usually these aren't that useful.
33:20
SPEAKER_01: It's mostly a thing that we sometimes use for demos.
33:23
SPEAKER_01: So the error is as follows.
33:25
SPEAKER_01: Alice, Bob, and Carol are on the system, and Alice owns the stick.
33:30
SPEAKER_01: Alice makes an offer to Bob.
33:32
SPEAKER_01: Bob is away.
33:34
SPEAKER_01: Alice gets tired of waiting for Bob to come back to make the offer because she wants
33:37
SPEAKER_01: to get rid of her stick.
33:38
SPEAKER_01: She makes the offer to Carol.
33:41
SPEAKER_01: Carol immediately accepts.
33:42
SPEAKER_01: So the stick transfers from Alice to Carol.
33:45
SPEAKER_01: Now, Bob comes back,
33:47
SPEAKER_01: sees the offer from Alice to Bob,
33:48
SPEAKER_01: and goes,
33:48
SPEAKER_01: oh yeah, I want that stick, clicks the button, and now the stick becomes Bob's.
33:52
SPEAKER_01: But it did not transfer from Alice to Bob, it transferred from Carol to Bob.
33:55
SPEAKER_01: So the change in variant that if the stick went from Carol to Bob,
33:58
SPEAKER_01: it must be because Carol made an offer that Bob accepted was violated.
34:03
SPEAKER_01: And therefore, the system raises an error.
34:05
SPEAKER_00: And then how did the system simulate this?
34:08
SPEAKER_00: It had to simulate a state where Bob was waiting or didn't respond for a while
34:14
SPEAKER_00: and responded later.
34:15
SPEAKER_01: We basically,
34:16
SPEAKER_01: assuming we start a state of basically Alice owns the stick,
34:21
SPEAKER_01: there's two possible things that
34:22
SPEAKER_02: can happen here, right?
34:23
SPEAKER_02: We have offer Bob.
34:27
SPEAKER_02: Yep.
34:28
SPEAKER_02: And we have offer Bob.
34:30
SPEAKER_01: Carol, right?
34:31
SPEAKER_01: So those both happen, and those are both distinct states.
34:35
SPEAKER_01: So the model checker says, okay, I'm going to create two new states.
34:39
SPEAKER_01: Then from this top one of offer Bob, there's three things that can happen.
34:43
SPEAKER_02: We can have Bob accept,
34:47
SPEAKER_02: Bob reject,
34:50
SPEAKER_02: or, and this is where the concurrency comes in, we can do offer
34:52
SPEAKER_01: Carol, right?
34:53
SPEAKER_01: Yep.
34:55
SPEAKER_00: I see.
34:56
SPEAKER_00: Yeah.
34:57
SPEAKER_00: I see where this is coming.
34:58
SPEAKER_00: And then when you continue, we will hit the bug.
35:01
SPEAKER_01: Yeah.
35:01
SPEAKER_00: The changing variant will be invalid at whatever step that is run at.
35:07
SPEAKER_01: Right.
35:07
SPEAKER_01: And that's actually where a lot of this, like, Yeah, so this is what TLA plus is then.
35:39
SPEAKER_00: Yeah, basically.
35:41
SPEAKER_00: And one story I've heard, and I think you might have been involved, is AWS using TLA+.
35:48
SPEAKER_00: Can you talk about how they onboard it,
35:50
SPEAKER_00: how they're using it, what they're using it for, as far as you're aware?
35:53
SPEAKER_00: Yeah.
35:54
SPEAKER_01: So the seminal paper on this was in 2014.
35:58
SPEAKER_01: The Use of Problem Methods at Amazon Web Services.
36:01
SPEAKER_01: And they talked about how a couple of people in the company were interested in
36:04
SPEAKER_01: and learned TLA+,
36:05
SPEAKER_01: in another language called Pluscow, which is something that compiles TLA+.
36:09
SPEAKER_01: And applied it to aspects of the DynamoDB and S3 storage systems.
36:15
SPEAKER_01: In doing so, they're able to find fairly complicated bugs that could potentially lose data.
36:20
SPEAKER_01: And I think it was in the replication system.
36:22
SPEAKER_00: In the paper,
36:22
SPEAKER_00: it said that the shortest error trace exhibiting
36:25
SPEAKER_00: the bug contained 35 high-level steps.
36:28
SPEAKER_00: Which, if I understand that correctly,
36:31
SPEAKER_00: it was at a depth that it would have been very hard for a human to persevere
36:35
SPEAKER_00: or you would have needed to be really determined and precise.
36:39
SPEAKER_01: I did not work on that project, of course, so I don't know what the details are.
36:41
SPEAKER_01: I can speculate that the reason it found a 35-step bug was because
36:44
SPEAKER_01: the state space was probably 100 million states wide.
36:47
SPEAKER_01: So there were like plenty of, say, like 70 or 80 step chains that were totally safe.
36:52
SPEAKER_01: And just having this one 35-step chain was invalid.
36:55
SPEAKER_00: Through working with a lot of customers and teams
36:59
SPEAKER_00: that have used formal verifications with distributed systems, what are some...
37:04
SPEAKER_00: Problems you've come across with distributed systems that might be a bit of
37:08
SPEAKER_00: a repeat pattern of, you know, how they break down or why they break down.
37:11
SPEAKER_01: And I can think of, like,
37:12
SPEAKER_01: one thing that, like,
37:13
SPEAKER_01: besides, like,
37:13
SPEAKER_01: just general race conditions and locks,
37:15
SPEAKER_01: this is the one that, like, is always when you pull your hands off.
37:17
SPEAKER_01: It's like, yes, it's another time to allow, time to check the time to use bug.
37:22
SPEAKER_01: And time to check the time to abuse is a situation where...
37:24
SPEAKER_01: You are checking to see if something is like valid, can be done validly.
37:28
SPEAKER_01: And then you see that it's correct.
37:29
SPEAKER_01: And then a little bit later, you do it.
37:31
SPEAKER_01: Sometimes that little bit later is like a day later.
37:33
SPEAKER_01: Sometimes it's a microsecond later.
37:34
SPEAKER_01: But is any case where it is possible for something to go from being valid
37:37
SPEAKER_01: to being invalid in between the time you check and the time you use it?
37:42
SPEAKER_01: A good example here is imagine you're withdrawing like money from a bank account
37:48
SPEAKER_01: and putting it to another bank account.
37:49
SPEAKER_01: And this is not how banks work.
37:50
SPEAKER_01: I know they use a different kind of ledger.
37:52
SPEAKER_01: But just as a demonstrative example, Yeah, and it's very interesting because when...
38:18
SPEAKER_00: We were building Uber's payment system.
38:19
SPEAKER_00: I realized or I learned that the problem of having a message delivered in
38:24
SPEAKER_00: a distributed system exactly once is a very difficult one
38:29
SPEAKER_00: because typically that's what you need when you want to do one charge.
38:33
SPEAKER_00: You want to charge a customer's card exactly once because
38:36
SPEAKER_00: if you send multiple messages just in case one of them gets lost,
38:39
SPEAKER_00: you now have double charges.
38:40
SPEAKER_00: It turns out it's a complicated problem.
38:44
SPEAKER_00: It's a lot easier to do at least one's delivery than exactly one's delivery.
38:49
SPEAKER_00: But of course,
38:50
SPEAKER_00: you need exactly at least one's delivery to build on
38:53
SPEAKER_00: to create exactly one's delivery.
38:56
SPEAKER_01: Yeah.
38:57
SPEAKER_01: I wonder if this is like a lot of like businesses,
38:59
SPEAKER_01: they just charge you extra than refund you some amount.
39:03
SPEAKER_01: That seems like easier to do from an engineering perspective.
39:06
SPEAKER_00: As well,
39:07
SPEAKER_00: it's also from a risk perspective,
39:08
SPEAKER_00: you eliminate a lot of edge cases by authorizing upfront on the credit card,
39:14
SPEAKER_00: you have a credit limit.
39:15
SPEAKER_00: And if you would authorize exactly how much you think you need right now,
39:19
SPEAKER_00: but you need a bit more,
39:20
SPEAKER_00: you might get into that edge case where later you have trouble authorizing it.
39:23
SPEAKER_00: This is why often hotels don't want to deal with this.
39:25
SPEAKER_00: So they just authorize a larger chunk.
39:28
SPEAKER_00: And they know because it's a larger amount for hotels.
39:31
SPEAKER_00: Otherwise,
39:31
SPEAKER_00: they might have run into the thing where you run out of your credit
39:33
SPEAKER_00: and now they have to do a separate flow.
39:36
SPEAKER_00: But you're right.
39:37
SPEAKER_00: So some enduring decisions might happen because it's easier to do some stuff.
39:41
SPEAKER_01: Yeah, it makes sense.
39:42
SPEAKER_01: I honestly thought hotels did that because they were trying to convince you not to break stuff.
39:46
SPEAKER_01: Because like, hey,
39:47
SPEAKER_01: if you know that you're definitely going to lose $800 if you break something,
39:50
SPEAKER_01: you're not going to break stuff.
39:51
SPEAKER_00: Through working with engineering teams who are building distributed systems
39:54
SPEAKER_00: and you're coming in and helping them learn TLA plus learn how to survive things,
39:58
SPEAKER_00: what have you learned about how they usually think of verifying distributed systems
40:02
SPEAKER_00: before they learn about formal methods and what changes after?
40:06
SPEAKER_01: So I think the most interesting thing about formal methods
40:10
SPEAKER_01: and how it affects how you build systems isn't the theory of the method
40:15
SPEAKER_01: or how it makes you think about systems.
40:16
SPEAKER_01: It's the practice.
40:18
SPEAKER_01: Why is concurrency hard?
40:19
SPEAKER_01: Why is it hard for us to reason about concurrent systems?
40:22
SPEAKER_01: Why do you think it's hard?
40:23
SPEAKER_00: I think it's hard to keep several things in your mind of like where they could be.
40:29
SPEAKER_00: That's one.
40:30
SPEAKER_00: Or maybe we just don't really have a mental model of how to draw them out.
40:36
SPEAKER_00: I guess whiteboarding would be a way to do it,
40:38
SPEAKER_00: but I don't remember whiteboarding on concurrent system.
40:41
SPEAKER_00: I remember whiteboarding just boxes and imperative.
40:45
SPEAKER_00: This flowcharts are good for whiteboarding.
40:47
SPEAKER_01: So this is something that I've wondered a lot, right?
40:49
SPEAKER_01: Like why it's hard for us to deal with these systems.
40:51
SPEAKER_01: And I'm not sure it's because it's hard for us to think about them.
40:56
SPEAKER_01: I mean, like when you cross the street, aren't you working with a concurrent system?
41:00
SPEAKER_01: You're just, there's cars everywhere.
41:02
SPEAKER_01: They're going to hit you.
41:03
SPEAKER_01: You're going to die if you don't model the concurrent system in your head.
41:06
SPEAKER_01: And there's actually this really cool paper I found called Common Sense Computing.
41:10
SPEAKER_01: Where some people were trying to figure out like how people thought about concurrent systems.
41:14
SPEAKER_01: When talking with like sort of like high school and college students,
41:17
SPEAKER_01: they changed the concurrency problem from like, hey,
41:19
SPEAKER_01: we've got these threads doing some operation to like, hey,
41:21
SPEAKER_01: we've got these like Clerks at a ticket office,
41:24
SPEAKER_01: assigning seats at a concert, people saw the bug much faster.
41:28
SPEAKER_01: So I do think we can actually get quite good at seeing concurrency issues.
41:33
SPEAKER_01: I think a large part of the problem of why it's hard for us is because we don't get
41:37
SPEAKER_01: a lot of practice.
41:38
SPEAKER_01: Usually when you have a race condition in a system,
41:40
SPEAKER_01: you find out months later and then you try a fix and you find out weeks later after
41:45
SPEAKER_01: that if the fix actually worked.
41:47
SPEAKER_01: Whereas with the TLA+,
41:49
SPEAKER_01: like I write my model of the system and then I click a button and it tells me,
41:51
SPEAKER_01: hey, race condition.
41:52
SPEAKER_01: And then you fix it and it says like, hey, timeout bug.
41:55
SPEAKER_01: And then you fix it again and it says, hey, TOCTOU bug.
41:58
SPEAKER_01: And that feedback loop ends up being so much faster than you get in practice.
42:03
SPEAKER_01: And I think that more
42:04
SPEAKER_01: than anything else helps people find race conditions more easily and think
42:07
SPEAKER_01: about problems in distributed systems more easily.
42:10
SPEAKER_01: I've found personally that when I work with new clients, I wonder if it's a little bit like...
42:44
SPEAKER_00: Refactoring and also migrations.
42:46
SPEAKER_00: So refactoring a code base when you are starting out as a developer and you need
42:50
SPEAKER_00: to do a refactoring by hand,
42:52
SPEAKER_00: you know,
42:52
SPEAKER_00: let's say just changing a function name and then you need to go and change all
42:55
SPEAKER_00: the references of function.
42:57
SPEAKER_00: And the first time you do it, you change it at a few places and then you forget about the rest.
43:01
SPEAKER_00: And either it's a compilation issue or if it's a dynamic language, it's another problem.
43:05
SPEAKER_00: But then you get good at it once you practice.
43:07
SPEAKER_00: With migrations,
43:08
SPEAKER_00: most engineers that I've seen are terrible at migrations because you need to make
43:12
SPEAKER_00: a plan, you need to check, you keep in shadowing, reverse shadowing, all that funk.
43:18
SPEAKER_00: And then there are a few engineers who have done three or four or five,
43:20
SPEAKER_00: and then they close their eyes and they can just do it.
43:23
SPEAKER_00: I'm just thinking that when it comes to race conditions,
43:25
SPEAKER_00: most of us, I was exposed to race conditions by, oh, we did a double charge.
43:29
SPEAKER_00: And then we found the race condition, but I never did a second one.
43:34
SPEAKER_00: So I will not be good at finding race conditions.
43:36
SPEAKER_00: I'm not even good at thinking about them.
43:38
SPEAKER_01: I think that's right on the money.
43:40
SPEAKER_00: It sounds like you coming into teams or to these clients,
43:44
SPEAKER_00: it You have to please give them some practice,
43:46
SPEAKER_00: the very least,
43:47
SPEAKER_00: of how to think about this category of errors,
43:50
SPEAKER_00: even assuming that taking out even the tooling itself.
43:55
SPEAKER_01: I think there's also like more subtle things that you start to pick up from these tools.
43:58
SPEAKER_01: But I think that's like the most visceral one,
43:59
SPEAKER_01: the visceral like hatred of a race condition that gets a like physical presence in
44:05
SPEAKER_01: the algorithm.
44:06
SPEAKER_00: You've been doing this for a very long year for you.
44:09
SPEAKER_00: Writing TLA plus is like for most of us writing TypeScript or the language
44:13
SPEAKER_00: that we're familiar with.
44:14
SPEAKER_00: How has your thinking changed?
44:16
SPEAKER_00: And is there any similarities between when you program an imperative language and
44:20
SPEAKER_00: then you learn a different one,
44:22
SPEAKER_00: like a declarative language, which requires a very different thinking?
44:25
SPEAKER_01: And that also depends on the declarative language.
44:26
SPEAKER_01: Like I've, I've,
44:27
SPEAKER_01: I've done a lot of stuff in like logic programming languages
44:30
SPEAKER_01: and like I've done some stuff in like array languages,
44:33
SPEAKER_01: but like you show me CSS, I'm just like, what is this dark magic?
44:37
SPEAKER_01: Declarative?
44:37
SPEAKER_01: What are you talking about?
44:38
SPEAKER_01: I think so.
44:39
SPEAKER_01: It's going to be hard to sort of pin down exactly what though.
44:42
SPEAKER_01: Like my usual hacking language is Python these days,
44:45
SPEAKER_01: just because that's like one of the first things I use and I just know very well.
44:48
SPEAKER_01: And I think like at the very least,
44:49
SPEAKER_01: like the formal methods makes me much more willing to reach
44:52
SPEAKER_01: for mathematical solutions or like math heavy solutions than like simple,
44:56
SPEAKER_00: reliable solutions.
44:58
SPEAKER_00: Math is also an interesting topic.
45:00
SPEAKER_00: You've recently had a bit of back and forth on whether...
45:03
SPEAKER_00: Developers, programmers, software engineers should learn math.
45:06
SPEAKER_00: There was a bit of a discussion back and forth.
45:08
SPEAKER_00: Can we talk about the core of the argument?
45:11
SPEAKER_01: How math is useful in programming is a very interesting question, right?
45:14
SPEAKER_01: So first of all, there's math that we all find so useful we forget that it's actually math.
45:18
SPEAKER_01: Like counting.
45:19
SPEAKER_01: Counting is math.
45:21
SPEAKER_01: Knowing whether one thing is bigger than another number is math, right?
45:23
SPEAKER_01: It's just math that we have been taught from a very young age because it is
45:27
SPEAKER_01: so important that no matter what you're doing in life, you need that math.
45:30
SPEAKER_01: Then there's a lot of math that is useful for very specific specialist jobs.
45:34
SPEAKER_01: Like I've talked to some SREs who need calculus,
45:37
SPEAKER_01: but I think most programmers do not need calculus.
45:40
SPEAKER_01: There are some branches of math that are useful in a wide range of programming.
45:43
SPEAKER_01: I think things like understanding graphs and directed graphs,
45:46
SPEAKER_01: knowing matrices,
45:48
SPEAKER_01: knowing formal logic can be very useful for a lot of different people.
45:51
SPEAKER_01: But I think it is more useful for most developers to have an exposure
45:55
SPEAKER_01: to like what math has in the various fields versus just going on every single field
46:00
SPEAKER_01: when they see them, right?
46:01
SPEAKER_01: You've got to know what's available to know what's most useful for you.
46:04
SPEAKER_01: And most math will not be useful for you.
46:06
SPEAKER_00: It's also very interesting because for a long time,
46:08
SPEAKER_00: I thought at university,
46:09
SPEAKER_00: we have pretty heavy math education for computer science from algebra
46:13
SPEAKER_00: to computational theories, even formal methods.
46:17
SPEAKER_00: At university, I learned a bunch of advanced math.
46:19
SPEAKER_00: At first,
46:19
SPEAKER_00: when I came into the industry,
46:21
SPEAKER_00: it wasn't particularly useful or I didn't use it day to day.
46:24
SPEAKER_00: But then there are some tests.
46:26
SPEAKER_00: It's kind of useful.
46:27
SPEAKER_00: For example, matrix transformation.
46:29
SPEAKER_00: I learned 3D graphics and how you compute all the points based on 3D matrix transformations.
46:35
SPEAKER_00: And then it helped me understand when GPUs were becoming so powerful with AI,
46:39
SPEAKER_00: why this is because they're also very good at And I think going back
46:42
SPEAKER_00: to our discussion with the crossover project,
46:45
SPEAKER_00: I wonder if it helps you connect closer with other engineering disciplines in terms
46:48
SPEAKER_00: of you can understand more things there.
46:50
SPEAKER_00: For example,
47:10
SPEAKER_00: For electrical engineering, you do have math involved that is there to describe.
47:15
SPEAKER_00: And if you will want to have the vocabulary to understand that part.
47:21
SPEAKER_01: One of the interesting things,
47:21
SPEAKER_01: at least about the mathematical differences,
47:24
SPEAKER_01: is that in almost every traditional engineering field,
47:26
SPEAKER_01: the math they need is continuous math analysis,
47:28
SPEAKER_01: things like differential equations and calculus.
47:32
SPEAKER_01: And that in the United States is what's taught like at an advanced level
47:34
SPEAKER_01: in high school, if you get that far, is this kind of continuous math.
47:39
SPEAKER_01: In software engineering and computer science, the math that we most often use is discrete math.
47:43
SPEAKER_01: Things like combinatorics,
47:45
SPEAKER_01: basically which is the math of counting things,
47:47
SPEAKER_01: graph theory,
47:49
SPEAKER_01: formal logic,
47:50
SPEAKER_01: set theory,
47:51
SPEAKER_01: things that work with discrete entities,
47:54
SPEAKER_01: which isn't usually taught,
47:56
SPEAKER_01: at least in the American high school very much,
47:58
SPEAKER_01: or even early in university mathematics classes.
48:02
SPEAKER_01: And I wonder sometimes if that is the reason people don't recognize the use of math
48:06
SPEAKER_01: in software engineering is because the math they do need is not
48:09
SPEAKER_01: the math they've been exposed to.
48:11
SPEAKER_00: Interesting.
48:11
SPEAKER_00: Yeah, because the math that I did use more was Common Networks.
48:16
SPEAKER_00: And of course,
48:16
SPEAKER_00: like maybe these days those injuries are going out of style,
48:20
SPEAKER_00: but there's the here's a problem, build an algorithm that solves it.
48:24
SPEAKER_00: And then you ask like, OK, how efficient is this algorithm?
48:26
SPEAKER_00: And then there's a big old notation.
48:28
SPEAKER_00: We have the language to describe how efficient in space and time is,
48:32
SPEAKER_00: and you can do trade-offs,
48:34
SPEAKER_00: and once two people know the same thing,
48:37
SPEAKER_00: you can have discussions about these things.
48:40
SPEAKER_00: And on one end,
48:41
SPEAKER_00: it's very abstract,
48:41
SPEAKER_00: but on the other end, if you're close to the machine, it can be very useful.
48:45
SPEAKER_01: I've also found that my understanding of big O notation got
48:47
SPEAKER_01: a lot better once I understood the mathematics behind it,
48:49
SPEAKER_01: because I think it's usually explained in terms of like, oh,
48:52
SPEAKER_01: This function scales at this certain rate,
48:53
SPEAKER_01: but like it is more formally a way of describing a set of functions.
48:57
SPEAKER_01: And then there's the math of like how we do asymptotics and stuff, but like, et cetera.
49:01
SPEAKER_01: I think even like the technical aspects of math does help a lot in understanding those.
49:05
SPEAKER_00: Yeah.
49:06
SPEAKER_00: And with the TLA plus specifically,
49:09
SPEAKER_00: what cases have you seen in the industry TLA plus being a good fit
49:14
SPEAKER_00: for certain problems?
49:16
SPEAKER_00: And in what cases would you never consider it?
49:18
SPEAKER_01: I think the case of TLA plus and...
49:21
SPEAKER_01: Most, not all,
49:22
SPEAKER_01: but most role methods,
49:24
SPEAKER_01: they shine the most in highly computational domains where most
49:27
SPEAKER_01: the problems are highly technical and not like business embedded.
49:35
SPEAKER_01: And what I mean by that is that like how do you replicate nodes
49:38
SPEAKER_01: between these two data sets is like very technical, right?
49:42
SPEAKER_01: Something like I'm trying to think about like a good example here,
49:45
SPEAKER_01: like how do we make sure our sprints don't go over time?
49:51
SPEAKER_01: It's very business, right?
49:52
SPEAKER_01: It deals with like very human behaviors.
49:53
SPEAKER_01: I've had to help model client model that.
49:56
SPEAKER_01: And we got some use out of it, but it was very hard.
49:58
SPEAKER_01: So that's why a lot of my clients end up being things like database vendors
50:01
SPEAKER_01: or like cloud computing people who are or like hardware people who are working in
50:05
SPEAKER_01: a space that's like very important for business,
50:08
SPEAKER_01: but several steps removed from like the front lines of that business.
50:11
SPEAKER_01: The other thing I would say is that Different tools are good at different things.
50:16
SPEAKER_01: TLA Plus in particular tends to be good at discrete distributed systems where
50:21
SPEAKER_01: the main challenges are messing with concurrency and possibilities
50:24
SPEAKER_01: of interleaving-like behaviors.
50:26
SPEAKER_01: It doesn't do floating point.
50:28
SPEAKER_01: It doesn't do decimals.
50:29
SPEAKER_01: It Doesn't do as well when you're trying to figure out probabilistic things.
50:33
SPEAKER_01: Oh, that's another thing I guess I should be saying is that like where the kinds
50:36
SPEAKER_01: of errors you care about are ones where like if it is possible to happen,
50:40
SPEAKER_01: that is a big deal.
50:41
SPEAKER_01: It's not good if like you're like, OK,
50:43
SPEAKER_01: this error is bad,
50:43
SPEAKER_01: but as long as it happens less than one out of 100 times, it's OK.
50:48
SPEAKER_01: It can't do that kind of probabilistic reasoning for you.
50:50
SPEAKER_01: There are tools that can, but they lack things like functions or arrays or variables.
50:57
SPEAKER_01: Numbers also depends on how much time you need to spend planning.
51:00
SPEAKER_01: Like if you don't need to spend that much time planning, this is going to waste your time.
51:04
SPEAKER_01: I do want to add that,
51:04
SPEAKER_01: that this like,
51:05
SPEAKER_01: if you can iterate your way through a solution and the bugs aren't going to be
51:09
SPEAKER_01: that costly, then you might not need this tool.
51:12
SPEAKER_01: I think it's really important as like a person who talks about a really exotic tool
51:15
SPEAKER_01: to like constantly emphasize and like, no,
51:17
SPEAKER_01: I'm not trying to convince you to like use something that's not a good choice
51:19
SPEAKER_01: for you.
51:20
SPEAKER_01: I think a lot of the reason people are skeptical of these
51:22
SPEAKER_01: because they've been burned by things like Case and UML
51:25
SPEAKER_01: and all these other miracle solutions that were forced on them by people
51:28
SPEAKER_01: who wanted them to use it no matter what.
51:30
SPEAKER_01: And I think it's really important to always say,
51:31
SPEAKER_01: like, if this is the right tool for you, I am not going to recommend it.
51:34
SPEAKER_00: And then can we talk about other tools?
51:37
SPEAKER_00: Or can you show us a few other ones?
51:39
SPEAKER_01: Yeah.
51:39
SPEAKER_01: So the other tool I have installed on this computer is called Alloy,
51:43
SPEAKER_01: and it was made by an MIT professor.
51:47
SPEAKER_01: Different from what is lineage.
51:48
SPEAKER_01: Just like there's many different kinds of programming languages,
51:50
SPEAKER_01: there's many lineages of formal specification verification tools.
51:54
SPEAKER_01: So this example is a simple access control system.
51:59
SPEAKER_01: So we have a set of resources and users who can read those resources.
52:05
SPEAKER_01: So each resource has some people who it's reasonable by.
52:08
SPEAKER_01: And resources may or may not have a parent resource.
52:11
SPEAKER_01: L1 meaning less than or equal to one resource.
52:14
SPEAKER_01: There are no cycles.
52:15
SPEAKER_01: So no resource can have itself as a parent or its parent's parent as a parent.
52:20
SPEAKER_01: You can read,
52:21
SPEAKER_01: access a resource if the resource indicates you can read that resource or
52:26
SPEAKER_01: if its parent indicates you can read that resource.
52:29
SPEAKER_01: And we have a property that if you can read a resource, you can read its children.
52:34
SPEAKER_01: This system has a bug.
52:35
SPEAKER_01: What is it?
52:39
SPEAKER_00: I mean, I'm glancing at this and this all made sense to me.
52:42
SPEAKER_00: I thought this is it because we're saying all of the parents can access it.
52:47
SPEAKER_00: I'm assuming the bug,
52:48
SPEAKER_00: if there is one,
52:48
SPEAKER_00: it might have to do with something that we talked earlier of like accessing
52:52
SPEAKER_00: in certain areas.
52:54
SPEAKER_00: No idea.
52:54
SPEAKER_00: Can we run it?
52:56
SPEAKER_01: Yes, we can.
52:57
SPEAKER_01: So this was actually made in an earlier version of Alloy just for context.
53:00
SPEAKER_01: Alloy did not have any sort of temporal reasoning over state up until about Now,
53:05
SPEAKER_01: if I execute this,
53:39
SPEAKER_01: Here's the counter example.
53:42
SPEAKER_01: And this is one of the things about Ally specifically is that it can generate visualizations.
53:47
SPEAKER_01: So basically, here's the problem.
53:49
SPEAKER_01: We have a user who can read a parent resource.
53:55
SPEAKER_01: The parent has a child.
53:57
SPEAKER_01: Because of how we defined can access, we can read his parent so we can read the child.
54:05
SPEAKER_01: The child has a grandchild.
54:08
SPEAKER_01: We cannot read the grandchild.
54:10
SPEAKER_01: So, because we are not in,
54:13
SPEAKER_01: we are not assigned to the readable by for the child, only the parent.
54:18
SPEAKER_01: In other words, readable by is not transitive.
54:20
SPEAKER_01: So we can read the child, but not the child's children.
54:22
SPEAKER_01: And that is the bug.
54:24
SPEAKER_00: And to visualize this for us.
54:25
SPEAKER_01: Yes, which is quite nice.
54:27
SPEAKER_01: And one of the reasons why people really like Alloy.
54:28
SPEAKER_00: Nice.
54:30
SPEAKER_01: It's a bit worse for modeling,
54:31
SPEAKER_01: like, distributed systems, though, which is why most of my work is in TLA+.
54:35
SPEAKER_00: And then to do the fix, what would it involve?
54:38
SPEAKER_00: We would need to give access to the children's children?
54:45
SPEAKER_01: Yeah, there's a few different ways that we could fix it.
54:48
SPEAKER_01: And often, like, problem methods, they don't really tell you, here's how you fix it.
54:50
SPEAKER_01: It lets you choose how you want to fix it.
54:52
SPEAKER_01: Like, one thing I could do is I could say, okay,
54:55
SPEAKER_01: I'm going to say that this is a transitive lookup too,
55:00
SPEAKER_01: that we transitively close over all parents.
55:02
SPEAKER_01: And if I execute that, no more counterexample.
55:05
SPEAKER_01: That said, that might not be something physically implementable.
55:09
SPEAKER_01: I might try to tell like, hey,
55:09
SPEAKER_01: people like, hey,
55:10
SPEAKER_01: in our SQL database,
55:11
SPEAKER_01: you have to have a transitive query and our database administrator is like,
55:14
SPEAKER_01: no, that's going to crash the database.
55:15
SPEAKER_01: You can't do that.
55:15
SPEAKER_01: Then we have to find a different fix.
55:18
SPEAKER_00: So this is the beauty of formal methods.
55:22
SPEAKER_00: Yes, it gives you opportunities of how you will implement fixes,
55:26
SPEAKER_00: changes, and then you can rerun it again and see what difference it made.
55:30
SPEAKER_01: Exactly.
55:31
SPEAKER_01: Now, one quick fun fact.
55:32
SPEAKER_01: I love just fun facts about stuff.
55:34
SPEAKER_01: You see how this says solver sat4j?
55:36
SPEAKER_01: So have you heard of sat, S-A-T problems?
55:40
SPEAKER_00: No.
55:40
SPEAKER_01: Okay.
55:41
SPEAKER_01: Is there some variable that makes the statement P true?
55:45
SPEAKER_01: If I can make P true or false, is there a way I can make that true?
55:48
SPEAKER_01: Let's say P is a Boolean and I have a statement P.
55:52
SPEAKER_01: Can you assign some value of true or false to P to make that true?
55:57
SPEAKER_00: Typically, you can assign true and it will be correct.
55:59
SPEAKER_00: Well, true.
56:00
SPEAKER_01: That's even unsatisfiable by setting P to true.
56:02
SPEAKER_01: What about P and not Q?
56:06
SPEAKER_00: Also satisfiable by giving true to P and false to Q.
56:12
SPEAKER_01: Right.
56:12
SPEAKER_01: Now what about P and Q and not P?
56:16
SPEAKER_00: That's unsatisfiable because no matter what ruling you do, true and false will always be true.
56:24
SPEAKER_01: Lovely.
56:24
SPEAKER_01: What you've just done is a Boolean satisfiability problem.
56:27
SPEAKER_01: Taken some sort of statement of a ton of Boolean variables,
56:30
SPEAKER_01: in this case too,
56:31
SPEAKER_01: and either found some assignment that makes it true or said
56:34
SPEAKER_01: that it cannot be made true.
56:36
SPEAKER_01: Now, Boolean satisfiability is what we call NP-complete.
56:39
SPEAKER_01: And what that means in theory is that there's no such thing as
56:42
SPEAKER_01: a perfectly efficient algorithm that solves all problems.
56:45
SPEAKER_01: In practice, that means that we can solve them really fast.
56:49
SPEAKER_01: So often what makes Alloy interesting is that unlike TLA+,
56:53
SPEAKER_01: which must be brute-forced, Alloy can be converted into a satisfiability problem.
57:01
SPEAKER_01: I'll open this up.
57:03
SPEAKER_01: And it is able to turn that model into a Boolean probability saying not x21 and x96 and 0.
57:15
SPEAKER_01: So X15 or not X72, etc.
57:20
SPEAKER_01: And because of that,
57:21
SPEAKER_01: most alloy models can be checked in like a few milliseconds or a second at most.
57:26
SPEAKER_01: Whereas often for like a large TLA plus model,
57:28
SPEAKER_01: you have to basically churn it overnight to go through all 100 million states.
57:32
SPEAKER_00: Can we talk about some other tools on the table of someone looking into formal verification?
57:39
SPEAKER_01: Happily.
57:40
SPEAKER_01: So I don't have any more demos on my PC right now, but I can talk about a few of them.
57:45
SPEAKER_01: So a couple of the ones that have been successful to TLA Plus is the P language,
57:50
SPEAKER_01: which was invented by,
57:51
SPEAKER_01: I think,
57:52
SPEAKER_01: a person at Microsoft Research who was then poached by Amazon as a way of making
57:56
SPEAKER_01: a language that was more accessible than TLA Plus, among other things.
58:00
SPEAKER_01: So it basically looks like a set of state machines,
58:03
SPEAKER_01: interacting state machines that send messages to each other,
58:05
SPEAKER_01: almost like the actor model in like Erlang or something like that.
58:08
SPEAKER_01: Yep.
58:08
SPEAKER_01: So there's that.
58:10
SPEAKER_01: There's also another one in the same space as Quint,
58:12
SPEAKER_01: which was basically people who were making a different kind of model check
58:15
SPEAKER_01: for TLA Plus and then
58:17
SPEAKER_00: realized they can make an
58:19
SPEAKER_01: entire language that was easier
58:20
SPEAKER_01: for people to pick up.
58:21
SPEAKER_01: They've gotten a lot of interest in the banking and I believe cryptocurrency space,
58:26
SPEAKER_01: smart contracts.
58:28
SPEAKER_01: So another one that I've used,
58:29
SPEAKER_01: which is a lot more niche, but quite interesting, is called Prism.
58:32
SPEAKER_01: And Prism is a probabilistic mile checker.
58:35
SPEAKER_01: So like KLA Plus can tell you like this bug will never happen or it could happen.
58:39
SPEAKER_01: Prism can tell you this bug can happen 10% of the time or it is a 25% chance
58:45
SPEAKER_01: of happening if you shut down.
58:47
SPEAKER_01: It's really cool,
58:48
SPEAKER_01: but it's also much more like academic in that there's a lot more work required
58:52
SPEAKER_01: to actually translate languages into Prism.
58:54
SPEAKER_01: If you're interested in it,
58:55
SPEAKER_01: I've basically been doing this like, have you heard of the Jewish game Dreidel?
58:59
SPEAKER_00: No.
59:00
SPEAKER_01: Okay, it's a game that you play on Klanica where you spin a little top and you get money.
59:03
SPEAKER_01: And I do not like the game.
59:05
SPEAKER_01: And I have written a two-part series using Prism to show how this game is not fun
59:09
SPEAKER_01: by analyzing it as a mathematical thing.
59:11
SPEAKER_01: Love it.
59:13
SPEAKER_00: Those are, I think, some of the ones that are, like, really popular.
59:16
SPEAKER_01: But there's also, I mean, I could just keep listening.
59:20
SPEAKER_01: There's, like,
59:20
SPEAKER_01: Event B,
59:21
SPEAKER_01: which has, like, been used, I believe, famously in part of the Paris metro system.
59:27
SPEAKER_01: There's like MCRL-2, which I think comes from a Dutch university.
59:32
SPEAKER_01: Himera-X,
59:33
SPEAKER_01: which is mostly used for like robotic control systems,
59:35
SPEAKER_01: but I think that's mostly academic.
59:37
SPEAKER_01: There's like NewSMV, which I think NASA is used for a bunch of stuff.
59:41
SPEAKER_01: I can keep going.
59:43
SPEAKER_01: Then, of course,
59:43
SPEAKER_01: there's all the,
59:44
SPEAKER_01: of course, this is only for specifying like abstract models of systems.
59:47
SPEAKER_01: If you want to talk about verifying code,
59:49
SPEAKER_01: then you've got things like Daphne,
59:51
SPEAKER_01: which is basically something that compiles to like .NET
59:54
SPEAKER_01: and lets you basically write provable code.
59:56
SPEAKER_01: You've got JML for like model checking Java code.
1:00:00
SPEAKER_01: You've got like PrimaC for like checking C. You've got Adaspark.
1:00:05
SPEAKER_01: You've got like,
1:00:06
SPEAKER_01: and you've got Ethereum Provers like Rock and Lean and Isabel, and I can keep going.
1:00:10
SPEAKER_00: I wanted to ask how this property-based testing works.
1:00:16
SPEAKER_00: Relate to formal verification.
1:00:18
SPEAKER_00: And before, let's just like lay out what property-based testing is.
1:00:22
SPEAKER_01: So let's go back to the entire thing with max, right?
1:00:24
SPEAKER_01: Maximum list.
1:00:25
SPEAKER_01: We can define like the specification of max as it is in the list and
1:00:28
SPEAKER_01: for all elements of the list, it is the largest element of that list, right?
1:00:33
SPEAKER_01: I actually have a demo on my computer of doing that.
1:00:36
SPEAKER_01: So let's actually go into this.
1:00:37
SPEAKER_01: So over here in this file that I wrote for my book, plug,
1:00:44
SPEAKER_02: I have
1:00:49
SPEAKER_01: I have basically three variants of max,
1:00:51
SPEAKER_01: a good version which just returns the max of the list,
1:00:54
SPEAKER_01: one that returns the max of the first three,
1:00:55
SPEAKER_01: and the one that returns the max of the absolute value.
1:00:57
SPEAKER_01: This below here is a property test.
1:01:00
SPEAKER_01: What it does is it says,
1:01:02
SPEAKER_01: given a list of integers where each list has at least one integer in it,
1:01:09
SPEAKER_01: the maximum value of that function should be in the list
1:01:13
SPEAKER_01: and all other values should be less than or equal to it.
1:01:16
SPEAKER_01: Yep, clear.
1:01:18
SPEAKER_01: So this basically looks a lot like our formal verification spec, our formal specification spec.
1:01:22
SPEAKER_01: The difference between the formal methods that we do and property testing is that
1:01:27
SPEAKER_01: the formal methods are saying like, okay, can we prove this for every possible list?
1:01:32
SPEAKER_01: And property testing is, well, that's very, very hard.
1:01:36
SPEAKER_01: And as we talked about, very difficult to do in practice.
1:01:39
SPEAKER_01: Can we instead generate a thousand random lists and try all those?
1:01:43
SPEAKER_01: I have it set that way.
1:01:44
SPEAKER_01: It basically has the invalid max, max of first three.
1:01:47
SPEAKER_00: We should be getting errors or it should cast
1:01:50
SPEAKER_02: some errors.
1:01:52
SPEAKER_01: Let's run it.
1:01:56
SPEAKER_01: Let me just run it from the command line.
1:01:57
SPEAKER_01: That's faster.
1:02:02
SPEAKER_02: PyTest, test, max.py.
1:02:08
SPEAKER_02: This is an old machine I mostly bring around for conferences because it's like easy
1:02:11
SPEAKER_02: to just throw on something on here.
1:02:17
SPEAKER_01: So we see over here that it says that this test failed on this line,
1:02:24
SPEAKER_01: that for the list 0001, it is not true that all the values are greater than zero.
1:02:33
SPEAKER_01: This is because, as I said, our bad max only looks at the first three values.
1:02:36
SPEAKER_01: So it found the max was zero, but here the actual max of the list was one.
1:02:41
SPEAKER_01: I broke this down to two subspecs for part of the book where we have testing
1:02:44
SPEAKER_01: that max is the largest element and also that it's in the list.
1:02:48
SPEAKER_00: So that's why one of the tests passes.
1:02:50
SPEAKER_00: I should note, though, that if I believe I run this with a verbose,
1:02:56
SPEAKER_01: what I'm trying to do for this demo is show that it actually does not start with
1:03:00
SPEAKER_01: the...
1:03:01
SPEAKER_01: Largest list,
1:03:02
SPEAKER_01: it actually starts with a much smaller,
1:03:05
SPEAKER_02: with, here we go, if I print max, if I print, then I do it like this, I think.
1:03:19
SPEAKER_02: It tries a lot of edge cases first.
1:03:22
SPEAKER_01: So it's basically trying huge lists, it's trying tiny lists, it's trying empty lists, etc.
1:03:28
SPEAKER_01: And once it has one that fails,
1:03:30
SPEAKER_01: for example,
1:03:30
SPEAKER_01: this value, it starts to shrink it, finding the minimally interesting example.
1:03:35
SPEAKER_01: And that's why this lets us find a bug.
1:03:39
SPEAKER_01: Not just find a bug,
1:03:40
SPEAKER_01: but also find a bug presented in a way that is comprehensive for the average human.
1:03:44
SPEAKER_01: Because I think that it found the original bug with this list,
1:03:46
SPEAKER_01: and I do not think that looking at this, I'm going to know what the problem is.
1:03:49
SPEAKER_01: That's basically property-based testing in a nutshell.
1:03:52
SPEAKER_01: And as you can see,
1:03:52
SPEAKER_01: it is less thorough than formal verification, but it's a lot easier to apply.
1:03:55
SPEAKER_00: So it sounds like it can be a nice middle ground in terms of getting started with it.
1:04:01
SPEAKER_01: And probably just stopping with it,
1:04:02
SPEAKER_01: because I think that I love formal methods,
1:04:05
SPEAKER_01: but I think it's a fairly niche tool for most people.
1:04:08
SPEAKER_01: And I think like property based testing is in general going to be useful for more people.
1:04:13
SPEAKER_00: So speaking of verification in general, today we have AI generating way more code.
1:04:20
SPEAKER_00: We have data to prove this as well, but also day to day.
1:04:23
SPEAKER_00: I see it on myself.
1:04:24
SPEAKER_00: I have AI generate a lot more of my code.
1:04:26
SPEAKER_00: We're getting more code.
1:04:27
SPEAKER_00: Code reviews are, people are, it's hard to pay more attention to this.
1:04:32
SPEAKER_00: So there's a growing number of people saying,
1:04:35
SPEAKER_00: well, maybe we should somehow validate things more.
1:04:38
SPEAKER_00: And there's an idea that keeps coming up on maybe formal verification
1:04:42
SPEAKER_00: or Operator-based testing or some of these things could be more useful.
1:04:45
SPEAKER_00: Do you think this will happen?
1:04:49
SPEAKER_00: Because I see a lot of people talking about this.
1:04:51
SPEAKER_00: I don't really see anyone doing much about it.
1:04:53
SPEAKER_01: I'm definitely seeing more business from people.
1:04:57
SPEAKER_01: My client is people trying to generate specs with AI and then getting
1:05:02
SPEAKER_01: to help work with the spec or find issues with that.
1:05:05
SPEAKER_01: And I'm definitely seeing more people like using property based testing.
1:05:09
SPEAKER_01: I know, for example,
1:05:10
SPEAKER_01: I think Kiro, like
1:05:11
SPEAKER_01: the Amazon spectrum development platform specifically advertises generating property
1:05:15
SPEAKER_01: tests as like one of the key values of it.
1:05:18
SPEAKER_01: And I've been seeing a lot of like papers about generating specs using AI.
1:05:24
SPEAKER_01: I will say this is kind of really exciting because as you saw,
1:05:26
SPEAKER_01: like a lot of the challenge of writing a spec,
1:05:27
SPEAKER_01: not all of it,
1:05:27
SPEAKER_01: but like a lot of it is like rocking your head around like very,
1:05:31
SPEAKER_01: very technical syntax and like semantics.
1:05:36
SPEAKER_01: That said,
1:05:37
SPEAKER_01: I've been doing a lot of experience with this myself,
1:05:39
SPEAKER_01: and I think the one thing AI is extremely bad at,
1:05:42
SPEAKER_01: as of March,
1:05:44
SPEAKER_01: I know that Claw just released a new Claw 4.8, so maybe this is all out the window.
1:05:47
SPEAKER_01: It changes every month.
1:05:49
SPEAKER_01: It is very bad at coming up with properties.
1:05:52
SPEAKER_00: It is very bad at that.
1:05:53
SPEAKER_00: What does coming up with properties mean?
1:05:55
SPEAKER_00: Is it writing the actual form of verification part?
1:05:58
SPEAKER_01: Yeah, so like if you give it properties and like a spec,
1:06:00
SPEAKER_01: it can tell you like, hey, we're going to fix the spec, make these properties pass.
1:06:04
SPEAKER_01: That's fine.
1:06:05
SPEAKER_01: But if you basically tell it,
1:06:06
SPEAKER_01: here's the spec,
1:06:06
SPEAKER_01: also come up with the properties of the spec,
1:06:08
SPEAKER_01: it'll be like, okay,
1:06:09
SPEAKER_01: so one of the properties I'm going to specify is that either P is true
1:06:13
SPEAKER_01: or not P is true.
1:06:14
SPEAKER_01: And then you're like, that's just always true.
1:06:15
SPEAKER_01: And it's like, wow, I verified it.
1:06:16
SPEAKER_01: Amazing.
1:06:17
SPEAKER_01: I'm so good at this.
1:06:18
SPEAKER_01: Especially when you deal with what's called liveness properties,
1:06:20
SPEAKER_01: properties about how like a system can evolve over a long period of time.
1:06:24
SPEAKER_01: It just...
1:06:26
SPEAKER_01: It's hard to put down.
1:06:27
SPEAKER_01: It's just not good at that yet.
1:06:28
SPEAKER_01: And often I find my clients,
1:06:30
SPEAKER_01: I have to tell them like,
1:06:32
SPEAKER_01: it's doing a good job at generating the actual design,
1:06:34
SPEAKER_01: but actually expressing what the design is supposed to do.
1:06:36
SPEAKER_01: It cannot do that yet.
1:06:38
SPEAKER_01: You have to do that part yourself.
1:06:39
SPEAKER_00: It's interesting because there's a blog post that I'll also link in the show notes
1:06:43
SPEAKER_00: from a year ago in March, 2025, titled The Coming Revolution in Distributed Systems.
1:06:48
SPEAKER_00: And this was an engineer working on GitHub's co-pilot team.
1:06:51
SPEAKER_00: And this person wrote how AI autonomously produced precise TLA plus specifications
1:06:56
SPEAKER_00: from Azure Storage's production source code and it uncovered a subtle race condition
1:07:01
SPEAKER_00: that had evaded traditional code reviews.
1:07:03
SPEAKER_00: And then this person was very enthusiastic and saying, well, this could be a revolution.
1:07:07
SPEAKER_00: AI could just generate TLA plus from specification like it did with Azure.
1:07:12
SPEAKER_00: This was a year ago and I haven't heard much on any of this,
1:07:16
SPEAKER_00: even though the models were not as great.
1:07:19
SPEAKER_00: What have you seen in this area?
1:07:20
SPEAKER_01: So actually the same person,
1:07:21
SPEAKER_01: Chang Huang,
1:07:22
SPEAKER_01: did come up with a tool called Lamport Agent where they demonstrated using this
1:07:26
SPEAKER_01: to specify parts of crack, I think it's called, part of DC's crack.
1:07:31
SPEAKER_01: I'm going to link both those in the thing.
1:07:34
SPEAKER_01: Here's my response.
1:07:35
SPEAKER_01: I was writing about this and then the thing that they did.
1:07:38
SPEAKER_01: He seemed to be a lot more successful than I was generating properties.
1:07:43
SPEAKER_01: But one,
1:07:44
SPEAKER_01: at least the example that he showcased in his later piece, one,
1:07:47
SPEAKER_01: he's an expert specifier who already knows how to do this stuff on his own without
1:07:51
SPEAKER_01: the LLM.
1:07:51
SPEAKER_01: He's the main expert.
1:07:52
SPEAKER_01: Yeah, he knows how to get the results out of it.
1:07:54
SPEAKER_01: As a general thing we've seen, like,
1:07:56
SPEAKER_01: To get good results, you have to already know how to get good results without it.
1:07:59
SPEAKER_01: It just helps you get good results faster.
1:08:00
SPEAKER_01: And also,
1:08:02
SPEAKER_01: one of the systems that he was able to create the complicated properties for
1:08:04
SPEAKER_01: in TLA Plus already had a sophisticated spec written in P.
1:08:08
SPEAKER_01: So I don't know how much that's relevant here.
1:08:09
SPEAKER_01: Maybe it read that and it cheated.
1:08:11
SPEAKER_01: Maybe that was like fine.
1:08:13
SPEAKER_01: I don't know.
1:08:14
SPEAKER_00: But we do see this a lot where when you're an expert in a domain,
1:08:17
SPEAKER_00: it may that be software engineering or like backend or mobile,
1:08:21
SPEAKER_00: AI works better for you.
1:08:22
SPEAKER_01: Then there's also this one interesting person,
1:08:24
SPEAKER_01: Claudia Colley did write a write-up because she just did about a multi-year project
1:08:28
SPEAKER_01: and using formal methamphetamine,
1:08:30
SPEAKER_01: the big Chinese cloud provider,
1:08:31
SPEAKER_01: where she talks about how in between her working on this paper and
1:08:39
SPEAKER_01: the time she got published,
1:08:40
SPEAKER_01: She got really sophisticated data on how long it took people to write formal methods
1:08:44
SPEAKER_01: at this one company.
1:08:45
SPEAKER_01: And then LLMs basically just compressed the scale by the time she actually had the paper out.
1:08:49
SPEAKER_01: So I think people are seeing like more use from like formal methods,
1:08:52
SPEAKER_01: but it seems people with the most success right now are specifiers who are using it
1:08:56
SPEAKER_01: to amplify their ability to specify.
1:08:58
SPEAKER_01: And we haven't yet really seen, I mean,
1:09:00
SPEAKER_01: people post acronyms all the time,
1:09:01
SPEAKER_01: like people who they had a AI write the whole spec for them,
1:09:05
SPEAKER_01: but those tend to not be very good specs.
1:09:07
SPEAKER_00: And what's your take on, again,
1:09:08
SPEAKER_00: I've heard some voices say
1:09:10
SPEAKER_00: that AI might make formal verification go mainstream based on this.
1:09:14
SPEAKER_00: But outside of the,
1:09:16
SPEAKER_00: do you see any movement outside of this niche of people who already know how
1:09:20
SPEAKER_00: to do formal verification?
1:09:21
SPEAKER_01: I think it is making it more popular.
1:09:23
SPEAKER_01: I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular.
1:09:26
SPEAKER_01: It's bringing it from maybe like 0.1% to 0.3%.
1:09:30
SPEAKER_00: Which is huge.
1:09:31
SPEAKER_00: There's also this thinking that I've read.
1:09:35
SPEAKER_00: Actually,
1:09:36
SPEAKER_00: in June 2025,
1:09:38
SPEAKER_00: in your newsletter, you said that AI is a specification force multiplier.
1:09:42
SPEAKER_00: And now, of course, we see that LMS are bad at vibing specifications.
1:09:47
SPEAKER_00: What changed between that time where you saw that they were like a year ago,
1:09:52
SPEAKER_00: they were pretty decent at doing it or they had science and now we have
1:09:56
SPEAKER_00: So what I wrote
1:09:58
SPEAKER_01: that it was really good at was fixing syntax errors,
1:09:59
SPEAKER_01: which is really big because that's often trips people up.
1:10:02
SPEAKER_01: It's good at understanding error traces,
1:10:04
SPEAKER_01: which is huge because being able to take like a 35 step error trace and turn that
1:10:07
SPEAKER_01: into like two paragraphs of English text, major improvement.
1:10:11
SPEAKER_01: Good at boilerplate,
1:10:12
SPEAKER_01: like mass changes to like a bunch of small things like updating like boilerplate
1:10:17
SPEAKER_01: and It's okay at writing properties from a very precise description.
1:10:23
SPEAKER_01: It's bad at fixing specs and it's real bad at providing properties for specs.
1:10:27
SPEAKER_01: Ha, I'm still consistent.
1:10:29
SPEAKER_01: So I think I called it early back then that it like is really bad.
1:10:33
SPEAKER_01: It's good at translating properties from like English,
1:10:34
SPEAKER_01: precise English into a spec, but it's bad at coming up with properties on its own.
1:10:38
SPEAKER_01: Everything I got back was trivial, uninteresting or too coupled with the implementation details.
1:10:42
SPEAKER_01: So I think ultimately what I'm going to say is that like,
1:10:44
SPEAKER_01: I think it has a lot of potential to improve things.
1:10:46
SPEAKER_01: But even back then in 2025,
1:10:49
SPEAKER_01: I was noticing that I was really bad at this one thing,
1:10:51
SPEAKER_01: that it continues to be bad as of March of this year.
1:10:54
SPEAKER_00: So then how much do you think you really need to know formal methods to be able
1:10:58
SPEAKER_00: to use LLMs to help you at all?
1:11:00
SPEAKER_00: You need to get the basics in place, likely.
1:11:03
SPEAKER_01: I think getting the basics in place is really valuable here, right?
1:11:06
SPEAKER_01: Because for one, I mean,
1:11:08
SPEAKER_01: even discounting,
1:11:09
SPEAKER_01: like being able to write the properties and all that,
1:11:11
SPEAKER_01: you need to be able to tell when the AI is doing something wrong, right?
1:11:14
SPEAKER_01: And if you don't know the basics, you can't really do that very well.
1:11:17
SPEAKER_00: In your book,
1:11:18
SPEAKER_00: Logic for Programmers,
1:11:19
SPEAKER_00: you argue that formal logic is probably one of the most useful parts
1:11:24
SPEAKER_00: for day-to-day engineering.
1:11:27
SPEAKER_00: Why is this?
1:11:28
SPEAKER_01: First of all, I'm honored that you've read my book, or at least the early drafts.
1:11:31
SPEAKER_01: I mean, the official answer is because logic teaches us to work with like booleans
1:11:35
SPEAKER_01: and statements.
1:11:37
SPEAKER_01: What we learn in elementary school, how to work with numbers, right?
1:11:41
SPEAKER_01: Essentially,
1:11:41
SPEAKER_01: there's not a whole lot of difference between knowing that One plus one is two,
1:11:46
SPEAKER_01: and true and true is true.
1:11:47
SPEAKER_01: It's still the manipulation of values.
1:11:49
SPEAKER_01: And it happens that Booleans are so important to software engineering
1:11:53
SPEAKER_01: that having some formal grounding in that is very handy,
1:11:56
SPEAKER_01: especially when we are not taught that in school for the most part.
1:11:59
SPEAKER_01: The other answer is that I've just...
1:12:03
SPEAKER_01: I'm learning logic and getting better logic and teaching logic a lot as part of teaching TLA+.
1:12:08
SPEAKER_01: I'm just finding more and more applications where I'm like,
1:12:10
SPEAKER_01: oh, because of logic, I can do this one thing.
1:12:12
SPEAKER_01: And I find that people who don't have that background struggle through that one thing.
1:12:16
SPEAKER_01: I guess I'm saying that empirically, logic keeps coming up as a useful form of math.
1:12:21
SPEAKER_00: And if I'm a software engineer and I work on complicated systems,
1:12:24
SPEAKER_00: distributed systems,
1:12:25
SPEAKER_00: what techniques would you recommend that I look into to harden these systems?
1:12:30
SPEAKER_00: We can assume that I'm already doing...
1:12:31
SPEAKER_00: I'm going to just completely go 90 degrees here and recommend this book
1:12:34
SPEAKER_00: by Nancy Levison called Engineering a Safer World.
1:12:57
SPEAKER_01: She was an aeronautics engineer
1:12:58
SPEAKER_01: who investigated things like Etheric-25 radiation case and like
1:13:03
SPEAKER_01: the Columbia disaster.
1:13:04
SPEAKER_01: And she was really fascinated in how like systems have been accidents
1:13:10
SPEAKER_01: and systems happen, like why accidents could happen in complicated systems.
1:13:14
SPEAKER_01: And I found her writing on this to be incredibly insightful and incredibly valuable
1:13:19
SPEAKER_01: in understanding how these systems can break.
1:13:21
SPEAKER_01: So that's the thing at first I'd recommend is checking out that book.
1:13:23
SPEAKER_00: Looking ahead for the industry a year ago,
1:13:25
SPEAKER_00: you wrote a post where you shared some of the uncertainties and anxieties.
1:13:30
SPEAKER_00: It was a longer post.
1:13:31
SPEAKER_00: It started with how Vitecoding will be never good as software engineering,
1:13:34
SPEAKER_00: experienced software engineers, and you wrote six different things.
1:13:37
SPEAKER_00: Can we read through them and just reflect on how you feel about them,
1:13:41
SPEAKER_00: what you think might have changed,
1:13:43
SPEAKER_00: and maybe talk about what potential new anxieties we have because there's
1:13:46
SPEAKER_00: so much change going on, that's for sure.
1:13:47
SPEAKER_01: The way I sort of think about it is that
1:13:48
SPEAKER_01: the next five years keep being rewritten every few months.
1:13:51
SPEAKER_00: Right?
1:13:52
SPEAKER_01: Yeah.
1:13:52
SPEAKER_01: So I wrote, the following can all be true.
1:13:55
SPEAKER_01: One, vibe coders will never be good at software engineering as an experienced software engineer.
1:13:58
SPEAKER_01: Probably true.
1:13:59
SPEAKER_01: I mean, if you don't have the basics, you can't really.
1:14:02
SPEAKER_00: It feels true.
1:14:03
SPEAKER_00: I even see it on myself when I try to build a software in a domain I'm not an expert
1:14:07
SPEAKER_00: in, like a game, and it's an absolute just vibe coded mess.
1:14:11
SPEAKER_01: Yeah.
1:14:12
SPEAKER_01: Elements can significantly augment a professional software engineer's ability
1:14:15
SPEAKER_01: to quickly
1:14:16
SPEAKER_00: write high quality software.
1:14:17
SPEAKER_00: I think also true.
1:14:19
SPEAKER_01: I mean, even if you don't have it writing a single line of code,
1:14:21
SPEAKER_01: just being able to be like, okay, what's this bug?
1:14:22
SPEAKER_01: Where's the bug?
1:14:24
SPEAKER_01: Or like, hey, what library should I look into to solve this problem?
1:14:27
SPEAKER_00: And I think we're starting to see or starting to recognize that engineers
1:14:31
SPEAKER_00: who have really deep knowledge are so much more efficient.
1:14:35
SPEAKER_00: And the ones who embrace these tools and figure out how to control them and not them
1:14:39
SPEAKER_00: to control, you know, like their anxiety or whatnot, they get a lot done.
1:14:43
SPEAKER_00: Absolutely.
1:14:44
SPEAKER_01: Elements will cause many software developers to lose their jobs.
1:14:47
SPEAKER_01: I don't know.
1:14:47
SPEAKER_01: That's a hard one to pin down because like,
1:14:50
SPEAKER_01: I mean, one, the software engineering, at least in the US, is starting to recover.
1:14:53
SPEAKER_01: Like we're starting to see more jobs open up for software development.
1:14:56
SPEAKER_01: So it's hard to tell how much of like the loss of the past few years was AI versus
1:15:01
SPEAKER_00: the end of like zero interest rate policy and like the post-COVID crash.
1:15:06
SPEAKER_01: And I think it's more the latter.
1:15:07
SPEAKER_01: But like, again, LMs are still getting better.
1:15:09
SPEAKER_01: Maybe they're going to cause job losses in the future.
1:15:12
SPEAKER_00: Yeah, this is a notable question.
1:15:13
SPEAKER_00: The data that we had in The Pragmatic Engineer,
1:15:15
SPEAKER_00: it did show that We are seeing overall more software engineering openings in the US,
1:15:19
SPEAKER_00: in Germany and France.
1:15:20
SPEAKER_00: They're declining a little bit at the same time.
1:15:23
SPEAKER_00: And there seems to be a big shift on who is being hired and the skill set.
1:15:27
SPEAKER_00: So now AI engineering is increasingly spreading to more software engineering fields,
1:15:32
SPEAKER_00: not all of them.
1:15:33
SPEAKER_00: And we're seeing a decrease in,
1:15:34
SPEAKER_00: for example, front-end engineering hiring, mobile engineering hiring.
1:15:36
SPEAKER_00: So I think the shape is changing, but it's always changed in the past.
1:15:39
SPEAKER_00: If you think about 20 years ago,
1:15:41
SPEAKER_00: The most in-demand engineer was a Java engineer,
1:15:43
SPEAKER_00: like Java specifically, like don't care.
1:15:46
SPEAKER_00: 10 years of Java experience required and that's changed.
1:15:49
SPEAKER_00: Okay, then we'll put up new jobs for many possibly far more money software developers.
1:15:53
SPEAKER_01: I think that's also true.
1:15:54
SPEAKER_01: I think when you basically need one developer to make your product as opposed
1:15:58
SPEAKER_01: to five, you're more likely to hire one developer, right?
1:16:00
SPEAKER_00: That's been true, yeah.
1:16:01
SPEAKER_01: The software jobs that LLMs open up will be lower paid and lower procedures in
1:16:05
SPEAKER_01: the heights of the 2008 to 22 tech era.
1:16:07
SPEAKER_01: And that's the thing that scares me the most is that As mentioned,
1:16:11
SPEAKER_01: I decided to leave a field and just become a techie.
1:16:13
SPEAKER_01: And I was able to do that.
1:16:15
SPEAKER_01: And I was able to get a well-paying job that led to me
1:16:18
SPEAKER_01: to now full-time mathematically prove systems correct.
1:16:21
SPEAKER_01: That's crazy.
1:16:22
SPEAKER_01: What other field can somebody just go like,
1:16:24
SPEAKER_01: what other engineering field can somebody go like,
1:16:25
SPEAKER_01: I want to be an engineer and just walk straight into it?
1:16:27
SPEAKER_01: What other field is going to send people to Budapest from the US to give a talk for 45 minutes?
1:16:32
SPEAKER_01: Like, it is really precious and magical what we have here.
1:16:36
SPEAKER_01: And I'm afraid of losing that.
1:16:38
SPEAKER_01: I'm afraid of a place where it just becomes like any other white-collar job
1:16:44
SPEAKER_01: where you get two weeks paid vacation every year and two days off sick.
1:16:48
SPEAKER_01: And I don't want to lose that.
1:16:50
SPEAKER_00: Are we saying we're afraid
1:16:51
SPEAKER_00: that software engineering might become just like every other engineering job?
1:16:55
SPEAKER_00: Yeah.
1:16:56
SPEAKER_00: Because that is the reality of a lot of engineering jobs.
1:16:58
SPEAKER_00: We do have a privilege.
1:16:59
SPEAKER_00: I don't think we talked about it when we compared the rest of engineering.
1:17:02
SPEAKER_00: We have massive privilege.
1:17:03
SPEAKER_01: Yes, we have a huge privilege and I don't want to lose that.
1:17:05
SPEAKER_01: And I mean,
1:17:06
SPEAKER_01: it would be nice if everybody else got the same things we are,
1:17:08
SPEAKER_01: but I don't want to like equalize us by losing what makes software engineering
1:17:11
SPEAKER_01: so magical and precious.
1:17:14
SPEAKER_00: Yeah.
1:17:15
SPEAKER_00: So this is a worry.
1:17:16
SPEAKER_01: Yeah, that's my that's my fear.
1:17:17
SPEAKER_00: And then number six.
1:17:18
SPEAKER_01: There will still be high-paid professional software engineering jobs,
1:17:21
SPEAKER_01: but they will be rare, more competitive, and less developer-friendly.
1:17:24
SPEAKER_00: I'm afraid we're seeing some of this already.
1:17:27
SPEAKER_00: I wonder if this is inevitable.
1:17:30
SPEAKER_00: I also see it in some other industries, for example, with investment banking.
1:17:34
SPEAKER_00: The traders used to be, many of them, very highly paid, highly respected.
1:17:38
SPEAKER_00: There are now fewer of them, still highly paid, highly respected.
1:17:41
SPEAKER_00: It's hard to get into them.
1:17:42
SPEAKER_01: Yeah.
1:17:43
SPEAKER_01: I mean, I think most jobs do ossify over time.
1:17:46
SPEAKER_01: As like the centers are set and more people enter them,
1:17:49
SPEAKER_01: software engineer,
1:17:50
SPEAKER_01: I think for a longer period of time was able to like get away from that.
1:17:54
SPEAKER_00: And then you close your prediction with these lines a year ago.
1:17:59
SPEAKER_01: I predict that in the next 10 years,
1:18:00
SPEAKER_01: software development will survive,
1:18:01
SPEAKER_01: but it will become like any other white collar professional work.
1:18:04
SPEAKER_01: No more $200,000 salaries, a little vacation or incredible employee bargaining power.
1:18:09
SPEAKER_01: I feel sad that we'll lose something so magical, but I guess it couldn't have lasted forever.
1:18:13
SPEAKER_01: Automation comes for all of us, even us automators.
1:18:15
SPEAKER_01: Here's a good way of ending this.
1:18:18
SPEAKER_01: If we start with automation comes for all of us, even us automators.
1:18:20
SPEAKER_01: On one hand, I feel like I'm losing something really special.
1:18:22
SPEAKER_00: On the other hand,
1:18:23
SPEAKER_00: a doctor friend of
1:18:23
SPEAKER_01: mine came to me a few months back and was like, hey,
1:18:26
SPEAKER_01: we managed to Create a new shift scheduling platform for our hospital
1:18:30
SPEAKER_01: to trade shifts that really saved us a lot of time and made all of us nurses
1:18:34
SPEAKER_01: and doctors so much happier.
1:18:35
SPEAKER_01: And I was able to just vibe it out.
1:18:37
SPEAKER_01: I don't know any kind of code, but AI let me do this.
1:18:39
SPEAKER_01: And I'm like, wow, it really is helping you and your hospital make your life better.
1:18:44
SPEAKER_01: And it feels so weird to balance my needs as a professional software developer
1:18:49
SPEAKER_01: with his needs as a doctor.
1:18:51
SPEAKER_01: Who matters more, my cushy job or his job?
1:18:54
SPEAKER_01: I don't know.
1:18:55
SPEAKER_01: And we're going to all find this out in the next 10 years, I guess.
1:18:58
SPEAKER_00: Grady Bush told me that this time reminds him of the time in the late 1960s
1:19:03
SPEAKER_00: and early 1970s where people could purchase computers and start to hack with them.
1:19:09
SPEAKER_00: And he said it was a magical time because teachers and people who had nothing to do
1:19:12
SPEAKER_00: with software...
1:19:13
SPEAKER_00: Saved up and started to just hack around and it democratized it.
1:19:18
SPEAKER_00: And I feel this is the first time I'm also feeling like this other person
1:19:22
SPEAKER_00: the gym told me that they're vibing something together.
1:19:25
SPEAKER_00: It feels it's opening up the field.
1:19:26
SPEAKER_00: And if anything, a lot more people are realizing, oh, software is cool.
1:19:30
SPEAKER_00: I can do it.
1:19:31
SPEAKER_00: And now they're trying to learn the hard parts of software engineering eventually.
1:19:34
SPEAKER_01: Did you ever read up Clay Shirky's essay, Situated Software?
1:19:36
SPEAKER_01: No.
1:19:36
SPEAKER_01: Basically what it is,
1:19:37
SPEAKER_01: is that this person was talking about how they think like The most important,
1:19:46
SPEAKER_01: the vast majority of software should be made for like three people or like a family
1:19:50
SPEAKER_01: or community or like one school.
1:19:52
SPEAKER_01: And up until now,
1:19:53
SPEAKER_01: that like could only really happen if one of those people in that family,
1:19:56
SPEAKER_01: that community or that school was like really, really into computers.
1:20:00
SPEAKER_01: But now it's possible for everybody to have situated software and computers.
1:20:04
SPEAKER_01: That, again,
1:20:04
SPEAKER_01: is going to change the world in some strange and some terrifying
1:20:08
SPEAKER_01: and some exciting ways.
1:20:09
SPEAKER_00: It's exciting.
1:20:10
SPEAKER_00: As closing,
1:20:11
SPEAKER_00: what are books,
1:20:12
SPEAKER_00: a few books that you could recommend that you have enjoyed or made an impact on you?
1:20:17
SPEAKER_01: Oh boy, let's just leave this just for this into just software books, okay?
1:20:20
SPEAKER_01: Because otherwise we're going to be here for like a month.
1:20:22
SPEAKER_01: So there's three books that I really love in software that I think of as like
1:20:25
SPEAKER_01: the books that have influenced me so much.
1:20:28
SPEAKER_01: The first one I think I mentioned in the interview was Nancy Levison's Engineering
1:20:31
SPEAKER_01: a Safer World.
1:20:32
SPEAKER_01: I believe that's actually free online.
1:20:34
SPEAKER_01: The second book is called Data and Reality by Bill Kent.
1:20:38
SPEAKER_01: And this one is actually hard to find because it was republished in 2000, I think, 11.
1:20:43
SPEAKER_01: But the republisher changed the book.
1:20:45
SPEAKER_01: So the last good edition is the second edition,
1:20:47
SPEAKER_01: which can be found like in dark corners of the internet online is actually kind
1:20:50
SPEAKER_01: of hard.
1:20:50
SPEAKER_01: But like it is basically by this like famous database designer who like worked
1:20:54
SPEAKER_01: on like IBM databases who was just asking like, What is data?
1:20:59
SPEAKER_01: What does it mean for something to have an identity?
1:21:00
SPEAKER_01: What does it mean for something to have oneness?
1:21:01
SPEAKER_01: If we talk about a book, is that the book, the physical copy?
1:21:05
SPEAKER_01: Is that the series?
1:21:06
SPEAKER_01: Is that an edition?
1:21:08
SPEAKER_01: And it's just an entire book about these questions about what data is
1:21:11
SPEAKER_01: and how we need to represent it.
1:21:13
SPEAKER_01: He ends it by saying that data isn't reality.
1:21:15
SPEAKER_01: It is our view of reality for our useful purpose.
1:21:18
SPEAKER_01: Incredible book.
1:21:19
SPEAKER_01: It totally changed how I think about things.
1:21:23
SPEAKER_01: The last book is called Debugging, The Nine Simple Rules by David Agans.
1:21:28
SPEAKER_01: And it's literally just like a book of war stories about debugging and like basic principles.
1:21:33
SPEAKER_01: But this is the book I give to every junior engineer
1:21:36
SPEAKER_01: because I think like nobody ever really talks about debugging as like
1:21:40
SPEAKER_01: a discipline outside of like basic heuristics.
1:21:42
SPEAKER_01: And this is like just at least something that's trying to do that.
1:21:44
SPEAKER_01: And having something is better than nothing in this category.
1:21:47
SPEAKER_01: So really good book.
1:21:48
SPEAKER_01: And I think it's like $10 for a used copy.
1:21:51
SPEAKER_01: So like anybody can just get one.
1:21:52
SPEAKER_01: It's great.
1:21:53
SPEAKER_01: Those, I think, are the three most useful books for software engineers.
1:21:55
SPEAKER_01: If you want to talk about other books, I can keep going.
1:21:59
SPEAKER_00: This is great.
1:22:00
SPEAKER_00: Well, hello.
1:22:00
SPEAKER_00: This was very educational, and I found it fascinating.
1:22:04
SPEAKER_00: Thank you.
1:22:05
SPEAKER_01: Thank you.
1:22:06
SPEAKER_00: I really enjoyed this conversation,
1:22:08
SPEAKER_00: especially the demos where Hillel showed tools like TLA+,
1:22:11
SPEAKER_00: Alloy, or Hypothesis, and how they can catch bugs.
1:22:14
SPEAKER_00: By the end of the conversation,
1:22:15
SPEAKER_00: I'm starting to understand more why it's not likely
1:22:18
SPEAKER_00: that formal verification will go mainstream, even with AI.
1:22:21
SPEAKER_00: I mean, these tools feel very rigid for the real world.
1:22:24
SPEAKER_00: For specific parts of a system that you can model mathematically,
1:22:27
SPEAKER_00: like state spaces, sure,
1:22:29
SPEAKER_00: they can work,
1:22:30
SPEAKER_00: but for everyday programs,
1:22:31
SPEAKER_00: it just feels like it will be a bit pointless to create TLA-plus specifications.
1:22:36
SPEAKER_00: One thing that I was also thinking about is how Hill talked
1:22:39
SPEAKER_00: about why he thinks we're not good at catching concurrency bugs.
1:22:43
SPEAKER_00: And it's because we don't have much practice with them.
1:22:45
SPEAKER_00: As a developer, you're lucky to debug a concurrency bug once every few years.
1:22:50
SPEAKER_00: So of course, you won't be able to build expertise this way.
1:22:53
SPEAKER_00: This is also similar to how most engineers are bad at migrations
1:22:56
SPEAKER_00: because most devs only ever do one or two migrations over several years.
1:23:00
SPEAKER_00: But if you're an engineer who does a bunch of migrations,
1:23:02
SPEAKER_00: you're going to be really good at them.
1:23:04
SPEAKER_00: Same thing if you're working on systems with concurrency issues and you become
1:23:07
SPEAKER_00: an expert in this.
1:23:08
SPEAKER_00: I also found it fascinating how other engineering fields have similarities
1:23:11
SPEAKER_00: with software engineering,
1:23:12
SPEAKER_00: like how mining engineers had their own agile revolution in the 1960s,
1:23:17
SPEAKER_00: and how all engineers hate the concept of waterfall.
1:23:19
SPEAKER_00: Plus, it was amusing to hear how source control is kind of an envy
1:23:22
SPEAKER_00: from other engineering fields that we,
1:23:23
SPEAKER_00: software engineers have, but not many others do.
1:23:26
SPEAKER_00: Check out the show notes for our related deep dives on distributed systems
1:23:29
SPEAKER_00: and tech depth that go into more detail into the topics that we talked about today.
1:23:33
SPEAKER_00: And if you've enjoyed this podcast,
1:23:34
SPEAKER_00: please do subscribe on your favorite podcast platform and on YouTube.
1:23:37
SPEAKER_00: A special thank you if you also leave a rating on the show.
1:23:40
SPEAKER_00: Thanks, and see you in the next one.