Hillel Wayne: Let's talk about formal methods. There's some sort of implicit mechanism in your brain that can see that and know what the function is supposed to do. So step one of what I do with formal methods is asking can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to actually be doing and write that down in a way that can be shown to anybody?

Host: Why are we not doing formal testing for everything?

Hillel Wayne: When you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. the imperative program you're right that we'll get 99% of the time is probably good enough to use in almost all cases.

Host: One story I've heard and I think you might have been involved is AWS using TA plus.

Host: They talked about how a couple of people in the company were interested learned TA plus and another language called Plus Scout and applied it to aspects of the Dynamo DB and S3 storage systems. In doing so, they were able to find fairly complicated bugs that could potentially lose data. we have AI generating way more code maybe for more verification or property based testing could be more useful. Do you think this will happen?

Hillel Wayne: I've been doing a lot of experience in this myself and I think the one thing AI is extremely bad at. There's a popular theory going around that AI will finally make formal verification go mainstream because when machines write the code, humans will need mathematical proof that is correct.

Host: Today I'm talking with one of the best people to respond to this, Hill Wayne, a formal methods consultant. He taught TLA plus a popular formal specifications language across the industry, wrote the book logic for programmers and will soon be joining antithesis. In today's conversation, we discuss the crossover project. Hill's research interviewing 15 plus traditional engineers to answer the question, can software engineers also be considered real engineers? How AWS used TA plus? an overview of how Amazon found a rare bug inside of Dynamo DB using this formal specifications language, a deep dive into property based testing and why this is a middle ground that most engineers should probably adopt and many more. If you want to understand more about formal verification and get a sense of whether this approach could go mainstream with AI, this episode is for you. In today's episode, we'll get to the question, does it make sense to use formal methods to verify AI written code? As a spoiler, the answer will be proper formal methods are an overkill for this, but lightweight formal methods can actually be helpful. This is where I need to mention our presenting sponsor and antithesis verifies your systems correctness by running your whole system in hostile simulation and finding bugs. It does this by using an approach called deterministic simulation testing or DST which AWS distinguished engineer Mark Burker and Ankor Desai have described as lightweight formal methods. Setting aside in synthesis for a minute, if you as an engineer want to get more serious in verifying that your system works as intended, your best bet would be to use lightweight formal methods. Now back to antithesis. Antithesis is turbocharges testing by running your whole system under aggressive fault injection. Imagine antithesis as hundreds or thousands of versions of the Mario game running. Each instance aggressively trying to break the game with increasingly weird input combinations. With antithesis, you can specify properties at the whole system level and antithesis will actively try to disprove them. So you can be confident that if your system holds up in antithesis, it will hold up in production. There's good reason teams like Jane Street, Fly.io and the CCD community rely on antithesis. Head to antithesis.com/pragmatic to learn more. So hello, welcome to the podcast.

Hillel Wayne: Thank you so much. I'm really excited to be here.

Host: It's so nice to have you here. I was curious, you're very well known for for meth methods, for programming, for for logic, for all of these topics, but how did you get into tech?

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

Host: The first time I came across your writing because you you you write a blog a pretty regular one and I I really enjoy your writing. The first time was with the crossover project. This was a project where you attempted to answer are we as software engineers actually engineers?

Hillel Wayne: Yes.

Host: Can we talk about this project?

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

Host: Can can we go a little bit into it?

Hillel Wayne: So, as I started talking to the first people, I realized that this was a much deeper project than I ever expected. And I decided I needed to have as comprehensive a look at traditional engineering as I could possibly get. There are many kinds of engineering. There's not just building bridges, but there's designing circuits. There's figuring out chemical processes. There's industrial engineering, which is figuring out the layouts of factories and how we organize kinds of labor. There's just so many different kinds. And I wanted to see every single kind's view into what engineering looked like to compare them all to software which when you think about it when we say like oh software isn't like building a bridge maybe it isn't but is it like designing a circuit is like figuring out a chemical flow maybe those are much more closer to the kinds of engineering we do I needed to know I think in the end I talked to about 15 or 20 people in total across about six or seven different fields

Host: and what were the similarities that you found that software engineering has with either specific types of engineering ing or across

If I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall.

No way.

Core tension of engineering is between how expensive it is to make a mistake and how quickly you can iterate. The faster you can iterate, the less planning you need to do before you iterate. And the more expensive it is, the more planning you need to do. That's why for example when you're building a building where you can't build it multiple times and see what happens you have to do a lot of planning up front but even then you are looking for ways to iterate on the plan you do things like build scale models you use software to simulate the building you do CAD models etc and in other fields like in for example electrical engineering you have the ability to come up with a design test it and then throw it to the fab and get something back so they will iterate a lot more than civil engineering does.

Interesting enough I heard the term smoke test originated from electrical engineering. Actually,

I did not look into that, but I could believe it.

Yeah, apparently it's when you have a test circuit and you just hook it up and if it smokes, it's already bad. That is very interesting. So, even within engineering, when we say traditional engineering, there's just layers of engineering or differences, right?

Layers of iteration. I'd say one of the first people I talked to was actually a mining engineer. He designed mines deep underground to make sure that they were stable and didn't leak toxic chemicals. And the first thing he pointed out to me was that they had their agile revolution in 1960. They called it, I believe, the vianese tunneling method as a way of really quickly iterating through building a mine and tunneling through rock. Basically making the change as fast as they could, seeing how the rest of the system reacted to it and then course correcting based on that.

Okay. So I guess we all hate waterfall.

We all hate waterfall, or the idea of waterfall.

Yeah. What are some of the interesting differences that you came across either where engineering is ahead of us or traditional engineering does have things on us which you were hoping to find or places where actually software engineering is ahead in some ways.

There's both differences in how we practice it but also differences in the shape of our material because every engineering concerns a different material. They have different constraints. While it's true that everybody tries to iterate as fast as they can, often turning to software to do that, software is the best at it. The best comparison is chemical engineering where I talked to people saying that they would set up their experiment, run it overnight and get the results the next day and that was fast. With us, we can basically press F11 and get the result, right? And that allows us to basically iterate much faster than even those fields can. I think we all kind of know this. One thing that we might not realize as software engineers is that our work is a lot more consistent than other fields. The example I always do sometimes because I've given a talk about this is I would pull out a CPU chip or a stick of RAM and I'd say hey here's the spec sheet and if you look at the spec sheet it says this resistor has a resistance that is within 20% of 100 ohms as long as you keep it between 20 and 50° centigrade. So they're basically saying that if they make a thousand of these, there's going to be a variance of 20% across all 10,000. And the only way to know is to test them. And then if you run it for too long or you heat it up too much, it's going to change again. With software, assuming no CPU bugs or anything like that, the same program if it runs on this computer, it'll run on your computer exact same. Sort this list the exact same with the sorting algorithm.

Does this also mean that we might not account for variability as much as other engineering disciplines do?

I'd say so. The variation we have to deal with is kind of our own making, right? We're basically saying, okay, we've got all these different systems, all these different APIs versus other people like we have all these different chipsets. We've got all these different ports or sizes, but also if you happen to touch an iron screw to a tungsten screw, they're going to cause corrosion between the two of them. And also, some of your screws are a little bit bigger than others and some are a little bit smaller than others, or a bit longer etc.

And how did you see the similarities or differences of software engineers for example often interact with customers with end users who use the software in other engineering fields is this also a thing where as an engineer you will talk or know your customer or just not knowing them at all.

I think it depends because different engineers I talk to had different experiences. Some said that they felt that with software they felt much closer to the customer, with other ones they said they felt much further. So I think it's hard to really tell there.

One thing I remember vividly is a difference that you pointed out which was very different and almost makes software engineering a bit higher status or a better place is open source the concept of open source.

Yes. So that is one thing that seems very special about software versus any other field. Like the reason I'm here in Hungary right now with you is because I'm going to be speaking at Craft conference, right?

Yeah.

Most other fields of engineering or in fact any other field of human labor has two kinds of conferences. Academic conferences where they talk about research and trade shows where vendors try to sell to companies. Software is kind of unique in having the third kind of the practitioner conference where we are just meeting to get better at what we do. We also are really the only kind to really focus heavily on open source and making our knowledge freely available for any language. You can probably find out how to learn a language online, right? You don't have to buy a book. You don't have to talk to the vendor to learn it. That's something really special about software.

Even some of the largest companies, I think of like an Uber or Airbnb, these are hundred billion dollar companies, they will not particularly hide how they built that piece of software. Uber publishes and does talks about their app that is used by all these people how exactly they built it or approximately. I wonder why this became unique in software and in not the rest of engineering, what does the rest of engineering have to lose with it or what did we do to get here.

I'm going to switch to speculation for a second, this isn't something that I could really speak on with full authority. But my guess is that part of it is cultural, but another part of it is that the material we work with is the same as our product, right? We are using software to write software versus using tools and lathes to build things or using software to design circuits. And I personally think that that similarity, basically that we are using the same materials on both ends is what makes it so much easier for us to talk about things like open source.

Interesting. I like this thinking of materials used in each engineering and how our material is software itself. Of course, it's hardware engineering and we know that's a bit different of course, but already there's a divide between hardware engineering and software engineers and how much they share, how much we know about them and so on. I kind of wonder, I've got some friends who do 3D printing and it seems like, and I haven't looked into this, but it seems like they also have a very open space of sharing things freely and I wonder if that's the same because it is so easy to share and because the unit of value is the schematic there if that kind of leads to the same thing. I also wonder if hacker culture might play a thing.

Guest: in places where it's easy enough to afford to get started on a thing for example ham radios which is not engineering but there's a thriving community where they share the setup the things they talk with each other small electronics might be and then but ultimately software started in the what 70s when it was affordable anyone could buy a computer maybe the internet I'm also just speculating

Host: yeah definitely something worth doing a follow-up project on Right.

Guest: Well, you've already spent a bunch of time on it.

Host: Don't give me so many rabbit holes. There's already too many rabbit holes in my life.

Host: One more thing that you brought up is version control and the fact that in software we just take it for granted. We have version control everywhere. And you said that this is super unique across most of engineering.

Guest: Yeah. I interviewed like 20 people on this. I think all 20 mentioned version control as a thing they wish they had in their old field.

Host: Wow.

Guest: Yeah. Now to be clear, they do have things like change management in like other fields, but I think version control as we have it is so much more sophisticated than anything they have. It's like comparing like a modern car to a model T.

Host: What do you think there are things that now having talked with so many people and learned about the different engineering cultures like active charging cultures? What could we learn from them? What are some kind of inspiration that might be useful here or there?

Guest: Yeah, this is a harder question because while everybody I talked to mentioned those two things of openness and version control, I got a much more scattering set of answers when talking to people about what we could learn from their old fields. The two things I kind of gleaned out is that one, while we are a lot better at iterating than other fields, we're worse at the planning part. Like we still need to do some kind of planning before we iterate and we just aren't as good as those other fields in part because we can get away with not doing it as much. But we could get some sort of fusion of the two and get even better than we currently are. Which, hey, plug for what I do. The other thing that I think is more interesting in terms of being a bit more shocking to me is that while we're better at being open about all of our materials, we seem to be worse at compiling information about the specifics of our job. And that's a bit loosey goosey, but the example I keep coming back to is that one of the engineers I talked about two favorite books. the design of everyday things which he recommends every engineer read and the snap fit handbook. Are you familiar with snap fits?

Host: No.

Guest: Looking around here to see if there's like one if I could just show it. But like you know like how remotes they have that little clicky thing in the back that you use that hold the battery in.

Host: Yeah.

Guest: That's a snap fit. [clears throat] It is a physical device that basically clicks into another device to keep them used. And this was a 500page book all about snapets, their engineering, appropriate shapes, materials, etc. And that kind of compiling of information about the materials is something other fields do that we don't do. An analogy that I would think of in software would be something like a 500page book on how to version an API.

Host: We could all use that.

Guest: Yes, we could.

Host: And and we don't have it.

Guest: We could learn it from engineering. We should have that.

Host: You started this project asking are we really engineers? And your personal inclination, which you didn't say at the time, was that we're probably not in the closing of this series. You said you're still a bit unsure of how to answer it. This was 5 years ago. this many years later, what is your inclination? Are we actually engineers?

Guest: I think so. I think this project and writing about and thinking about it has firmly moved me from the camp of we are definitely not to we probably are. I do want to caveat that I wrote this before LLM's thing and this has probably changed our field as we know it and it's probably also changed those other branches and I don't know how. So that could have changed the calculus between two spaces. But as of now, I think excluding LLMs and how they're changing things, what we do now is very similar to what those people in those other fields did according to my interviews.

Host: It's it's such a cool project and it's still a very good read. Uh I'll also link it in show notes below. I I do recommend going into it. So let's talk about formal methods. How did you get exposed to them? And for those of us who are not deep into it, what are they?

Guest: I'm going to give you a function max, right? Which should given a list return the largest number. What would be a test you'd write for that?

Host: I'd write a test that I do a list of like two items. It returns the the largest one that I know. I give a very long list. I I try to stress test it. I I I give a list where I give like similar numbers. I try to come up with some edge cases. I'll I'll probably write like five tests, try to think about integer overflows, potentially try some tricky, but maybe I'll take it to maybe eight if I'm feeling super ambitious and then I'm done.

Guest: Okay. So, when we take one of those tests, how do you know what the right answer is supposed to be?

Host: I just know because I have a I I learned math. So, uh in school I I know which which number is bigger. Honestly, I I look at it I have this I guess ingrained knowledge. It feels very basic knowledge that I don't even have to explain.

Guest: Right? You have some ingrained knowledge that you don't have to explain such that you can look at say the max of two and three and know it's three. Right? That's interesting. There's some sort of implicit mechanism in your brain that can see that and know what the function is supposed to do. Step one of what I do with methods is asking can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to actually be doing and write that down in a way that can be shown to anybody. So I would basically in this process say like the max of a list is an element that is in the list such that every other element is smaller than that element. That is a way that we can formally say what the maximum of list is. So that's part one just learning how to look at functions and say like okay I know what this is doing. How would I explain what this is doing in a way that is clear and unambiguous? Then step two is asking every single test you've written is basically some facet of it is an element of the list and it is the number in that list such that every other number in the list is smaller than it. Now that we have that what's the best way to show that our function actually satisfies that specification. Tests are one way. Those are basically taking individual values and showing how those component specification. Types are another way. we could basically say like okay in every single case we are putting in a list of elements and we're getting out a single element. So we have to make sure that every time we call it that's what's true. So basically the coming up with the the properties of the thing like what it actually is is the specification of it and then showing the function matches that specification is the verification and what f methods ask is can we use mathematics to show that it works not just for the cases that you asked for but every single possible list you pass in. And that is done through proof. Coming up with some sort of mathematical argument that this code matches this spec.

Host: And then in proof, again from university, I still remember the the maths proofs where we would proof an an equation. You do rigid transformations. You know what you're allowed to do. Sometimes you can bring in tricks, but those tricks are also inside of your rigid list. And every time, you know, you typically start from a complicated equation and you keep changing it. And in the end you you shape it in a way that it's now trivial or you transform. Those are one of the proofs we do. Is is this what formal methods also does to some extent?

Guest: Yes. But you know how to basically add two

Speaker A: tangent numbers by hand, right? Do you do that by hand or do you just use a calculator?

Speaker B: I now use a calculator. If it's easy enough, it might I use my brain as a calculator. Otherwise, I just punch it into the calculator.

Speaker A: Yeah. So similarly a lot of pro methods that math of transformation while you can do it by hand with like what's called a theorem provert often in industry that it's being done for the most part with tools that basically automate huge parts of this process. So you don't have to do every single transformation yourself. You can for example say okay we have these things are true at the beginning I want this to be true at the end and can you figure this out and it'll be like either yes I can prove these things match or no I need a little bit more help. And you say like okay at this point I'm going to also let you know that this is true and like okay I can verify that's true and it helps me get to the end and you just keep doing that until you actually have enough that the computer can do the proof for you.

Speaker B: Yeah. So with formal methods this I mean this sounds all logical I think is easy easy to follow in practice. What techniques technologies tools does the industry use the tech industry use to actually prove that you know some some stuff works?

Speaker A: To get to that we need to ask another question. Why isn't this being done for everything?

Speaker B: Okay, let let me ask that question. That's a good question. Yeah, this all sounds sounds sensible. It would be nice to not have to write out those five or eight tests. And I know that those tests might not cover all edge cases. Been there, done that where you miss and I I I didn't think that I didn't do a formal proof. I thought like, well, I missed a test case. That's on me. Sorry. Let me put in that that test case. I now have nine tests and now I go and think I did a great job. Why are we not doing formal testing for everything? Instead of finding the largest number in a list, why don't we try to find the file in a directory that has the most lines in it?

Speaker A: Well, now I'm thinking of writing a program that in kind of an imperative style, it goes through a four list. Each each file, I list how long the the lines are. I count the lines. I cannot tell easily.

Speaker B: Okay. Are we talking about asky lines or UTF at new lines? What happens if one of the files you don't have the file permissions to read it? Should you basically ignore it or should you say like, hey, my proof my my um function might be wrong.

Speaker A: You're now trying to What if one of the files is a shortcut to another file? What if it's actually directory?

Speaker B: Damn, you're now simulating a binary.

Speaker A: You're now simulating real world.

Speaker B: Yes. And that's the problem we have is that when you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases. And if you want something that works 100% of the cases, you've got to figure out, okay, what file system are we using? You have to figure out everything.

Speaker A: Yeah. And that's why it's [clears throat] not done

Speaker B: and basic it would just not be practical. It would be for the for 99% of the people would be why are you wasting your it's like premature optimization right?

Speaker A: Yeah especially when as you say writing 10 tests might get you most of what you need. What are practical technologies that you have seen used in some part of the industry that even though they will I'm assuming will be somewhat heavyweight because it sounds like pretty heavyweight. It might be the return the return of investment of using this heavyweight stuff is worth it that teams in industry are using it today right and here we can basically start to break this down to different parts of the landscape. So, one part is to look at the stuff that actually does need to be verified to that degree. And the usual term here is nukes and NASA like nuclear power plants and like um NASA, but I can tell you with firsthand experience, nuclear power plants do not care about this stuff. They're actually just fine with with with thorough testing.

Speaker B: Okay. Okay. So, then category two is like really focused cores of programs where they need like one specific part of the program to be like really verified and the rest of it they can use informal methods. And this is usually things that are like um small parts of databases or like cryptographic primitives. I believe that the HTTPS stack in Firefox is verified as part of something called Project Everest, but I might be getting some details of those wrong.

Speaker A: Would an operating system kernel fall into this or maybe just a very key specific part of a kernel like memory allocation or something like that?

Speaker B: Yeah, parts of um operating system kernel are good uses for this. Um, a couple examples I can think of is I believe Microsoft used some polarification of parts of their beasta kernel for the driver loading. Famously there was an operating system called4 that has been endto-end verified in a language called Isabel. It's a micro kernel. It's very small. It's mostly used for um automotive and military applications but it is a fully verified operating system with a caveat meaning that it's matching the specification. So it might do the wrong thing but of the things that you specify that it has to do right it will do those specific things right in the right circumstances. The last category is the kind I work in which is asking okay what if instead of verifying the entire real world system which is a nightmare as we just discussed. We create a simplified version of the system and verify that then the actual system might still have bugs but we can iron out the issues in the abstraction such that we don't actually build them in the real system. And and so that that's a topic where you are planning a system and you want to stress test it to iron out.

Speaker A: Yeah. Stress test the plan.

Speaker B: What what kinds of plans would these be roughly? Is is it planning like again database or or some sort of distributed system?

Speaker A: In my work, it's mostly been um databases and distributed systems for technology companies, but I've had some other like interesting gigs. Like I've had one gig that was involving formally verifying um firmware of a device kernel. And one honestly, one of the coolest projects I ever worked on was um verifying the transponders of a train system to make sure that they wouldn't cause problems to trains going over those transponders. That was a lot of fun. We found a really old bug in that one, too. That was kind of exciting.

Speaker B: This whole episode is about a question that only gets more important as AI writes more of your code. How do you know if it's correct? And for some parts of a codebase, you really don't want an AI model to be taking guesses at O is on top of that list. And this is where I need to mention our season sponsor, work OS. If you're building any SAS, especially an AI product, you'll need O for apps and agents. This is the layer where close enough is just not good enough. So don't [snorts] let this layer get improvised by AI. Worker gives you the proven implementation SSO skim and fine grid authorization built for how agents operate and in a way that's easy for them to integrate with an implementation that you can trust. Check it out at work.com. I also want to talk about our season sponsor Turbopuffer. But this time I don't want to talk about how they are fast, cheap, and extremely scalable search engine built on object storage. Instead I'd like to talk about their team. I interviewed Simon, the co-founder and CEO, on stage at AIGO's World Fair and also hung out with their team for a few days in person. Here's a few the interesting things I learned about them. The company is full remote yet feels pretty connected. They have a Slack first culture. For example, all of their customers have a dedicated Slack channel and engineers are in these channels seeing feedback from these customers, often fixing their bugs. The team gets together for annual summits at least twice a year and campfires form several times a month anytime

Host: several remote employees gather in the same city. Simon describes their engine culture as hardcore and whimsical. They focus on solving difficult problems but also try to have fun. A good example is the pragmatic engineer landing page that they built. We agreed to have a custom landing page and then their team decided to build a cool logo that animates on mouse movement. Another interesting thing is their team composition. Pretty much everyone currently working at the company has 10 15 years of experience. For a startup, they are an unusually seasoned team. Finally, I really appreciate how pragmatic their engineering philosophy is. Simon and the team strongly believe in how simplicity scales and this is a reason that object storage is Turbopuffer's only dependency. The team do seemingly silly things like build their job QE in a single file on object storage because they understand the core primitives and they know how they scale. to check out the whimsical animation or if you're building AI products, head to turbopuffer.com/pragmatic. And with this, let's get back to how TLA Plus works with a demo from Hill. Can we see a demo?

Hill: Okay, sure. So, I've got a couple languages with me. Um, the kinds that I've worked in. So, the most popular technology right now for that kind of planning is this language called TA Plus. It was invented by Leslie Lamport, the same guy who made Latte, the um type setting language actually.

Host: Oh, yeah. All the PDFs behind the scenes are are latte. Yeah, Pet Caesar Latte

Hill: and he wanted a language that could be used to model distributed systems. So he basically created this thing called TA plus temporal logic of actions plus everybody always asks about the name. You don't need to know the name just known as TLA plus. And what it does is it basically represents the state machine of a system. Every possible state it can be in and every possible state it can it can transition to. Then we can use a brute force model checking where we basically find every initial state and every state that can evolve from those and check if they have properties. TA plus is unique in some ways because it has certain properties like checking livveness and refinement that we won't get into. But let's actually see a demo right now. So this is one of the demos I like to use to showcase this. And we in this demo we have a simple model of a trading platform. Each person on the platform has a set of items and they want to trade these to other people. The way that we're going to show the simplified system is that each item is assigned to a person. There's also a set of outstanding offers. We're only going to model sending items to people, not swapping items. If you propose an item, you have to own that item and it's basically added to the set of offers. And then you can accept an offer. If that offer is available, you remove it from the set of offers and the owner transfers. If you reject the offer, it's just removed from the set. Then we define what can happen next. A next state as in one of the ways the system can evolve is we pick some two people that are different. That's what this from dash equals 2 means. and some random item and either you propose that item, accept a proposal for that item which must already exist or reject an existing proposal. Below we have a property that a valid change is one where if the owner changes it is because the new person accepted an offer from the old person. So if the item goes from you to me it's because you offered it to me and I accepted that offer. And finally we have a change invariant some property of the system saying every change is a valid change. Now what's the bug in this?

Host: Well, first of all, this has a learning curve.

Hill: Yes, it has a learning curve. And that's why this is fairly niche. And I should probably point out right now that when Leslie Dumper made this in 1994, he was thinking of it mostly he was a mathematician, right? So he was using his mathematical like background and like learning how a mathematician would write some symbols. In the 30 years since that point it's been 30 years since 1994 already. A lot of languages have been developed in part from the lessons of learn of TA plus that make things a little bit more appealing to programmers. So you have things like Quint and P which are languages that look more like programming languages and are easier for people to gro. The reason a lot of us used TA plus was because like the first really high-profile demonstration of this kind of work in practice was an Amazon paper, the use of formal methods at Amazon Web Services in 2014 and they used TLA plus for this. So that's what a lot of us just have originally started on.

Host: So going back to this, there is a bug in this one with with with all the associations and how can we how can we figure out what the bug is? Will will the system help tell us or or we now need to think through what case we miss?

Hill: Well, if we had to think through it ourselves, we wouldn't be using this nasty syntax, would we?

Host: Nope.

Hill: So, what I've done is I've also written a quick um configuration file saying take a specification, take these three people, Alice, Bob, Carl, and have them trade around a stick. And then I tell it, make sure this property that the change in variant always holds.

Host: Always holds. Now I just have to run this.

Hill: I'm also having it output the state space for you so you can see what that looks like. And it just puts out the error for us. It says the property has been violated. It took 53 states to find it. And the way it works is it's on a small screen so it's being word wrapped. But if I see it kind of looks like this. Essentially the error is as follows. And let's actually see if the error I can show it to you with the um dot file. as um biz graph is not dotiz what am I saying? So this is just um a preview of the state space it's generating. So you can see it's basically generating every possible state it can find. This isn't the whole state space. Usually because these the state traces end up being like 100 million states for like in the state space. Usually these aren't that useful. It's mostly a thing that we have for that we sometimes use for demos. So, the error is as follows. Alice, Bob, and Carol are on the system, and Alice owns the stick.

Host: Yep.

Hill: Alice makes an offer to Bob. Bob is away. Alice gets tired of waiting for Bob to come back to make the offer because she wants to get rid of her stick. She makes the offer to Carol. Carol immediately accepts. So, the stick transfers from Alice to Carol. Now, Bob comes back, sees the offer from Alice to Bob and goes, "Oh, yeah. I want that stick." Clicks the button, and now the stick becomes Bob's. But it did not transfer from Alice to Bob, it transferred from Carol to Bob. So the change in variant that if the stick went from Carol to Bob, it must be because Carol made an offer that Bob accepted was violated. And therefore the system raises an error.

Host: And then how did the system simulate this? It had to simulate a state where Bob was waiting or or didn't respond for a while and responded later.

Hill: We basically assuming we start in the state of basically Alice owns the stick. There's two possible things that can happen here, right? We have offer Bob.

Host: Yep.

Hill: And we have offer Carol, right? So those both happen and those are both distinct states. So the model checker says, okay, I'm going to create two new states. Then from this top one of offer Bob, there's three things that can happen. We can have Bob accept

Host: Bob reject

Hill: or and this is where the concurrency comes in. We can do offer Carol, right?

Host: Yep.

Host: I see.

Hill: Yeah.

Host: Mhm. I I see where this is coming. And then when you continue, we will hit the bug.

Hill: Yeah.

Host: The change in variant will be invalid at whatever step that is run at.

Hill: Right. And that's actually where a lot of this like becomes useful for distributed systems because often it'll be like okay process one can do one of six things, process two can do one of six things, process three can do one of six things. And when you do this root force you get states like process one takes step one, then process one takes step two, then process two takes step one

Speaker A: takes step one, then process one takes step three, then process three takes step one and two, then process two takes step two and three, etc. And being able to sort of see every possible iteration of that is very hard for human beings to do, but a computer with enough CPU can just brunch through to in a night or two.

Speaker B: Yeah. So, so this is what TA plus is then.

Speaker A: Yeah, basically.

Speaker B: And one story I've heard and I think you might have been involved is AWS uh using TLA plus. Can you talk about how they onboarded, how they're using it, what they're using it for as far as you're aware?

Speaker A: Yeah. So the seminal paper on this was in 2014 the use of foral methods in Amazon web services and they talked about how a couple of people in the company were interested it and learned TA plus another language called pluscow which is something that compiles TA plus and applied it to aspects of the Dynamo Dynamob and S3 storage systems. In doing so they were able to find fairly complicated bugs that could potentially lose data and I think it was in the replication system. In the paper it said that the shortest error trace exhibiting the buck contained 35 highle steps which if I understood that correctly it was at at a depth that it would have been very hard for a human to p persevere or you would have need to be really determined

Speaker B: and precise.

Speaker A: I did not work on that project of course so I don't know what the details are. I can speculate that the reason it found a 35step bug was because the state base was probably 100 million states wide. So there were like plenty of say like 70 or 80 step chains that were totally safe and it just happened this 135st step chain was invalid.

Speaker B: Through working with a lot of customers and and and teams that that have used form of verifications with distributed systems, what are some problems you've come across with distributed systems that might be a bit of a repeat pattern of of you know how they break down or why they break down?

Speaker A: If I can think of like one thing that like besides like just general race conditions and locks, this is the one that like is always a new pull was like yes, it's another time to allow a time to check the time to use bug. And time to check time to abuse is a situation where you are checking to see if something is like valid can be done validly and then you see that it's correct and then a little bit later you do it. Sometimes that little bit later is like a day later. Sometimes it's a microcond later. But is any case where it is possible for something to go from being valid to being invalid in between the time you check and the time you use it. A good example here is imagine you're withdrawing like money from a bank account and putting into another bank account. And this is not how banks work. I know they use a different kind of ledger, but just as a demonstrative example, you check, oh, do they have $10 in their account? Yes, we deduct $10. We put $10 in this account. But what can actually happen is you check, do you have $10 in this account? Yes. And then while you're still getting ready to withdraw, somebody else quickly runs in and grabs those $10 away. And now they're $0 and now you deduct those $10, you have negative $10. That's a time to check the time to use kind of bug. They happen everywhere.

Speaker B: Yeah. And it's very interesting because I when we were building Uber's payment system, I realized or I learned that the problem of having a message delivered in a distributed system exactly once is a very difficult one because typically that's what you need when you want to do one one charge. You want to charge a customer's card exactly once because if you send multiple messages just in case one of them gets lost, you now have double charges. And turns out it's a it's a complicated problem. It's a lot easier to do at least once delivery.

Speaker A: Yeah.

Speaker B: Than exactly one's delivery. But of course you need exactly at least one's delivery to build on to create exactly one delivery.

Speaker A: Yeah.

Speaker B: I wonder if this is why like a lot of like um businesses they just charge you extra and then refund you some amount that seems like easier to do from an engineering perspective as as well.

Speaker A: It's also from a risk perspective you eliminate a lot of uh edge cases by authorizing upfront on a credit card you have a credit limit and if you would authorize exactly how much you think you need right now but you need a bit more you might get into that edge case where later you have trouble authorizing it. This is why often hotels don't want to deal with this. So they just authorize a larger chunk and they know because it's it's a larger amount for hotels. Otherwise they might have run into the thing where you would run out of your credit and now they have to do a separate flow. But you're right some engineuring decisions might happen because it's easier to do some some stuff.

Speaker B: Yeah, it makes sense. I honestly thought hotels did that because they were trying to convince you not to like break stuff because like hey if if you know that you're definitely going to lose $800 if you break something like you're not going to break stuff.

Speaker B: Through working with engineering teams who are building distributed systems and you're coming in and helping them learn TA plus uh learn how to survive things. What have you learned about how they usually think of verifying distributed systems before they learn about formal methods and what changes after?

Speaker A: So I think the most interesting thing about formal methods and how it affects how you build systems isn't the theory of the method or how it makes you think about systems. It's the practice. Why is concurrency hard? Why is it hard for us to reason about concurrent systems? Why why do you think it's hard?

Speaker B: I think it's hard to keep several things in your mind of like where they could be. That's one. Or maybe we just don't really have a mental model of how to draw them out. I guess whiteboarding would be a way to do it. But I I don't remember whiteboarding on concurrent system. I remember whiteboarding just boxes and and imperative. This flowcharts are good for whiteboarding.

Speaker A: So this is something that I've wondered a lot, right? Like why it's hard for us to deal with these systems. And I'm not sure it's because it's hard for us to think about them. I mean like when you cross the street, aren't you working with concurrent system? You're just there's cars everywhere. They're going to hit you. You're going to die if you don't model concurrent system in your head. And there's actually this really cool paper I found called common sense computing where some people were trying to figure out like how people thought about concurrent systems. when talking with like sort of like high school and college students, they changed the concurrency problem from like, hey, we've got these threads doing some operation to like, hey, we've got these like clerks at a ticket office assigning seats at a concert. People saw the bug much faster. So, I do think we can actually get quite good at seeing concurrency issues. I think a large part of the problem of why it's hard for us is because we don't get a lot of practice. Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked. Whereas with the TA plus like I write my model of the system and then I click a button and immedately tells me hey race condition and then you fix it and it says like hey timeout bug and then you fix it again and says hey to bug and that feedback loop ends up being so much faster than you get in practice. And I think that more than anything else helps people find race conditions more easily and think about problems and distribute systems more easily. I've found personally that when I work with new clients and we're modeling their system, I usually have no idea how their system works, right? Because they're the domain experts. I just have know this really weird funky language made 30 years ago. But once we actually have the model, I can see the bug in the model much faster than they can, even if it's their system simply because through this

...main change in how it affects people's ways of thinking about distributed systems. It gives them actual practice of seeing how those systems can go wrong so much faster.

I wonder if it's a little bit like refactoring and also migrations. So refactoring a codebase when you are starting out as a developer and you need to do a refactoring by hand, you know, let's say just changing a function name, and then you need to go and change all the references to that function. And the first time you do it you change it at a few places and then you forget about the rest, and either it's a compilation issue or if it's a dynamic language it's another problem, but then you get good at it once you practice.

With migrations, most engineers that I've seen are terrible at migrations because you need to make a plan, you need to do checks, you can do shadowing, reverse shadowing, all that funk. And then there are a few engineers who have done three or four or five and then they close their eyes and they can just do it.

I'm just thinking that when it comes to race conditions most of us... I was exposed to race conditions by "oh we did a double charge that one and then we found the race condition." But I never did a second one, so I will not be good at finding race conditions. I'm not even good at thinking about them.

I think that's right on the money. It sounds like you coming into teams or to these clients, you at least give them some practice, the very least of how to think about this category of errors even assuming that taking out even the tooling itself.

I think there's also more subtle things that you start to pick up from these tools, but I think that's like the most visceral one—the visceral hatred of a race condition that gets a physical presence in the algorithm.

You've been doing this for very long. For you, writing TLA+ is like for most of us writing TypeScript or the language that we're familiar with. How has your thinking changed? And is there any similarities between when you program in an imperative language and then you learn a different one like a declarative language which requires a very different thinking?

Mhm. And that also depends on declarative language. Like I've done a lot of stuff in logic programming languages and like array languages, but you show me CSS and I'm just like, "what is this dark magic declarative? What are you talking about?" I think so.

Um, it's going to be hard to sort of pin down exactly what though. Like my usual haggling language is Python these days just because that's one of the first things I used and I just know it very well. And I think at the very least, formal methods makes me much more willing to reach for mathematical solutions or math-heavy solutions than simple reliable solutions.

Math is also an interesting topic. You've recently had a bit of back and forth on whether developers, programmers, software engineers should learn math. There was a bit of a discussion back and forth. Could we talk about the core of the argument?

How math is useful in programming is a very interesting question. Right? So first of all, there's math that we all find so useful we forget that it's actually math. Like counting, counting is math. Knowing whether one thing is bigger than another number is math, right? It's just math that we have been taught from a very young age because it is so important that no matter what you're doing in life, you need that math.

Then there's a lot of math that is useful for very specific specialist jobs. Like I've talked to some SREs who need calculus, but I think most programmers do not need calculus.

There are some branches of math that are useful in a wide range of programming. I think things like understanding graphs and directed graphs, knowing matrices, knowing formal logic can be very useful for a lot of different people. But I think it is more useful for most developers to have an exposure to what math has in the various fields versus just going all-in on every single field when they see them, right? You've got to know what's available to know what's most useful for you. And most math will not be useful for you.

It's also very interesting because for a long time I thought at university we had pretty heavy math education for computer science, from algebra to computational theory to even formal methods.

At university I learned a bunch of advanced math and at first when I came into industry it wasn't particularly useful or I didn't use it day-to-day. But then there are some times where it's kind of useful. For example, matrix transformation. I learned 3D graphics and how you compute all the points based on 3D matrix transformations, and then it helped me understand when GPUs were becoming so popular with AI why this is—because they're also very good at matrix transformations, which happens to be pretty similar. So every now and then I feel it helps with your general understanding and it helps you be unafraid to go into deep. So if I see a paper with formal proof, I'm not going to shy away from it. I can start reading it and I will know my limits, but I have that understanding.

And I think going back to our discussion with the crossover project, I wonder if it helps you connect closer with other engineering disciplines in terms of you can understand more things there. For example, for electrical engineering, you do have math involved that is there to describe, and if you will want to have the vocabulary to understand that part.

One of the interesting things at least about the mathematical differences is that in almost every traditional engineering field, the math they need is continuous math analysis, things like differential equations and calculus. And that in the United States is what's taught at an advanced level in high school if you get that far, is this kind of continuous math.

In software engineering and computer science, the math we most often use is discrete math. Things like combinatorics basically, which is the math of counting things, graph theory, formal logic, set theory—things that work with discrete entities which isn't usually taught at least in the American high school very much or even early in university mathematics classes. And I wonder sometimes if that is the reason people don't recognize the use of math in software engineering is because the math they do need is not the math they've been exposed to.

Interesting, yeah, because the math that I did use more was common networks. And of course, maybe these days those entries are going out of style, but there's the "here's a problem, build an algorithm that solves it", and then you ask like "okay, how efficient is this algorithm?" And then there's the Big O notation. We have the language to describe how efficient in space and time it is and you can do tradeoffs. And once two people know the same thing, you can have discussions about these things. On one end it's very abstract, but on the other hand, if you're close to the machine it can be very useful.

I've also found that my understanding of Big O notation got a lot better once I understood the mathematics behind it, because I think it's usually explained as terms of like "oh this function scales at this certain rate", but it is more formally a way of describing a set of functions and then there's the math of how we do asymptotics and stuff, etc. I think even in the technical aspects, math does help a lot in understanding those.

Yeah. And with the TLA+ specifically, what cases have you seen in the industry TLA+ being a good fit for certain problems, and in what cases would you ever consider it?

I think the case of TLA+ and most—not all, but most—formal methods, they shine the most in highly computational domains where most of the problems are highly technical and not business embedded. And what I mean by that is that something like "how do you replicate nodes between these two data sets" is very technical, right? Something like—I'm trying to think about a good example here—like "how do we make sure our sprints don't go overtime" is...

Presenter: business, right? It deals with like very human behaviors. So, I've had to help model client model that and we got some use out of it, but it was very hard. So, that's why a lot of my clients end up being things like database vendors or like cloud computing people who are or like hardware people who are working in a space that's like very important for business, but several steps removed from like the front lines of that business. The other thing I would say is that different tools are good at different things. TA plus in particular tends to be good at discrete distributed systems where the main challenges are messing with concurrency and possibilities eventually being like behaviors. It doesn't do floating point. It doesn't do decimals. It doesn't do as well with when you're trying to figure out probabilistic things. Oh, that's another thing I guess I should be saying is that like where the kinds of errors you care about are ones where like if it is possible this error to happen, that is a big deal. It's not good if like you're like, "Okay, this error is bad, but as long as it happens less than one out of a 100 times, it's it's okay. It can't do that kind of probabilistic reasoning for you." There are tools that can, but they lack things like functions or arrays or numbers.

Presenter: Also depends on how much time you need to spend planning. Like if you don't need to spend that much time planning, this is going to waste your time. I I do want I do want to add that that this like if you can iterate your way through a solution and the bugs aren't going to be that costly then you might not need this tool. I I think it's really important as like a person who who talks about a really exotic tool to like constantly emphasizing like no I'm not trying to convince you to like use something that's not a good choice for you. I think a lot of the reason people are skeptical of these is because they've been burned by things like case and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what. And I think it's really important to always say like if this isn't the right tool for you, I am not going to recommend it.

Interviewer: And then can we talk about other other tools or can you show us a few other ones?

Presenter: Yeah. So the other tool I have installed on this computer is called alloy and it was made by an MIT professor. Different format is lineage. Just like there's many different kinds of programming languages, there's many lineages of formal specification verification tools. So this example is a simple access control system. So we have a set of resources and users who can read those resources. Yep.

Interviewer: So each resource has some people who it's reasonable by and resources may or may not have a parent resource. L1 mean L1 meaning less than equal to one resource.

Presenter: There are no cycles. So no resource can have itself as a parent or its parents parent as a parent.

Interviewer: Yep. You can read access a resource if the resource indicates you can read that resource or if it's parent indicates you can read that resource and we have a property that if you can read a resource you can read its children.

Presenter: Yep. This is has a bug. What is it?

Interviewer: I mean I I'm I'm glancing at this and this all made sense to me. I thought this is it cuz we're saying all of the parents can access it. I'm assuming the bug if if there is one is it will it might have to do with something that we talked earlier of like accessing in certain areas. No idea. Can we run it?

Presenter: Yes, we can. So this was actually made in an earlier version of alloy just for the just for context. Um alloy did not have any sort of temporal reasoning over state up until about 4 years ago. So this is one examples I used from before then of basically how you can analyze and find bugs in static configurations. An alloy that often means finding bugs in data structures or in data models and domain models actually. So there's actually some interesting there's some interest in this in the domain driven design community I found. I'm going to copy this over to alloy their IDE which is a bit more rudimentary and that's why everybody uses the VS code. Now, if I execute this, here's the counter example. All right.

Presenter: And this is one of the nice things about Ali specifically is that it can generate like visualizations. So, basically, here's the problem. We have a user who can read a parent resource. The parent has a child because of how we defined um can access we can read as parent so we can read the child.

Interviewer: Yes

Presenter: the child has a grandchild we cannot read the grandchild. So because we are not in we are not assigned to the readable by for the child only the parent. In other words readable by is not transitive. So we can read the child but not the child's children. And that is the bug.

Interviewer: Mhm. and to visualize those for us.

Presenter: Yes. Which is quite nice and one of the reasons why people really like Alloy.

Interviewer: Nice.

Presenter: It's a bit worse for modeling like distributed systems though, which is why most of my work is in TA plus.

Interviewer: And then to do the fix, what would it involve? We would need to give access to the children's children.

Presenter: Yeah, there's a few different ways that we could fix it. And often like pro methods, they don't really tell you here's how you fix it. It lets you choose how you want to fix it. Like one thing I could do is I could say okay I'm going to say that this is a transitive lookup too that we transitively close over all parents and if I execute that no more counter example that said that might not be something physically implementable I might try to tell like hey people like hey in our SQL database you have to have a transitive query and our database administer is like no that's going to crash the database you can't do that then we have to find a different fix

Interviewer: so this is the beauty of formal methods yes it it it gives gives you opportunities of how you will implement fixes, changes, and then you can rerun it again and see what difference it made.

Presenter: Exactly. Now, one quick fun fact. I love just fun facts about stuff. You see how this says solver SAT 4J. So, have you heard of SAT SAT problems?

Interviewer: No.

Presenter: Okay. Is there some variable that makes the statement P true? If I can make P true or false, is there a way I can make that true? So let's say P is a boolean and I have a statement P. Can you assign some value of true or false to P to make that true?

Interviewer: Typically you can assign true and it it will correct

Presenter: both true. Yeah.

Interviewer: So that statement is satisfiable by setting P to true. What about P and not Q

Presenter: also satisfiable by by giving giving true to P and false to Q.

Interviewer: Right. Now what about P and Q and not P?

Presenter: that that unsatisfiable because no matter what booleaning you do the the true and false will always will never be true.

Interviewer: Lovely. What you've just done is a boolean satisfiability problem taken some sort of statement of a ton of boolean variables in this case two and found some either found some assignment that makes it true or said that it cannot be made true. Now boolean satisfiability is what we call empty and what that means in theory is that there's no such thing as a perfectly efficient algorithm that solves all problems. In practice that means that we can solve them really fast. So often what makes alloy interesting is that unlike TA plus which mostly brute forced alloy can be converted into a satisfiability prop. I'll open this up and it is able to turn that model into a boolean probability saying not x21 and x96 and x15 or not x72 etc. And because of that most alloy models can be checked in like a few milliseconds or a second at most. Whereas often for like a large TA plus model, you have to basically churn it overnight to go through all 100 million states.

Interviewer: Can we talk about some other tools uh on the I guess a table of someone looking into formal verification?

Presenter: Happily. So I don't have any more demos on my PC right now, but I can talk about a few of them. So a couple of the ones that have been success plus is um the P language um which was invented by I think a person at Microsoft research who was then poached by Amazon as a way of making a language that

Guest: was more accessible than TLA plus among other things. So it basically looks like a set of um state machines interacting state machines that send messages to each other almost like the actor model in like Erlang or something like that.

Interviewer: >> Yep.

Guest: >> So there's that. There's also another one in the same space as um Quint which was basically people who were making a different kind of model check for TA plus and then realized they can make an entire language that was easier for people to pick up. They've gotten a lot of interest in the banking and um I believe cryptocurrency space smart contracts. So another one that I've used which is which is a lot more niche but quite interesting is called Prism and Prism is a proistic mile checker. So like Kila Plus can tell you like this bug will never happen or it could happen. Prism can tell you this bug can happen 10% of the time or it is a 25% chance of happening if you shut down. It's really cool but it's also much more like academic in that there's a lot more work required to actually translate languages into Prism. If you're interested in it, I've basically been doing this like um have you heard of the Jewish game Drrele?

Interviewer: >> No.

Guest: >> Okay. It's a game that you play on Clanica where you spin a little top and you get money. and I do not like the game. And I have written a two-part series using Prism to show how this game is not fun by analyzing as a mathematical thing.

Interviewer: >> Love it.

Guest: >> Those are I think some of the ones that are like really popular. But there's also um I mean I could just keep listening. There's like there's like event B which is like been used I believe famously in part of the Paris Metro system. Um there's like MCRL2 which I think is come comes from a Dutch university. Hum X which is mostly used for like um robotic control systems but I think that's mostly academic. There's like new SMV which I think NASA's used for a bunch of stuff. I can keep going. Then of course there's all the of course this is only for specifying like abstract models of systems. If you want to talk about verifying code then you've got things like Daphne which is basically something that compiles to like net and lets you basically write provable code. You've got JML for Java check for like model checking Java code. You've got like um Primma C for like checking C. You've got Ada Spark. You've got like and you've got Ethereum provers like um Rock and Lean and Isabelle. And I can keep going. I

Interviewer: >> I wanted to ask how does property based testing relate to formal verification and and before let's just like lay out what property based testing is.

Guest: >> So let's go back to that entire thing with max right max of a list. we can define like the specification of max it is in the list and for all elements of the list it is the largest element of that list right I actually have a demo on my computer of doing that so let's actually go into this so over here in this file that I wrote for my book plug I have a I have basically three variants of max a good version which just returns the max of the list one that returns the max of the first three and one that returns max the absolute value.

Interviewer: >> Yep.

Guest: >> This below here is a property test. What it does is it says given a list of integers where each list has at least one integer in it.

Interviewer: >> Yep.

Guest: >> The maximum value of that function should be in the list and all other values should be less than or equal to it.

Interviewer: >> Yep. Clear.

Guest: >> So this basically a lot like our formal verification spec, our formal specification spec. The difference between the formal methods that we do and um property testing is that the formal methods are ask are saying like okay can we prove this for every possible list and property testing is well that's very very hard and as we talked about very difficult to do in practice can we instead generate a thousand random lists and try all those I have it set so that way it basically has the invalid max max the first three

Interviewer: >> we should be getting errors or it should catch some errors.

Guest: >> Mhm. Let's run it. Let me just run it from the command line. That's faster. Uh um pi test uh test max.py. This is an old machine I mostly bring on for conferences because it's like easy to just throw in something on here. So we see over here that it says that this test failed on this line that for the list 00001 it is not true that all the values are greater than zero. This is because I said our badmax only looks at the first three values. So it found the max was zero but here the actual max of the list was one. I broke this down to two subspects for a part of the book where we have testing that max is the largest element and also that it's in the list. So that's why one of the tests passes. Um I should note though that um if I believe I run this with a verbose what I'm trying to do for this demo is um show that it actually does not start with the um largest list. It actually starts with a much smaller with here we go. If I print max, if I print then I do it like this. I think it tries a lot of edge cases first. So it's basically trying huge list is trying like tiny list is trying like empty list etc. And once it has one that fails, for example, this value, it starts to shrink it. Finding the minimally interesting example. And that's why this lets us like find a bug. Not just find a bug, but also find a bug and present it in a way that is like comprehensible for the average human because I think that it found the original bug with this list. And I do not think that looking at this, I'm going to know what the problem is. That's basically property property based testing in a nutshell. And as you can see, it is less thorough than formal verification, but it's a lot easier to apply.

Interviewer: >> So, it sounds like it can be a nice middle ground in terms of getting started with it

Guest: >> and probably just stopping with it because I think that I love formal methods, but I think it's a fairly niche tool for most people and I think like property based testing is in general going to be useful for more people.

Interviewer: >> So, speaking of of verification in general, today we have AI generating way more code. We have data to prove this as well, but also dayto-day I I I see it on myself. I have AI generate a lot more of my code. We're getting more code. C code reviews are people are it's hard to pay more attention to this. So there's a growing number of people saying well maybe we should somehow validate things more and there's an idea that keeps coming up maybe for more verification or property based testing or some of these things could be more useful. Do you think this will happen or because I see a lot of people talking about this. I I don't really see anyone doing much about it.

Guest: >> I'm definitely seeing more business from people in my my client as method is people trying to generate specs with AI and then getting me to help like work with the spec or like find issues with that and I'm definitely seeing more people like using property based testing. I know for example I think Kro like the Amazon specri development platform specifically advertises generating property tests as like one of the key values of it and I've been seeing a lot of like papers about generating specs using AI. I will say this is kind of really exciting because as you saw like a lot of the challenge of writing a spec not all of it but like a lot of it is like rocking your head around like very very technical syntax and like semantics. That said, I've been doing a lot of experience with this myself and I think the one thing AI is extremely bad at as of March, I know that claude just released a new like cloud 4.8, so maybe this is all out the window. It changes every month. It is very bad at coming up with properties. It is very bad at that.

Interviewer: >> What What does coming up with properties mean? Is it writing the actual form of verification part?

Guest: >> Yes. So, like if you give it properties and like a spec, it can tell you like, hey, we're going to fix the spec, make these properties pass. That's fine. What if you basically tell it here's a spec also come up with the properties of the spec. It'll be like, okay, so one of the properties I'm going to

Speaker A: specify is that either P is true or not P is true. And then you're like, that's just always true. And it's like, wow, I verified it. Amazing. I'm so good at this. Especially when you deal with what's called liveness properties, properties about how like a system can evolve over a long period of time. It just it's hard to put down. It's just not good at that yet. And often I found with my clients, I have to tell them like it's doing a good job at generating the actual design, but in actually expressing what the design is supposed to do, it cannot do that yet. You have to do that part yourself.

Speaker B: It's interesting because there's a blog post that I'll also link in the show notes from a year ago in March 2025 titled "The Coming Revolution in Distributed Systems". And this was an engineer working on GitHub's Copilot team. And this person wrote how AI autonomously produced precise TLA+ specifications from Azure storage production source code and it uncovered a subtle race condition that had evaded traditional code reviews. And then this person was very enthusiastic and saying well this could be a revolution, AI could just generate TLA+ from specification like it did with Azure. This was a year ago and I haven't heard much on any of this even though the models were not as great. What have you seen in this area?

Speaker A: So actually the same person Chang Huang did come up with a tool called Lamport Agent where they demonstrated using this to specify parts of CRAQ I think it's called part of DC's CRAQ. I'm going to link both those in the thing. Here's my response because I was writing about this and then the thing that they did. He seemed to be a lot more successful than I was at generating properties. But at least the example that he showcased in his later piece, one, he's an expert specifier who already knows how to do this stuff on his own without the LLM so that makes it easier. Yeah, he knows how to get good results out of it.

Speaker B: As that's a general thing we've seen, like to get good results you have to already know how to get good results without it, it just helps you get good results faster. And also one of the systems that he was able to create the complicated properties for in TLA+ already had a sophisticated spec written in P, so I don't know how much that's relevant here, maybe it read that and it cheated. Maybe that was fine. I don't know.

Speaker B: But we do see this a lot where when you're an expert in a domain, and may that be software engineering or backend or mobile, AI works better for you. Then there's also this one interesting person Claudia Collie did write a write up because she just did about a multi-year project in using methods at the big Chinese cloud provider where she talks about how in between her working on this paper and the time she got published she got really sophisticated on how long it took people to write formal methods at this one company and then LLMs basically just compressed the scale by the time she actually had the paper out. So I think people are seeing more use from formal methods but it seems people with the most success right now are specifiers who are using it to amplify their ability to specify and we haven't yet really seen—I mean people post Hacker News all the time like people who they had an AI write the whole spec for them but those tend to not be very good specs. And what's your take on, again I've heard some voices say that AI might make formal verification go mainstream based on this, but outside of this niche of people who already know how to do formal verification, do you see any movement?

Speaker A: I think it is making it more popular. I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3%. Which is huge.

Speaker B: There's also this thinking that I've read actually in June 2025 in your newsletter, you said that AI is a specification force multiplier. And now, of course, we see that LLMs are bad at writing specifications. What changed between that time where you saw that they were like a year ago they were pretty decent at doing it or they had signs and now we have a bit more proof they're not as good?

Speaker A: So what I wrote that it was really good at was fixing syntax errors which is really big because that often trips people up. It's good at understanding error traces which is huge because being able to take a 35-step error trace and turn that into two paragraphs of English text, major improvement. Good at boilerplate like mass changes to a bunch of small things like updating boilerplate, and it's okay at writing properties from a very precise description. It's bad at fixing specs and it's real bad at providing properties for a spec. Ha, I'm still consistent.

Speaker B: Yeah.

Speaker A: So, I think I called that early back then that it is really bad. It's good at translating properties from precise English into a spec, but it's bad at coming up with properties on its own. Everything I got back was trivial. I understand you're too cold with the implementation details. So I think ultimately what I'm going to say is that I think it has a lot of potential to improve things, but even back then in 2025 I was noticing that it was really bad at this one thing that it continued to be bad as of March of this year.

Speaker B: So then how much do you think you really need to know formal methods to be able to use LLMs to help you at all? You need to get the basics in place likely.

Speaker A: I think getting the basics in place is really valuable here, right? Because for one, I mean, even discounting being able to write the properties and all that, you need to be able to tell when the AI is doing something wrong, right? And if you don't know the basics, you can't really do that very well.

Speaker B: In your book, Logic for Programmers, you argue that formal logic is probably one of the most useful parts for day-to-day engineering. Why is this?

Speaker A: First of all, I'm honored that you've read my book, or at least the early drafts. I mean the official answer is because logic teaches us to work with booleans and statements what we learn in elementary school how to work with numbers right essentially there's not a whole lot of difference between knowing that 1 plus 1 is two and true and true is true it's still the manipulation of values and it happens that booleans are so important to software engineering that having some formal grounding in that is very handy especially when we are not taught that in school for the most part. The other answer is that I've just on learning logic and getting better at logic and teaching logic a lot as part of teaching TLA+ I just finding more and more applications where I'm like oh because of logic I can do this one thing and I find that people who don't have that background struggle to do that one thing. I guess I'm saying that empirically logic keeps coming up as a useful form of math.

Speaker B: And if I'm a software engineer and I work on complicated distributed systems, what techniques would you recommend that I look into to harden these systems? We can assume that I'm already doing basic unit testing, potentially integration testing, but I'm now interested in like, well, should I look into formal methods, property based testing? If it's formal methods, there's all these different technologies. It's almost overwhelming. What is a good place to start to just do some experiments that are cheap to do?

Speaker A: I'm going to just completely go 90 degrees here and recommend this book by Nancy Leveson called Engineering a Safer World. She was an aeronautics engineer who investigated things like the Therac-25 radiation case and the Columbia disaster and she was really fascinated in how systems have been accidents and why accidents could happen in complicated systems and I found her writing on this to be incredibly insightful and incredibly valuable in understanding how these systems can break. So that's the thing at first I'd recommend is checking out that.

Host: book. looking ahead for the industry a year ago. You wrote a post where you shared some of the uncertainties and anxieties. It was a longer post. Uh it started with how VIP coding will be never good as software engineering experienced software engineers and you wrote six different things. Can we read through them and and just reflect on how you feel about them? What you think might have changed and and maybe talk about what potential new anxieties we have because there's so much change going on. That's for sure.

Guest: >> The way I sort of think about it is that the next five years keep being rewritten every few months, >> right?

Host: >> Yeah.

Guest: So I wrote the following can all be true. One, bibec coders will never be good at software engineering as an experienced software engineer. Probably true. I mean, if you don't have the basics, you can't really

Host: >> It feels true. I I I even see it on myself when I try to build a software in a domain I'm not an expert in, like a game, and it's an absolute just vibe coded mess.

Guest: >> Yeah, LMS can significantly augment a sign a professional software engineer's ability to quickly write high quality software. I think also true. I mean, even if you don't have it writing a single line of code, just being able to be like, okay, what's this bug? Where's the bug? Or like, hey, what library should I look into to solve this problem? And we're I think we're starting to see or starting to recognize that engineers who have really deep knowledge are so much more efficient. And the ones who embrace these tools and figure out how to control them and not them to control, you know, like like their anxiety or whatnot, they get a lot done.

Host: >> Absolutely. Elements will cause many software developers to lose their jobs.

Guest: I don't know. That's a hard one to pin down because like I mean one the software engineering at least in the US is starting to recover. Like we're starting to see more jobs open up for software development. So it's hard to tell how much of like the loss of the past few years was AI versus the end of like zero interest rate policy and like the postcoid crash. And I think it's more the latter but like again LM are still getting better. Maybe they're going to cause job losses in the future.

Host: >> Yeah, this is a noble question. the data that we had in the pragmatic engineer it did show that we are seeing overall more software engineering openings in the US in Germany and France they're declining a little bit at the same time and there seems to be a big shift on who is being hired and the skill set so now AI engineering is increasingly spreading to more software engineering fields not all of them and we're seeing a decrease in for example front-end engineering hiring mobile engineering hiring so I think the shape is changing but it's always changed in the past if you think about 20 years ago the most in demand engineer was a Java engineer like Java specifically like don't care 10 years of Java experience required and that's changed >> okay then we'll open up new jobs for many possibly far many software developers

Guest: I think that's also true I think when you basically need one developer to make your product as opposed to five you're looking to hire one developer right

Host: >> that's been true yeah y

Guest: >> the software jobs that LLM open up will be lower paid to lower precision the heights of the 2008 to22 tech era and that's the thing that scares me the most is that as mentioned I decided to leave a field and just become a techie. And I was able to do that. And I was able to get a well-paying job that led to me to now full-time mathematically prove systems correct. That's crazy. What other field can somebody just go like what other engineering field like I want to be an engineer and just walk straight into it? What other field is going to send people to Budapest from the US to give a talk for 45 minutes? Like it is really precious and magical what we have here and I'm afraid of losing that. I'm afraid of a place where it just becomes like any other like white collar job where you get two weeks paid vacation every year and like two days off sick and I don't want to lose that.

Host: >> Are we saying we're afraid that software engineering might become just like every other engineering job? Yes.

Guest: >> Because that is the reality of a lot of engineering jobs. We do have a privilege. I I don't think we talked about it when we compared with the rest of engineering. We have massive privilege.

Host: >> Yes. We have a huge amount of privilege and I don't want to lose that and I I mean it would be nice if everybody else got the same things we are but I don't want to like equalize us by losing what makes software engineering so magical and precious.

Guest: >> Yeah. So this is a worry.

Host: >> Yeah. That's my that's my fear.

Guest: >> And then number six >> there will be still be high paid professional software engineering jobs but they will be rare, more competitive and more and less developer friendly.

Host: >> I'm afraid we're seeing some of this already. I I wonder if this is inevitable. Um I also see it in some other industries. For example, with investment banking, uh the the traders used to be many of them very highly paid, highly respected. There are now fewer of them still highly paid, highly respected. It's harder to get into them.

Guest: >> Yeah. I mean, I think I think like most jobs do oify over time like as like the standards are set and more people enter them. Um sovereignty I think for a longer period of time was able to like get away from that.

Host: >> Yeah. And then and and then you closed your prediction uh with with with these lines a year ago.

Guest: >> I predict that in the next 10 years software development will survive, but it will become like any other white collar professional work. No more $200,000 salaries, a lunification, or incredible employee bargaining power. I feel sad that we'll lose something so magical, but I guess it couldn't have last forever. Automation comes for all of us, even us automators. Here's a crazy way of ending this actually fits in the backling. If we start with automation comes for all of us, even automators. And like on one hand, I feel like I'm losing something really special. On the other hand, a doctor friend of mine came to me like a few months back and was like, "Hey, we managed to like create a new shift scheduling platform for like our hospital like to trade shifts that really saved us all a lot of time and like made all of us nurses and doctors so much happier." And I was able to just vibe it out. I don't know any kind of code, but like AI let me do this. And I'm like, "Wow, it really is helping you like in your hospital make your life better." And it's like it it feels so weird to balance my needs as a professional software developer with like his needs as a doctor. Like who matters more? like my cushy job or his job. Like I I don't know. And it's going to we're going to all find this out in the next 10 years. I guess

Host: >> Grady Woo told me that this time reminds him of the time in the 19 late 1960s and early 1970s where people could purchase computers and start to hack with them. And he said it was a magical time because teachers and people who had nothing to do with software saved up and start to just hack around and it democratized it. And I feel this is the first time I'm also feeling like this other person in the gym told me that they're vibing something together. It feels it's opening up the field and if anything a lot more people are realizing, oh software is cool. I can do it and now they're starting to learn the hard parts of software engineering eventually.

Guest: >> Did you ever read up Clay Sher's essay situated software?

Host: >> No.

Guest: Basically what it is is that this person was talking about um how they think like the most important the vast majority of software should be made for like three people or like a family or community or like one school. And up until now that like could only really happen if one of those people in that family that community that school was like really really into computers. But now it's possible for everybody to have situated software and that again is going to change the world in some strange and some terrifying and some exciting ways.

Host: >> It's exciting. As closing, what are books, a

Host: few books that you could recommend that you have enjoyed or made an impact on you?

Hill: >> Oh boy. Let's just leave this just for this into just software books, okay? Because otherwise we're going to be here for like a month. So there's three books that I really love in software that I think of as like the books that have influenced me so much.

Hill: The first one I think I mentioned in the interview was um Nancy Leonson's Engineering a Safer World. I believe that's actually free online. The second book is called Data and Reality by um Bill Kent.

Hill: And this one's actually hard to find because it was republished in 200 I think 11, but the republisher changed the book. So the last good edition is is the second edition which can be found like in dark corners of the internet online is actually kind of hard but like it is basically by this like famous database designer who like worked on like IBM databases who was just asking like what is data? What does it mean for something to have identity? What does it mean for something to have oneness? If we talk about a book is that the book the physical copy is that the series is that an addition?

Hill: And it's just an entire book about these questions about what data is and how we need to represent it. He ends it by saying that data isn't reality. It is our view of reality for our useful purpose. Incredible book. It totally changed how I think about things.

Hill: The last book is um called debugging the nine simple rules by David Aens. And it's literally just like a book of war stories about debugging and like basic principles. But this is the book I give to every junior engineer because I think like nobody ever really talks about debugging as like a discipline outside of like basic heristics.

Hill: this is like just at least something that's trying to do that and having something is better than nothing in this category. So really good book and I think it's like $10 for a used copy. So like anybody can just get one. It's great. Those I think are the three most useful books for software engineers. If you want to talk about other books I can keep going but [laughter]

Host: this this is great. Well hello this was very educational and I found it fascinating. Thank you. Thank you. I really enjoyed this conversation, especially the demos where Hill showed tools like [music] TA+ alloy or hypothesis and how they can catch bugs.

Host: By the end of the conversation, I'm starting to understand more why it's not likely that formal verification will go mainstream even with AI. I mean, these tools feel very rigid for the real world. For specific parts of a system that you can model mathematically, like state spaces, sure, they can work, but for everyday programs, it just feels like it would be a bit pointless to create TA plus specifications.

Host: One thing that I was also thinking about is how Hill talked about why he thinks we're not good at catching concurrency bugs, and it's because we don't have much practice with them. [music] As a developer, you're lucky to debug a concurrency bug once every few years. So, of course, you won't be able to build expertise [music] this way.

Host: This is also similar to how most engineers are bad at migrations because most devs only ever do one or two migrations over several years. But if you're an engineer who does a bunch of migrations, you're going to be really good at them. Same thing if you're working on systems with concurrency issues and you become an expert in this.

Host: I also find it fascinating how other engineering fields have similarities with software engineering, like how mining engineers had their own agile revolution in the 1960s and how all engineers hate the concept of waterfall. [music] Plus, it was amusing to hear how source control is kind of an envy from other engineering fields that we software engineers have, but not many others do.

Host: Check out the show notes for related deep dives on distributed systems at TechDEP that go into more detail into the topics that we talked about today. And if you've enjoyed this podcast, please do subscribe on your favorite podcast platform and on YouTube. A special thank you if you also leave a rating on the show. Thanks and see you in the next