Re-Designing Data-Intensive Applications: The Shift to Cloud-Native Storage

Welcome to the Bug Bash Podcast, where we talk about all things software correctness and reliability. I'm your host, David Wynn. It's been nine years since designing data intensive applications became the standard text for distributed systems. Today, Martin Kletman and Chris Rickomini joined the show to pull back the curtain on the upcoming second edition. After all, the era of local disks is giving way to cloud native objects storage, so we discuss why modern databases are being entirely rebuilt on top of S3. From there, we revisit the cap theorem and why it might be time to retire in favor of offline availability. We also get into a surprisingly practical debate on AI, exploring how LLMs might be terrible at creative design, but perfect as test miracles for verifying complex system migrations. You'll want to stick around for this one. A quick word before we start today's show. If you're looking to connect with other folks in real life who care about software correctness and reliability, consider attending the Bug Bash Conference, April 23rd and 24th in Washington, DC. All the details are at bugbash.antificis.com. Alright, welcome to the Bug Bash Podcast, everybody. Today we've got a really exciting pair of guests. The second edition of everybody in the world's favorite book, at least everybody in my world's favorite book, designing data intensive applications, aka the book I wish I had had when I started writing distributed systems, but I didn't, so I had to make all the mistakes the hard way. Welcome Martin, welcome, Chris. Thank you. I feel like there's so many possible things that we could talk about, but I think one question I have is like, I was obviously a little bit hamming it up for you guys, but I think it is fair to say that designing data intensive applications has kind of turned into the distributed systems practitioner's Bible. It's just the book, like anytime I see anybody asking for recommendations about how to learn about this very tricky and complicated subject, it's always the first recommendation I see. And I think that's with good reason. It's really, really good. And it's very comprehensive. And I'm just curious, like, was that your intention? Like was was the goal to make it that big or did it happen that way by accident? And if so, why do you think it did? I mean, we've been speaking to that since it's about the first edition. Yeah, so it didn't really intend to make it quite that big. I think the original target was for 400 pages and then it turned into 600. The really, I just wanted to like try to write the book that I wish I had had myself when I was getting started with all of this. And I just found that whenever I was reading up about things online, I would run into some articles that like either were like, you know, super deep research jargon, like really hard to understand or really vague marketing fluff that's sort of trying to get you to buy some product, but sort of, or just really explain the substance of it, right? And so to get something in between, in between those two extremes. Did anything surprise you about the reception for the book? I mean, you seem like a very understated person. So I would assume that you didn't expect it to become quite as popular as it has become. But are there sections of the book that got a better reception or a worse reception than you expected? I mean, on the whole, I was expecting, you know, this is a very new thing like who cares about distributed systems. Like fairly specialized stuff. And I was thinking that, you know, like the most people who just using a database, they don't really need to know things. That level of detail they can just use the manual of the database and, and help me find it. I was mainly aiming at the sort of person who like maybe needs to make the choice as to which database system to use for a particular application because there are so many to choose from. And so I thought, you know, that'll be a small number of like senior architects and that, that sort of style of person. I wasn't really expecting just like this would become such a comparatively mainstream thing. Yeah, I think one thing that makes the book really successful and that I personally love about it is it's actually not just a book about distributed systems. Like it's, it's, it's written that way. But it actually like communicates some pretty deep wisdom about designing any kind of system. Like maybe, maybe not even just software systems, right? Like it's, it's actually like in some ways like a collection of very general engineering wisdom sort of expressed through the lens of distributed systems. And I think that's one way in which you've kind of, as you said, like merge these levels of abstraction very successfully. I don't know anything else quite like it. Yeah, and I've sort of really wanted to make it real like by having a lot of case studies and connections to like real stuff. And it's, you know, when you hear these delightful stories like that, subsea cables are getting interrupted because of shark bites or stuff like that. And it's just, yes, like I have to put that in. It's just, of course, it gets then packaged into like trying to figure out what are the general principles that we're trying to explain here so that it's not just a collection of anecdotes but really trying to like generalize out from those. But I think enriching it with those little nuggets, I think kind of, you know, it makes it more real and makes people believe that, you know, this is how real systems actually work because it's got sort of these stories of hard one wisdom in it. And you know, I've spent time going through various post-mortems of production incidents and like saying, okay, like is there an interesting moral from the story that we can extract here and fit into the narrative somewhere? So why did you guys decide that a second edition was necessary and, you know, what are you most excited about in the second edition, you know, what's changed the most, you know, what I guess was changed in the industry was changed in the book. Yeah, so the, I think it was pretty clear of all wilder to second edition was necessary because the first it was just getting a bit dated. It's now nine years old. It came out and then actually the first few chapters I started writing a few years before then, so the, the first few chapters are probably like 12 years old by now and stuff changes in that time inevitably. I did try to focus it as much as I could on general principles rather than like the latest version of the latest piece of a particular software, so there should have some longevity, but nevertheless stuff changes. So one of the big things to change, for example, is that the first edition basically assumes this model where a node in a distributed system is like one machine with some local disks and if it wants to store something, it stores it on its local disk and if it wants to replicate something, it sends it over to network to another machine. That's sort of basically the assumption it makes. But now we have these cloud native systems where actually maybe you're not writing to a disk, maybe you're writing to an object store and other object stores itself, this distributed system that were layering services upon services upon services and that's, that became clear that like it was really important like fundamental design change right down at the foundations of the way that people build practical distributed systems and data systems and we have to reflect that somewhere somehow. Why do you guys think that happened? This is, this is so true. This is like a huge change in everybody's assumptions about distributed systems architecture. Like back in the stone ages when we were doing it, it was like obviously you will have a super super fast SSD on the computer and you will optimize your storage engine and your your system to like use that super fast SSD. And now everybody is like obviously you will have super high throughput access to disaggregated object storage and rely on that for everything. And that is how every modern database is getting built. So like what many things changed? What do you think was the, what do you think were the key ones that made everybody switch? Chris, I think you have like particular opinions and expertise in this area. I was just going to hand it with Chris. So this is speaking mostly from personal experience, but the attraction to cloud systems to me has always been like I could pay someone else to be on on page or duty. Like basically it's an operational question. And like if I could pay someone to not have to, so I don't have to worry about replication and network partitions and my notes can't talk to each other anymore because somebody's doing maintenance in the data center and I'm getting page three in the morning and there's corruption on this. Like that stuff is just not fun. It's just painful, right? And so I think that's true on both the compute and the the persistence side. So being able to kind of voice that off into a third party and have them, you know, some of the throat to choke, so to speak, is really nice. I do think it's a bit of a mirage in some ways because now your cloud systems don't work anymore and you have to go and figure out what like, oh, who changed the access control on this bucket or who, you know, who did this random deployment or why is this system degraded, you know, and it turns out there's some noisy neighbor or something. So it's not a solution, but I think the allure maybe 15 years ago was like, oh, this is so much better, I can just have an endpoint to call. So that's my perspective on it. You know, I think there's obviously some trade offs cost being one of them. But yeah. Do you think the shift would have happened as quickly or in the same way if S3 had not added strong consistency? Well, you know, Simon, I'm going to bush yours last name, Eskilden, the turbo puffer founder has an excellent talk, I'm blanking on the conference name. It was a year or two ago where he actually runs down the timeline for some of the major changes that led to a system like turbo puffer being built the way it was. And one of the things he points out is actually, they didn't, S3 particular didn't get strong consistency, consistency until like very late. I want to say it was later than 2020 even. And so my argument would be yeah, it would already happen to be for strong consistency was built into S3 in particular. You know, those of us living in Google Cloud Storage land had that much earlier. So I'm a bit of a GC in Google Cloud Storage and Google Cloud fan, but anyway, I digress. So yeah, I think so. I think it would have happened regardless. And I think even without S3, it would have happened being able to get machines on demand and all that kind of stuff and Kubernetes on top of that and EBS, right? These are all systems that are just really pretty incredible when you take a step back. Well, maybe that I think having the option of strong consistency and being able to do like a essentially an atomic compare and swap does enable the distributed systems built on top of the object store to be quite a lot simpler than they would otherwise because essentially you can outsource your consensus to the object store. And that is like a really nice simplification that's like, you know, previously people would have to use something like ZootKeepo or LCD in order to outsource their consensus to another system. And so having it integrated into the object store, I think can be quite a big simplification there. Yeah, it's incredible. You know, we I started working on a project a couple years back, which is basically like a key value store that's built on top of object storage. And it's inspired by TurboPuffer and WarpStream and so on these cloud native databases, so to speak. And lately what we've been discovering is, hey, you know what, we can actually rip this part into constituent components and provide like a transactional object that automatically will do fencing for you because it turns out doing fencing on top of an object is like trivially simple if you have compare and swap. And oh, we can build a distributed queue on top of object storage, which is something that TurboPuffer actually just posted about, which is again something on our compactor that we're looking at is like, oh, this is basically a distributed queue to distribute workload for compaction. There's like on and on with these these kind of things. Oh, we can build a right head log and just have that be a separate thing like wall three with Chroma. So I think Martin's 100% dead on it. Like once you get that, you know, precondition set up the way that S3 has and GCS and so on, you can basically build all these primitives really, really easy and then compose them in a bunch of great ways. Yeah, we, um, we had an synthesis actually have built our own analytic database engine, um, basically because for some weird reason, nobody else's analytic database in the market allows you to have a data model where time is a thing that branches and forks as it goes forward, which is very odd. I thought everybody lived in that world. Um, but, but basically we, we decided we had to do this ourselves, but the key enabling technology realization, I mean, one was that we have a very, very easy way to test it that works very well. That reduced the development cost a lot. But the other, the other really was just understanding that you don't need to write your own storage engine anymore. And that is just like, I feel like that is lowered the barrier to entry so much for doing this kind of thing. Yeah, 100%. I think, you know, if you could sort of look at a database stack, it starts, uh, sort of well, at the persistence layer of some sort, but the layer above that that you're kind of alluding to, I think is probably something like data fusion or duct DB. And then you have these great files formats. You can use like parquet and, you know, on and on, Lance and nimble and stuff. And so you can now, I'm not going to say easily, but you can, it's definitely viable to stack these things together to make an analytic database in particular that's actually pretty stellar. I think, uh, polar signals did something similar recently. They've been talking about it as well. Um, it's like definitely a viable thing. So it's very cool. Like, can you, can you guys tell us a little bit of the co author story? Like the book has been around for Martin, as you said, like about a decade now. And Chris, I think at that time, you were at we pay, is that right? Actually, I was at LinkedIn. Uh, sitting next to Martin, Martin, I'm on sabbatical. Well, so you guys tell us like, how did you, how did you guys come back together to bring V2 of this project to life? I mean, maybe you should talk about how we know it in the first place. Um, so yeah, Chris was at LinkedIn working on, uh, SAMSAR at the time, the stream processor. Um, I had ended up putting LinkedIn through the acquisition of my previous startup. Um, but after a while, our team got disbanded. I needed to find a new team. Um, I'd heard that, oh, the Kafka folks were doing really interesting stuff. And so I got in touch with Jay and said, hey, can I work with you and do, um, do something here? And then he introduced me to the SAMSAR team and so, uh, got, uh, working with Chris then. Yeah. That's, that's about right. I want to say that was like 2012 or 2013. And so, yeah, wind up with just about, I think when you were working on that first few chapters of the book. And I remember actually, after you went on sabbatical, I got an email from you and it was like a PDF of the first couple chapters and everything. I was like, oh man, this is, and at the time it was still a very chunky couple of chapters. Um, it's, it was cool to see it kind of evolve and actually get published and have the reception that it did. Um, but yeah, that's, that's essentially how we knew each other is working on SAMSAR and being at LinkedIn at the same time. Yeah. And then, um, LinkedIn was very kind to give me, uh, like 50% time to work on the, on the book. So I was then 50% software engineer working with Chris and the other half of my time, uh, trying to write the book, but then realized that actually trying to do those things. Those things at the same time is really hard, especially like, you know, we were putting SAMSAR into production. And there was constantly like production things to worry about. And so it's quite hard to switch off from that and then focus on like a multi year writing project in parallel. Um, so then I ended up, uh, yeah, taking a sabbatical and just, um, on my own dime, uh, focusing full time on writing the book. Uh, and then I somehow slid into academia. Um, I finished the, um, I, so I got a job at the university where I could do some interesting research and finished the book, um, at the same time. That turned out to be a bit more compatible. Now I've stayed in academia, but, um, when it came to writing the second edition, I started writing the second edition by myself. Um, but then at some point realized that I just, I had fallen quite behind on what current industry practices were because, you know, I had retreated into my ivory tower of academia. Um, and so like while I was reasonably up to date on sort of 2014 era technology, I just totally missed out on what had happened, uh, since, um, but I, it's like, I hadn't really stayed in touch very actively with Chris, but, uh, you know, Chris wrote a great, um, blog and use letter. So I kept getting some, uh, useful insight from that. And then at some point it occurred to me like, really, I should just bring Chris on board as a co-author. This, this would make so much, much more sense. So then I just sent Chris an email saying, Hey, is you interested? And he said, yes. So you guys have both done the startup thing and you have both been cogs in a giant soulless corporate machine. And Martin, you have also been in academia. Can you, can you both give us your hottest takes comparing and contrasting these various lifestyles and, and ways for a, uh, enterprising computer scientist to make a living? Well, Chris wrote a whole book on, uh, sort of getting started as a software engineer. Yeah, I'm trying to think of a hot take though. Um, Luke, Luke warm is fine too. Yeah, I guess, um, my, my hottest take is, is the size of the company doesn't, which seems to be kind of the backdrop of the question. It doesn't, doesn't necessarily matter all that much. I think there are, you know, working at a company like Google is very different than working at a company like JP Morgan Chase, even though they're both massive corporations, right? Um, I think in some sense, uh, one of the things I find myself optimizing more when I think about, uh, work in my career is, uh, is, is the, the company sort of tech oriented engineering driven, you know, aligns with the, the outlook that I have because where I find that I struggle the most is when just culturally my view of the world differs just fundamentally, right? From a, like when I landed at JP Morgan Chase, they're bank, they're a financial company. Technology is a tool to them. And I get that. And that's, you know, arguably the way that it should be for them. But like technology is like a passion in my life. You know, my view and excitement of things is a little bit different than theirs. Working companies that align with, uh, are compatible with the things you want to work on and, uh, you know, your view of the world is really important. You know, I had one of my employees, um, that worked with me at Weepay and ended up at, uh, Clickhouse. And she, she was telling me, I was having coffee with her and she's like, you know, it turns out like if you're really passionate about databases, like you should work for a database company and I was like, that is like, uh, shockingly insightful and, and shockingly non-obvious. Um, and so that's sort of my, I guess, hot take is like, don't worry so much about the size of the company. We're worried about sort of the values and outlook that you have and how compatible they are with the company's, you know, leadership and direction. Now my perspective there's, uh, LinkedIn was the only big company that I've ever worked at. So I really have very little comparison there. Um, my, my feeling is that, you know, they, they were fine. I think they, they did a lot of things right. Um, but I didn't really fit into that sort of big company corporate style because, um, I sort of had a lot of opinions on stuff that I wanted to do and I was kind of more happy sort of prototype, exploring things without like having predefined okay hours or that sort of structure. Um, this just doesn't fit my temperament that well. Um, so, so start up suited me fine because they're, you know, we're just sort of wildly trying a bunch of things and no idea how it's where it's going, but, um, at least we're exploring something academia suits me fine because it, you know, the research, it's, uh, very free, very open end is the difference is there maybe just one of timescale really that's like in a startup you're trying to ship things like on the timescale of weeks to months. Um, on, in academia, I'm free to think on things on a timescale of years to decades and, uh, that's something that I rather value now that, um, you know, I can just work on things that I believe are important without it having to be a commercially viable thing right now. Um, but I tried to still sort of bring a bit of that startup mindset into my research, um, so that, that focus on making something that's actually useful, you know, that's, that's something that sometimes gets forgotten in, in academia. Um, and sometimes, you know, very fundamental research sometimes doesn't need like a practical use case, but I tried to keep my research quite anchored in, in practice. And so that's, that's sort of my, my startup route showing through. So I remember when you first went to academia, I think we had a conversation and you said that you were working on using CRDTs and data structure like that to enable privacy preserving collaboration tools. Is that still what you're working on? And has that, how did that project go and, you know, what did you learn from it and, and so on? Yeah, it's, it's basically still ongoing. Uh, it's been 10 years or so since I start working on that and that's, that's what I mean with timescale of decades. Um, there's just a bunch of really hard problems that actually just take a really long time to solve. This is the last company that will ever criticize you for taking a long time to work on something. We've, we've got this three years. Yeah, so, um, so you know, I set out saying basically I want, I want something like Google docs, but with end to end encryption and decentralized so that we don't have to rely as much on Google servers. That was basically the essentially the premise that I started out with. Um, and then I started doing a bunch of work on the CRDTs which enable that decentralized collaboration. But for example, the end to end encryption piece that's only just coming together. So, uh, like only just within the last year or so, um, my collaborators at Incenswitch have been building a, uh, a library called Keyhive, which, um, extends with our auto merge CRDT library, um, to add into an encryption and decentralized access control, uh, based on some cryptographic identity system. Uh, and so, you know, it's been, it's been a long process there and even that is still by no means finished. It's still, you know, the software isn't even properly released yet. Uh, we really need to do some formal proofs to verify that the, that it's actually correct. Um, and, uh, and actually putting it into practice is still going to take another couple of years, I think. But that has been like essentially something that I've been just gradually tugging away at, uh, little, little project by little project prototype wise, just gradually over the years, making the data structures more efficient, um, making them do stuff that they couldn't do before, um, informed by the needs of, of collaborative applications. You mentioned, formal proofs, which is always something that's interesting to us. Like one thing that is striking to me as, you know, someone from industry is that formal proofs generally speaking like loom large in academia. But I just kind of rarely see them used in everyday industry software projects, especially once a project is off the ground and is then being actively like extended and maintained and performance optimized, even if there was a proof, like I don't really see people returning to it. Uh, what has your experience been? I know Chris, you all use Fisbee in slate DB, right? Yeah. It's a part of a suite of things we've tried. Um, so we use Fisbee initially to define, um, our manifest management protocol for our, or, or maybe just for listeners, can you explain a little bit about what Fisbee is? This thing I mentioned earlier, this key value store, uh, that is slate DB. So it's, if you imagine rocks DB, which is a key value store, uh, that sits on a single node and you can get put delete scan data. Um, it's that, but it, it persists all its data on object storage so it can run without a local disc at all if you, if you like. Um, and under the hood, it's, uh, using a storage sort of strategy called a log structure at Merge Tree, um, which is like actually a very simple, pretty straightforward way to build a database. All your rights just get appended to a log. And then periodically you read over that log and you try to, what they call compact out, which means deduplicate any duplicate keys you have so that you only have the latest version. That, that action is called compaction. That's like pretty much it. Um, and that's both a vast oversimplification and also like pretty true. Um, and then in that context, what is Fisbee? Yeah. So how do you use it? Fisbee is a, um, oh gosh, you might be able to define it better than I am. I believe what they would call it is a, uh, formal proof system. Um, but I think there's like model based testing aspects to it as well. There's like all these subgenres of formal proofs. Um, but the, the gist of it is, it's a little language where you can define, um, the behaviors that you believe to be true and the, the behavior of your system. And then you can define, um, you know, expect it outcomes essentially and it'll run through all the different, um, states of your definition and verify that, uh, your, um, invariance hold. So for example, if I put a key into slate DB and then I call get on that key, I should get the value back, right? 100% of the time, no matter what happens, right? Now under the hood, slate DB is doing a lot of stuff. Like I said, it's writing to a, uh, right ahead log. It's compacting data. There's a whole bunch of other stuff that it does. So what Fisbee will do is it'll, uh, run that, you know, simulate that put and it'll run all the different variations of pathways in the code that slate DB could, uh, execute. And then it'll check back and see in all those cases, if I call get anywhere in that flow, I'm always going to get the value back. Now what one of the things I said there was in the code, the truth is, uh, Fisbee and most of these other systems, TLA plus and so on, um, don't actually tie into your code. So you're defining in this sort of Fisbee language, um, how you believe your code to behave. Um, and so it's really good for testing designs, um, but it's, it's, it's more, uh, difficult to test the actual implementation that you have. Um, now JP, the author of Fisbee has recently added some model based testing aspects to it where it actually has a little framework with an API where when you define your model behavior, it'll give you a little hooks in like rust or, you know, Python or whatever. And then you can plug in your actual code. Um, and so you can kind of merge the two, but in general, there's sort of been this barrier between the design and the actual implementation. Um, I think that gets to one of your earlier questions about like you, you rarely see this used, especially once your system is like off the ground, right? And the truth is, like once your system's off the ground is changing constantly, it's dynamic. There are many other ways to test. You're getting bug reports, you're getting feature development stuff. So oftentimes I feel this stuff kind of falls by the wayside just because it's, it's, it's not low overhead to do. Uh, most of these languages are very mathematical in nature. Um, that's one of the reasons we chose Fisbee is actually it uses a language called star arc, which is like a watered down version of Python, which is actually approach, approachable for a developer versus some of these other languages. Um, and so I could go on about it, but I'll pause there. Yeah, should I? Yeah. So as Chris already said, like there's this distinction between like verifying things about a specification versus verifying actual implementation. Um, and most of the value I also think is actually in verifying the specification, uh, checking that, and that's more about actually check using the computers of tool to check our own thinking, whether our own thinking about how a system is supposed to behave, stands up once you consider weird edge cases that you might have not thought of as a human. And then once the, uh, once the specification works and we've tested that, um, it behaves the way we expect, then I feel most of the value has been gained already. Uh, at that point, yes, bugs could arise when you translate it into an implementation. Um, but then the added effort that it would take to formally verify the actual implementation, as the specters often out of proportion with the benefits you would get. Um, I mean, I think doing some like property based testing on the actual implementation is really valuable as well. That's kind of a comparatively low hanging fruit. But if you wanted to like actually use a proof assistant to, uh, you know, actually prove something, so not just model check it, but actually like formally proved theorems about the code. That's just a ton of work. Um, I'm sort of cautiously optimistic that, um, LLMs would, would get good enough at writing formal proofs that we can just outsource all of that, uh, to an AI agent. And then it doesn't matter if it hallucinates because, um, the proof checker will only accept the proof if, if it really is rigorous. Um, so it seems like a really good use case for, um, for LLMs, but I haven't really tried that myself yet. So, um, I have the suspicion that the AI tools may be able to help with making, um, those kinds of verification things more mainstream. But for now, um, in the world of proofs written by hand, actually writing them by hand is just, just really hard. And so all of the, uh, I've done some, uh, formal verification work with the Isabelle proof assistant, for example, which, so unlike a model checker does allow you to formally prove things. So it's, you can reason about infinite state spaces, for example, improved that really in, in all the possible situations, something will be true. Whereas in, in a model checker, you would have to test some bounded, uh, bounded limited subset of a state space. And, uh, and yes, writing those Isabelle proofs is just incredibly time consuming. Um, but it's valuable in those places where we're trying to design a really subtle algorithm and we have no idea if it's right. If we don't actually prove it and then actually the process of going through and writing the proof, that is what helps us understand why or why not the, the algorithm works. The fact that you get like a proof artifact at the end is kind of then a convenient side effect. So actually the process of writing the proof is not because we want the proof at the end. It's because in our heads, we want the understanding that we gain from having written the proof. And, uh, and that is something that I've come to value quite a lot about these proof assistants. So even though it's terribly time consuming, but I found it's, it has sharpened my own thinking tremendously to have to write a proof step by step that the stupid machine will accept that the proof really is true because so many times while writing the proof, I've then run into things where I think, yeah, this is obviously true and then spend half an hour trying to prove it and then realize, no, there's a counter example. So, so actually the process of writing proof has just made me better at just thinking about things through in a sort of structured way, even if I'm not actually using the proof tool anymore. It's just made me better thinking about things and that is something I've come to value quite a lot. That's an interesting. So that makes a ton of sense to me. We're like so many complicated cognitive tasks. Like having a way to force yourself to think step by step and rigorously makes your thinking better and sharper. Exactly. I'm really curious how that contrasts with this idea that maybe LLMs can write the proofs for us because if a lot of the value is in the writing and the struggle and the thinking, do we still get the benefits if I can push a button, walk away, have a coffee and come back and then just have my Isabelle proof waiting for me? That's a very good question. I don't know. I guess we would have to try it. I mean, at the moment, a lot of the time spent writing the proofs is actually very frustrating because it's just like trying to figure out exactly what is the right inductive hypothesis to use for this thing so that I can then get this lemma over there and then that and then is just hours of grinding away on really minor lemma's where I'm just trying to prove associativity for list append, it's obvious. Why should this be so hard? That kind of thing. So, I think if it can just take out some of that drudge work and allow us to focus more on the high level steps of the proof, I think that will already be a tremendous gain in terms of partly just making less frustrating and time consuming to write these proofs partly enabling more people to write these proofs without having to have had to go and do a PhD and spend years learning the various arcane proof tactics that these proof assistants have built in. So I suspect it's probably the net benefit if we can automate more of it. So one of the speakers last year at Bug Bash the conference was a guy named Uncle Shesai who's then at AWS now it's no flake. He's the developer of a formal methods language called P, which is specifically optimized for reasoning about distributed systems. He gave a fantastic talk, which you can look up on YouTube, which serves at an even more extreme version of what you're saying, Martin. I think he actually said I made me miss quoting him, but he basically said like I get 90% of the value from formal methods before I run the model checker. Like that's almost just like an afterthought. It's the value of the method is that it actually forces me to sit down and think about what I believe my system does, which it's frightening easy not to do otherwise. So something that we've done here, we actually do use a little bit of formal methods inside of antithesis, which I think surprises people sometimes because they think we're anti-formal methods were really not. We use proof-based techniques quite heavily in all the security critical parts of our systems where they're really what you want to use. One thing that we've sort of done is taken on cushions advice there to heart. We basically have a semi-formal proof that is not machine-checkable, but that is human checkable because it has some definitions and some terms that cannot be reduced to a completely logical description. But it still has the sort of overall semantic structure of a proof with lemmas and implications and quantification and so on. And so it's actually a really nice balance because it means that we can engage in this like formal reasoning style and catch mistakes that we would otherwise not catch. But it lets us avoid a lot of the like incredibly nitty-gritty annoying arguing with the checker that you've just described. And it also lets us use it in a domain where some of the terms cannot be defined in ways that like a computer would be satisfied with. So I don't know if this is going to catch on or anything, but we've been calling it semi-formal methods and trying to encourage more people to do it. Have people call it like smart casual as well? Like a step down for formal? That's right. What I like in that context is, I can't remember it from somebody said, writing is nature's way of showing you how fuzzy your thinking is. Yes. But then Leslie Lamport extended that and said, "athematics is nature's way of showing you how fuzzy your writing is." And then more than that, proof assistance are nature's way of showing you how fuzzy your mathematics is. That's awesome. Yeah. This whole conversation to me feels like a parallel to just writing in general. Like as soon as you try to write something down in a book, on a blog, whatever it might be in a design document, instantly you're starting to push against your actual mental model and discover mistakes and gaps and everything. So it definitely feels like this could be zoomed out, this conversation and applied to any number of writing based activities. So did you put you guys in the spot? Did you use any AI in the second edition of your book? Not for the actual content, but Chris actually used it to put some pretty good effect. Yeah. They came, O'Reilly, our publisher. They run the offer quizzes in Safari Online Learning area where you can go after each chapter and take quizzes. And so they needed quiz questions for each chapter. And I managed to sort of prompt engineer my way into getting all the quiz questions to be generated through the LLM, which worked surprisingly well. Which in hindsight, Martin was pointing out maybe it shouldn't be so surprising. Like the whole point of it is like this sort of probabilistic, weird, hallucinogenic answer thing. So we used it there for these quiz questions. So if you take the O'Reilly Online quiz, you are using LLM generated questions that have been sort of heavily reviewed and tweaked. On my PR was hundreds of lines. It's hard to know where the LLM ends and Martin and I begin, but that's one area where we used it. I think I used it. There's one summary in the chapter where I took the chapter and I was like, I'm out of gas. I can't write the summary for this. Can you do that? I'm out of the summary and I sort of tweaked it and reworded some stuff because it em dashes everything and every paragraph started with, and then and then next, next, whatever. But other than that, I think where I got the most benefit out of it was really like, I'd write something and I'd be like, what did I miss? Where are my gaps? What is stuff that's incorrect? And so it was sort of like a little in-embrowser helper and checker and editor for me. And I would take its advice and kind of mull it over and think, did I miss this? Should I add this? Is it worth adding? But that's really where I found the most benefit for it was sort of expanding the scope, checking work, that kind of thing. Your O'Reilly quiz example is a fantastic example from my broader thesis that AI excels at satisfying sort of make-work box-checking requirements from large organizations. Like anytime, like, you know, I could tell you in a word, but you are requiring that I fill out a form. I think that's an excellent use case for AI. And this one in particular because it's multiple choice questions. So we need that for each question to be one correct answer and three incorrect answers. So we need something to come up with plausible sounding but incorrect statements. And I find that really hard to do, personally, but turns out it's an LLM is really good at it. That's actually interesting. So I have. So we're actually very interested in using LLM's for testing software, obviously. And one of the things that we've found is that these days, they're so heavily RLHF'd. And if you think about it the way their training works also, they're actually quite bad at generating really crazy and implausible stuff, even if you ask them to. Like sampling them at high temperature has, I think, gotten harder and harder as AI has gotten more sophisticated, which is a little bit annoying to me because even outside of the domain of software testing, what I really want, I feel like the thing that I could use AI for really effectively is just generate a lot of crazy ideas and then use them as inspiration or as prompts for me, my neural network, to decide what to do. And I feel like these days, a mix of economic incentives and also just how is to cast a gradient doesn't work, means that they're actually not that good at that. Yeah, that's an interesting point. I guess where I see myself getting the most benefit from them in the testing area is really in the unit test space, which to your point, I'm not doing crazy things with it. I'm usually like positive case, negative case, like happy path, does this work. And I find it to be excellent for that. But where I bump up against the case you're describing is not so much with testing, but with design, where when I'm designing something and I'm like, okay, I have this idea, tell me the trade-offs and tell me the alternatives I could be doing. It actually doesn't do too well with that. And I think it's the same underlying symptom or cause that you're describing, which is that it can only be as creative as the mean of the internet. So you're always going to get back, more or less whatever, the obvious stuff that everyone else has discussed, rather than sort of the more creative ideas. So that's been disappointing and resonates with what you're describing. I think there's something like a little bit profound here, actually. Take reinforcement learning. I suppose I'm trying to train an agent to play a game of chess. And the way you do that with RL, you are optimizing it for a goal, which is winning the chess game. And what I really want is to optimize for the most variety of interesting chess games that are possible. So you tell me, what is the loss function for that? Like you can't just optimize for like the entropy of the policy or like the entropy of the moves it recommends because making random moves does not lead to interesting chess games. It leads to very boring chess games, right? And so what you want to do is actually maximize like the output entropy at the end of running your model outputs through some potentially non-differentiable system. And that is not a thing that I think anybody knows how to do. And you know, exactly what you need for testing. Yeah, I guess I feel like jumping in because I could argue that if you look at AlphaGo and it's self-play, they didn't change the goal. The goal was still the win go, right? But I think moving from training on the corpus of the internet to something that involves a much more self-play rather than human RLHF or whatever it is, that could be an avenue in which we find and discover interesting and creative things that no human would have come up with, which is sort of like, I forget it was like move 137 or whatever it is in that AlphaGo game where it was shocked everybody. That to me could be a path, but I agree with you like, I don't know how to do that with code. Like, what is the, what is the win go version of like code? Maybe it's some test based thing? I don't know. It gets tricky, right? I don't think anyone's really figured that out for our domain. Well, I think part of this is the irreducible part of like growing up as an engineer, which is like it worked and the test pass is just the beginning of making it good in the way that we're all aiming for. And it's the part of the journey to good that is checkable and has like a clear binary answer like the test pass where they don't. But then there are so many other things that we're looking for like, understandability or looking for some sense of like some intuition about it's likely reliability and debugability and production. We're looking for its ability to be like understood and inherited by future engineers who were not part of building it. And those are all much fuzzier human things. And it's very hard, I think, to write a good loss function for it. I know. That was a very depressing part of me growing up as an engineer where I was like, oh my God, like I'm three years in. I have nailed this job. Like what's next on my assent to, you know, some future career. And it was only like six months later that I looked back just like, oh God, I've made such a mess over the last three years. I need to spend another few years cleaning up after myself. Yeah, that's, you know, we alluded to a book that I wrote earlier, but one of the pieces of advice is like, you got to stick around long enough to suffer from your own mistakes. If you have jobs every two years, you'll never learn the lessons that you're supposed to learn. Someone else will be learning those lessons for you. I have a random question for Martin. I think the very first time I met you was at Strange Loop in maybe 2013 or 2014. And you will be testing. You were presenting at the unconference the night before and you had a talk to a packed room about why the cap theorem is dumb. It was, that wasn't quite the title, but it was like the cap theorem is not a useful framework for thinking about distributed systems or something, something more diplomatic like that. And that was really fun. Yes, I recall it was a really good talk. It was a really, really good talk. There was a number of people there who I know who we all liked it. So I feel like that opinion has become quite mainstream these days. And I think when you gave that talk back in 2014 or 2013, that was like, heresy. And so I'm curious, why do you think you were able to see that? And so many other very smart people were not able to see that. Like what was it about the social conditions at back then that meant that that was such a hard insight for people to get? Oh, that's a really interesting question. It's definitely true that's, yeah, it felt so unharritical. I think I had considered submitting it as a talk to the main Strange Loop Conference and decided, no, this was too controversial, too hot take. I'll do it at the evening event where it's not recorded and where people are a bit drunk and then it'll be appropriate for that sort of setting. But yes, I don't know. In retrospect, it seems to me kind of obvious. I mean, if you read the actual paper that tries to formalize the CAP theorem, there's nothing in it basically. And I asked, do you recall the alternatives? At my point in the career, I was all CAP theoremed out and that's all we talked about. But I mean, it was sort of a framework from which we viewed a lot. I wasn't aware of any alternatives to even question this paradigm. Were there other alternatives at that point? I mean, I think the essential insight which Martin had and which my then boss, now co-founder Dave Sherer also had was like the CAP conjecture by Brewer is like a reasonable conjecture about reasonable things that a system designer might care about, consistency of availability, so on. The CAP theorem, as formalized by Lynch and Co at MIT, redefines those words to mean things that no systems designer would ever care about. And once the terms are defined in such a way, the theorem, as Martin was saying, is literally trivial. Like it's like, of course that is true. And I have learned nothing interesting or new about the world. And yet everybody who was building distributed systems in the early 2010s believed this was like the most important thing that had ever been discovered. And so when I see an entire community of super smart people get something so crazy wrong, I'm always very curious why that happened. You know, like what happened? I think the people like, you know, building the distributed databases, they understood perfectly well what was going on. I don't think they really had much of a misconception. I think it was more that this was the no-sequel era. No-sequel was trying to compete against the dogmas of relational databases of the time and tell people that, you know, actually you don't necessarily need serializability for everything. This is a great theory. Okay, a lot of people wanted to build inconsistent databases. And so they grasped for a reason why that was a good thing, not a bad thing. I think it was a marketing thing really. It was that, you know, there were, say, Bachel building react. They needed to convince people that this was like a reasonable design trade off to make. And my impression is that there's a lot of the cap theorem boosterism came from Bachel actually. And I mean, they did some great work. And so I think for the, you know, for the purposes for which the system was designed, it's reasonable. And they did some great early stuff on CRDTs, which I appreciate. But yes, I kind of feel that maybe they're the sort of the marketing imperative forced people to simplify down on to sort of a simple message. And the cap theorem seemed to be something that resonated as a marketing message. And therefore it just got repeated at nauseam and then got repeated by a lot of people who didn't really understand it. So I think the people building the technical technologies they did. But then it just sort of got repeated by people who hadn't thought about it carefully as a sort of received wisdom. Yeah, it's funny. I actually worked at Google Cloud during the Cloud Spanner launch and was slightly involved in it. And they literally wheeled in Eric Brewer. And we're like, you know, like write a blog post saying that your cap conjecture was wrong. We need it now. So yeah, I feel like the wisdom has totally done a done a 180 year. I do think, you know, Kyle Kingsbury of Jebson, right? He has been carefully trying to rebrand cap snowsh of availability as total availability. And I think that's a reasonable reframing because it just clarifies how absurdly absolutist like the formalizations notion of availability is. Yeah, I've had some discussions with Kyle about like what the right term that it should be. My preferred terms actually offline availability or disconnected operation. And it makes a ton of sense if you're thinking on software running on mobile devices, because like the calendar app on my phone, I want to be able to change events on my calendar regardless of whether I have a network connection right now. So it's a replicated database. And I want the availability and the cap theorem sense of the word I wanted to be able to modify the state of the database while it's offline and disconnected from any other replica. So in that situation is exactly what we want. If it's perfectly whether it makes so much sense in a sort of where the replicas are nodes in data centers and even if it's georeplicated, I don't know, that's much more debatable. But yes, so hence I prefer this offline availability term because it sort of focuses on the device in your hand use case. The makes a ton of sense I've avoided all client side development for basically my career. So that's not one of the use cases that pops to my entry. But yeah, whereas that's what I've been doing basically since I left industry. It's all been about collaboration software that stores its state's client side and it does all of the interesting work client side. And the server's just become like communication pipes really. I just some ways of getting some bytes from A to B. And I find that's a sort of refreshing perspective because it's small data and a big data intentionally. And I love it. Yeah, on the subject of the cap and will you just mention spanner and stuff. There was a paper or a white paper that was written back in like 2018 that caught my eye when I was at WePay and we were using a bunch of Google services. But in it, they have actual availability data for Google and like what actually caused the availability errors. And it's like 50% of the availability errors are actually user errors. Only 7% are network errors. I was looking at this and I was like, are we focusing on the wrong thing? Like this just seems like there's a lot of low hanging, maybe not low hanging fruit, but alternative issues here other than what we're talking about. It's probably related to the stuff you were talking about. It's written by Eric Brewer. That's a guy called Spanner True Time and the Cap theorem. And I remember reading this paper and being like, whoa, okay, we're a little misguided here on what we're looking at. I think that's really useful in empirical data. Yeah. And getting to that ratio, it's like one of these things where if you look at any kind of, if you look at any kind of statistics where it's like a lot of a high percentage of really bad stuff is something that sounds, you know, it's because there's been a huge war to get all the other bad stuff to a lower percentage, right? It's like people don't die and infancy anymore, which is why everybody dies of heart disease. It's like it was a huge struggle to get to everybody dying of heart disease. And so I feel like it's sort of the same way with what you're describing. Like Google's production network is like man millennia of effort that have gone into making it just outlandishly reliable, which is why you're allowed to say stuff like that. Circling all the way back to the beginning where now, so we've talked about the cap theorem which I think just sort of won this early round of distributed systems like thought leadership marketing stuff. You're, you've written this book now. You're working on V2. You're teaching young computer scientists who are interested in distributed systems. Do your courses sort of roughly follow the outline of the book and like how do you teach your students to think through these kind of trade-offs? Do you still talk about cap? Do you talk about like Daniel Abadi had some other framework that he was proposing at the time that I don't remember? Like do you teach one of the alternatives to cap? Pac-Elka or something like that. I think that was right. So the distributed systems course I teach to undergraduates is quite a bit more theoretical than the book. So it actually takes quite a different approach. I've sort of from time to time considered whether I should turn that into a separate book. But you know writing one book is enough of a trauma already. So so far I haven't embarked on that one. But the lecture notes are freely available online and there's a recording I put of it on YouTube as well. So anyone who's interested can just get that for free anyway. And so that one is quite a bit more theoretical because it's it's aimed at a different audience. Our undergraduates get quite a lot of mathematical background in our teaching. So the computer science course has quite a lot of theory in it and it's comparatively thin on the sort of practical software engineering aspect. Basically the philosophy in our department is that yeah people will pick that up on the job. People consider our computer science course to not be vocational training for an industry job but trying to like teach people the foundations of what computer science really is. For better or for worse either. You can judge that either way but anyway that's that's just the reality of how things are. But it means that you know I can use mathematical notation and be comfortable to the students will understand what it means. I go a lot more into algorithms and like my favorite part of the course is running the students through the pseudo code of an entire implementation of the raft algorithm which takes basically an entire hour, no actually more than an hour if you are sort of included the prelude of like the state transition that's that's happened. And so you know there's a ton of detail in there but I try to like really get them to think about like okay what what are really all the weird edge cases and then sort of think about that in an algorithmic way. Ideally what I'd like to do in the future iteration of that course is to incorporate model checking as well so that everything is done in a model checkable language with basically the philosophy of like look how subtle these algorithms are if you don't at least model check them if not do a proof you have no clue whatsoever whether they're correct or not. And so yeah whereas the and so that course focuses very much on distributed systems whereas the book is really a databases or in the book the sort of the distributed systems aspects there are to support the data management but it's sort of lead leads with the databases. So it's actually quite a quite a different thing. And besides that I teach a sort of practical cryptography course that's like a whole separate topic again. I guess one thing that's been on my mind you kind of mentioned earlier that some people think into this is sort of anti formal methods but I think I'd be interested in your guys is read on formal methods versus sort of the DST and sort of practical verification stuff in general because in my mind I kind of view them as complimentary and and so what I'm lacking personally as a user is like what are the best practice I like okay I want to make sure my software works best end to end and I feel like the sort of current messaging around that is okay you write systems tests you write unit tests you write integration tests right but there there doesn't seem to me to be a coherent story that spans both the design aspect all the way through to deployment to the system and I feel like there's some story to be told between you start with your formal methods and you do DST and you do a property based testing or whatever it is is that something you guys you have like a story that you tell around that and like oh yeah here's one you would use the ST and here's one you would use formal methods and here's how they tie together or is this more just like people have to stitch this together in their own brain. So okay I you know this is maybe not a company approved statement all right now we're getting the hot takes. I'm a little bit of a cynic. I think that the thing we're all trying to do here which is write software that works correctly is so hard and we need all of the help that we can get and so I think that you know I think that if you're really serious about this stuff you will probably find a way to use all of these tools because like because we know that it's provably impossible to write perfectly correct software right or proof of proof of the impossible to know that you have written perfectly correct software. So and honestly the struggle is not like getting formal methods people to adopt DST or getting DST people to adopt full methods it's getting 99.999999% of the world to test their software at all because most people just don't care about quality or they care about it but they're disempowered and they have no idea how to achieve it. And so you know I like when I learn that a potential customer is using formal methods I celebrate a little bit inside both because it means that they probably you know are writing some good software for their customers and because they're going to be easier to sell antithesis to because they like have demonstrated that they care about quality on on some level at all. You know the reason that that we started a startup focused on testing rather than on formal methods maybe also a little bit of cynicism like formal methods are really awesome if you are the kind of person who is going to sit down and decide to write really great software from day one. And I think the vast majority of the world is not going to do that. I think they do not have time for I mean they don't have time for any of this stuff. And they don't care about any of this stuff and even if they care their boss doesn't care about this stuff. And so you know as hard as a crazy it might sound given given that antithesis is today still a little bit hard to adopt we have really optimized everything and especially in the long term for making this as easy as possible to slap on as a band aid after the fact when you realize that you have gotten into very hot water and that you don't know what you're doing and that you need some help. And I think that you know the nice thing about about property based testing in general is that it's a little bit easier and to explain and a little bit easier to sort of like blur your eyes and imagine that's just like a fancy kind of unit test and a little bit easier to like show it to your boss and sort of try and convince him that you're doing something sensible here. I think that formal methods and proof based techniques are absolutely critical and non-negotiable in any kind of security critical domain because in an adversarial or antagonistic domain where you need to not just find most of the bugs but you need to find all of the bugs because it's totally asymmetrical right if your opponent finds one bug that's it you're done it's it's as if you had nothing that's the kind of confidence that really only a proof based technique can get you but it's still very very hard to do in that situation. I think if the situation's non adversarial testing generally gives you a better return on investment but yeah that was not approved. That was sort of what the threat I was trying to plot is it doesn't feel obvious to me when I should pick up my dst tool and use it and when I should pick up my formal methods tool and use it when I should pick up my chaos testing tool and use it and to your point there's return on investment for these things and you know there's sort of a risk impact matrix that the compliance people love to show you and so me as a practitioner I'm trying to figure out you know what is the risk what is the impact of the thing goes wrong and when should I apply which tool I don't feel like there's a good story about that around that right now I think that the security thing you point out is you know dead on and not something I had considered but that's in hindsight totally obvious it's like oh yeah that's an area where you would favor heavily these kind of tools and to the risk impact you know it's it's you know probably high risk high impact and so something where you'd want to pick up these kind of tools but but as a user for outside that domain even I struggle you know I wrote a dst thing first late db and found it to be you know relatively low return on a relatively high amount of investment for me and I will be the first to claim that is because I punted on the hardest part which is the state exploration part so there's like totally random and so so like it doesn't explore that much state to be honest but but I walked away being like well what do I do here like what's the you know how do I get more value out of this so that was kind of what I was pulling at is like if I want to use this stuff like when and where yeah for me it's just it's basically like is the situation adversarial if so you really want formal methods and then like also is it like highly asymmetric like if you're adversary whether that's actually a bad guy or just the world trying to find bugs in your software is economically able to devote thousands or hundreds of thousands of times more compute than you can then then something a little bit more formal is probably the right call you know I think those are sort of the criteria I mostly think about but I think what I what I mostly want to communicate here is that the concerns of these four people are so remote from the concerns of the vast majority of the market who by and large do not test their software yeah but as expected a lot of people you know a lot of people are basic building basic crud apps for some sort of business processes and they don't have particularly complex needs and it's not particularly subtle they if they just use a database with serialized transactions they're probably most of the way there to it being fine and then but then it's the people building the database systems well they need to be thinking really hard about the the various critical edge cases and that's not even adversarial system like you said but but just one way you're reasoning about concurrency and failures but then adversarial makes it even harder I push back on that a little bit I think like I think even the crud apps can be surprisingly subtle sometimes and and there's a lot of there's a lot of middle ground also between a pure you know react crud app and database like there's a lot of kinds of systems in the world and we're not very good at testing any of them look at look at all computer games how much blood and sweat and tears and lost vacation days have gone into trying to like make computer games not be full of showstopper bugs on launch day and and and now badly have they done even even with all of that even with all that energy like it just I don't know it seems to me like complex software artifacts are astonishingly hard to get right for for very fundamental reasons about the world and better tools for getting them right I think you're just gonna like I think there's room for a lot of tools for for helping to get them right is I guess what I'm saying yeah definitely I think there's also the like Chris in talking about like when you deploy these various things a lot of these correctness tools they have a time in the development lifecycle when they're most effective and we spent a lot of time talking about formal methods and how they're most effective when you're writing a specification but the problem with that is that oftentimes that's the time when as a business or even as a person you're kind of least willing to be all in on putting tons of effort into a project because you're not sure if anyone's gonna like it or if it's gonna deliver the value you want it to and there's so much very reasonable pressure to get something deployed in production to like see how it feels and if it's really solving the problem we have and if anyone's gonna use it and you know even for hobby projects for me at least you're like well once I get it kind of working am I even still gonna care about this project or will I have lost interest and so things that require like a big upfront investment I think people rationally shy away from them unless they're really really certain that this is going to be critical software that they really are going to want it to be correct yeah that was definitely my experience with SlateDB is early on it was just like oh we need to build a thing and then once we we built it you know I ran through the DSD stuff and I was all excited we found these three bugs and it turned out we knew about all three of the bugs because users had reported them so it was like well okay like we learned some stuff that we we knew and it's it's cool it could detect it but at the same time it was like you know it would have been nice to know that before the users were using it but on the flip side is a chicken and egg thing or it's like well nobody was using it so why would we test it I think that's a hard thing to navigate you know like Barton in your research part of the goal I assume is to like figure out how to do this properly and that is sort of core to the goal separate from adoption or GitHub Stars or NPM downloads the investing very early in very stringent correctness makes sense yeah absolutely I have as a researcher because I I don't have to care about it being like a commercially viable product if I think something is important enough to write a paper about it then it's worth spending some time formalizing it sorry but you absolutely right I think for for most people it's if you're building a practical system and you you don't you have different incentives from academia right and I think there are probably there are projects in industry that fit the same well like well you know if you're building internally within Google some like V2 rearchitecture of Spanner that's really going to like take on all the traffic of the one I assume you take the time to get it right before you start flopping traffic was there was a there was a project while I was there to rewrite Spanner storage engine and you know it was a very long running project let's just put it that way because when you're operating at Spanner scale very rare events happen every day not only that but but that you already know that system is used like when you roll it over that that sort of is this going to be used question that we were discussing is an answer it's foregone conclusion yes this will be used by you know billions and billions of transactions per second or whatever it is it's some insane load so it you already know that you're going to exercise in all these you know quote-unquote adversarial ways I also feel like one of the learnings I took away from my my sort of hobbyist approach to DST was I took an end to end approach to it which is like we have a database where it testing the public API is we're going to verify everything works and in order to do that you kind of have to have this whole system working but I feel in hindsight like there was a better way to go about it where I could have just done DST on subcomponents so for example just the compactor or you know just the object persistence part of the code and I could have bumped that up and done it much earlier somewhere somewhere in that spectrum between like a full DST which is what I wrote and on the other end just a full design proof I feel like I could have broken it down into components it probably gotten a lot more value earlier on but again like I didn't know what I was doing I didn't think this through and I didn't find a whole lot of guidance on like when and how to do this and most of what I found was like these really cool you know tiger beetle posts from from Joran and company where I was like oh look at all this cool stuff is and so I I I feel like there's still work to do in helping people you know that even wanted to do this like do it effectively yeah no way when to use which tool yeah is I mean I have no idea how you even explain how to give some general rules and as to when to which use which tool yeah that's what I struggle with so can I can I drop a crazy idea I had this morning on you guys so okay one one of the most annoying things about property based testing in DST and and so on is what should my properties be like what is my system actually supposed to do it's the thing that Ankush was talking about in his talk that he got great benefit from formal methods just being forced to think about it but most people don't want to think about it oh one very useful potential property that you have sometimes is if you're doing like a big re-architecture or a migration like we were talking about a very natural property is my new system behaves exactly like my old system right and that's a astonishingly powerful test oracle that you can deploy and that can give you great confidence that the thing you've rewritten is good so going back to our conversation about AI a thing that I've noticed in my own hobby usage of AI coding and also talking to others who use it more seriously is that AI is often very good at one shot generating a program and astonishingly bad at making incremental changes to programs or dealing with large and complex code bases so I think it is possible that we and I'm not sure I like this world but I think it might be the world we're heading towards where basically all software becomes right only like like you basically ask the AI to generate a software program for you and then when you want to make a change you literally delete it and ask the AI to make you a new software program with like a new thing added to the prompt and I feel like in that world the dst ability to compare two systems and to be like did these two systems behave in exactly the same way you know asterisk apart from whatever actually becomes like a crazy superpower and like very very useful and could could help with this sort of like one shot right only software development future. It's really interesting. I mean I think this sort of having a test oracle to compare against is definitely a very valuable principle. We're using it for some of our formal verification stuff where we define an algorithm in Isabel for example then extract executable Haskell code from it but I mean what we're going to do with I'm not going to put that Haskell code in production it would be far too slow anyway because it's not designed to be performant but we can use it as a test oracle against the rust handwritten rust implementation check and then just do some property based testing to check whether the two seem to behave the same way that seems like a wonderful way of gaining confidence in the correctness of an implementation. I don't even think that rust implementation needs to be handwritten. I found the LMS to be fantastic at rewriting code in a new language so you could just give it the Haskell and it could rewrite the rust right and then you could verify. Do these do the same thing. Yeah like I did that recently there was some Java chaos testing proxy tool that was like no longer maintained. I was like okay LLM rewrite this in rust for me and I'll use it and it was like shockingly good at doing that and so that's to me seems like an actually really interesting pretty clear path from a proof to you know some sort of like you know Haskell right tell me about your monads and then from the Haskell stuff in a rust all with like no human intervention in a way that's like actually a breadcrumb of verifiability is really interesting. I hadn't considered that. It's funny because that's common like to date that's been an anti-pattern of property based testing like you do not want to write a whole separate implementation in your tests but perhaps actually as we drive the cost of authoring software down that changes the calculus they're pretty dramatically. And on that note it's been a great discussion. Yeah awesome awesome guys I guess this is the part where we plug your book designing data intensive applications. Edition 2 is coming either before this errors or after this errors but either way you should preorder it or order it right should be in the February I believe. Yeah I should note there's already an early edition on Safari online too so if you got access you can go check it out. Well I'll go get an online print copy now and remember I got the early access edition of the first one so I want to paper copy of the second. Thank you both this has been really wonderful thank you so much. Thank you for joining us. Have a good one. It's been fun. Bye. Thanks for checking out the Bug Bash podcast. If you want to reach out maybe with an idea for a show or maybe you want to be on it send us an email at [email protected] or if chats more your style head over to antithesis.com and scroll to the bottom where you'll find the link to our discord. Finally if you're looking to connect with other folks in real life who care about software correctness and reliability consider attending the Bug Bash conference this year April 23rd and 24th in Washington DC all the details are at bugbash.antithesis.com until next time.