Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust.
Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust.
Watch all our episodes on the Building Better Systems youtube channel.
Joey Dodds: https://galois.com/team/joey-dodds/
Shpat Morina: https://galois.com/team/shpat-morina/
Alastair Reid's paper project: https://alastairreid.github.io/RelatedWork/papers/
Rust verification tools: https://github.com/project-oak/rust-verification-tools
Meeting Developers Where They Are paper: https://arxiv.org/abs/2010.16345
Galois, Inc.: https://galois.com/
Contact us: podcast@galois.com
Intro (00:02):
Designing manufacturing, installing and maintaining the high-speed electronic computer, the largest and most complex computers ever built.
Shpat (00:21):
Hey Joey, how's it going?
Joey (00:23):
I'm doing pretty good. How about you?
Shpat (00:24):
Doing pretty well? We're going to be listening to an interview that we did with Alastair Reid. Can you tell us a little bit about it?
Joey (00:32):
Yeah. So Alastair is a formal verification engineer. Alastair was at ARM for quite a few years, working on some really critical formal methods applications within the hardware world and has recently transitioned to Google where he's now trying to apply the same sort of thing. But for software, I was just got some really cool ideas about how to bring formal methods and how to bring proof style approaches to a large number of engineers, either in the hardware or the software world. So I'm really excited about doing this interview. We'll take a listen.
Joey (01:12):
Thanks for joining us Alastair. Thank you for having me. So I'm going to kick you off with our usual question, which is what is your approach to building better systems?
Alastair (01:22):
Uh, so at the moment I'm working on, uh, verifying, uh, rust programs and, uh, trying to use the, uh, the tools developed and the kind of formal methods community, uh, to do that. And the idea here is I think that kind of, we can make programmers, uh, can more effective using formal verification tools. So, uh, you know, help them kind of hit whatever the quality goal is, help them hit it more efficiently is kind of the idea. And if you then choose to kind of like take the time, saved and build something better, you know, I'll be happy with that, but just getting people to go, this is worth doing, uh, it makes my job easier, more enjoyable. I'll take that as a win.
Joey (02:07):
This is a bit of a different perspective than what we have sometimes, which is that formal verification is this really heavyweight thing that you can do on the most important projects. But it sounds like you have a, an overarching thesis that this is something people could find the approaches you're building are something that people could find useful from day to day. Right.
Alastair (02:26):
And I mean, it's partly that, but it's also that a, if you see that, you know, this is I'm going to guarantee your is correct. Well, one you're probably lying, but two, you're also setting yourself up with a really hard goal to hit and you're guaranteeing that it's going to be quite an expensive task. And so you're only going to apply it in a few cases. And so, you know, I'd much rather just get lots of people getting some value to verification tools and then build on that. And kind of later on people go, well, if I get a minimum number of people getting a bit more value and then, you know, right at the tippy top, you've got kind of like, you know, the people who are trying to kinda like show a very strong properties, but there's not so many of them perhaps.
Joey (03:12):
And until about a year ago, I think you were putting together approaches like this at arm, or you were working on just how to approach this problem at arm. Right? Yeah.
Alastair (03:21):
We were trying to figure out how we could kind of bring formal verification into, uh, kind of inside the company. And there was some sort of like technical ideas. And so I was kind of contributing to that. So a kind of five, we built the, uh, formal specification, Dom architecture, and it's got like all instructions and all their address translation and all exception handling and, you know, it's a very complete specification. Uh, but then we had to kind of let use that and okay, so we kind of figure out a way that it's kind of, uh, very effective at finding the kinds of bugs that normal testing is missing. And it's like, great, we're done. It's like, no, we've got to persuades kind of the, uh, the teams that they should actually use this. So it's like, you know, you sweetened individual, he's happy. Yeah, this is great.
Alastair (04:12):
But you've got to persuade the, the tech leads and the project manager that overall their project is going to be better. They're going to kind of like get alpha a little bit earlier. They're going to kind of have a better time when it comes to integration testing. And finally, they're going to release something to customers that is going to be less buggy and hopefully delivered a bit earlier. And so you've got to do all that. And then you've got to go to the next team and do it with them as well. And eventually you've got to kind of like work your way up to kind of like the kind of senior management and say, so we want you to give us a bunch more money to buy tools. We want, uh, we want to do a bunch more training for people, and we want you to hire some extra people so that we can do this new technique. And then we had to kind of like figure out, well, how enough that we're going to persuade them, spend more money. Cause they don't like spending more money. So, uh, you know, so we had to yeah. Figure out how to do that. Um, so did that in hardware and then switched to Google and, uh, um, trying to figure out kind of what I can take from that for verifying, uh, software.
Shpat (05:24):
What's different about the two jobs verifying hardware versus software and what maybe surprisingly was, is similar.
Alastair (05:34):
Um, so right at the lowest level, there's a loss of similarity. So they can have, I tend to use automatic verification tools because I think they give you the most bang for the buck. And so underneath a sat solver, model checkers, basically the same kind of flight, the Lewis level libraries you're using. But then on top of that, uh, does a huge amount of in, in software, different ways of a kind of writing it, different languages you ate in and, uh, libraries you're using all kinds of stuff has a huge amount of variety. And, uh, well, that's how I'm, it was mostly processors. And so we could focus on kind of one thing and one set of challenges that come up and processors. So kind of that the bits of what you actually do when you're at the keyboard is kind of different, but then kind of like, you know, you get the same thing that Paul was talking about is like within the project, it's the same as questions.
Alastair (06:34):
Like, you know, I've just verified something. I go to commit whatever I verified and someone has to review it. So can that person who's reviewing it, do a decent job of reviewing it when they look at what I verified, can they go, yup. Looks like you've done. You've checked everything that we once check or are they going, huh? Why didn't you check this? Or maybe the, the can't even spot that, uh, you know, there's something missing there because they're unfamiliar with, uh, with verification. So there's, you know, that kind of team level stuff and then kind of the higher levels in the company as well.
Shpat (07:12):
Yeah. If, if there, I would imagine that if they're, you know, in a position to say, why didn't you check this and why did we verify this? You've already kind of, you already bring in a bunch of value because you've, you know, you brought the team kind of halfway to meet you halfway. Yeah.
Alastair (07:26):
Yeah. So we've got to figure out kind of like how to get to that, to that point where they can actually look at something and go looks like you've done enough. And, you know, they can be confident that that that's the right answer. How do you,
Shpat (07:42):
This, this concept of convincing, so to speak the higher ups about the value of this stuff is very interesting to me. I think sometimes we hear about people having feeling burned from formal methods when they were introduced to them decades ago. And it seemed that the promise was much more than what ended up happening now, of course, some of those tools were not as deployable, um, academic prototypes and things like that. So we often kind of meet that now basically, uh, you know, when the actual state of the tools and approaches is, is very different. You're doing this at huge organizations that, that, you know, have businesses built around delivering things quickly. Right. I'm just, I'm very curious about how you go about getting people to understand where we are with these tools and approaches. Yeah. So that's really
Alastair (08:37):
Hard because all kinds of messages kind of floating around any company about what formal verification means. And, uh, so I, I suspect that what I'm going to end up doing is trying to avoid using the words, formal verification. I just kind of like, this is a better way of testing, which, you know, if you want to get value out of the formal verification tools, then just treating as a better way of testing things and maybe not even worrying about, you know, soundness, it's like, it's all key to miss some bugs, but we'll catch some really important ones. You know, that might be a successful message. And then you can kind of like go from there, but at the moment, the sole use of things being oversold, uh, and the there's all kinds of things that they knew will not work. And, you know, there'll be promised the moon and they won't get it, uh, that you have to be super careful about what you see and what other people are seeing about your work as well. You have to be kind of careful about that. So
Shpat (09:39):
It's interesting. W when we, before we started recording, I asked you how your day was, and you told me excitedly that you spend it working on proofs and just kind of technical work. And then when you talk about this, you know, having these conversations and debates, um, I feel like you find as much joy in, in getting people on the same page about this stuff as, as in some of the technical stuff. Um, how, how, how correct is that statement?
Alastair (10:06):
I get joy from it. Um, I'm not sure about joy. I, I, it's one of those things like, like writing a paper where it's like, I'm really glad when I finished doing it, but when am I actually doing it? It's like, it's just the most miserable thing in the world. So, but the end result. Yeah. So if I, you know, when I can persuade someone kind of our, you know, kind of like correct someone's viewpoints and things. Yay. But, you know, if I could avoid having to do that and just focus on the technical stuff, because someone else was doing that, I might be happy with that too.
Shpat (10:42):
You're doing it out of necessity. Yeah.
Joey (10:45):
Part of it. I think part of the, part of the idea hopefully is that it's a, like, you have to get this, you have to get the momentum started, but like obviously no successful approach has been one person sort of going out and calling up every developer and saying, Hey, this is, this is the way to think about this. This is so far part of it, part of what this, what it sounds like you're going after is trying to figure out the right approach that can see the kind of growth that any successful tool sees, which is, you know, not calling up people one by one and saying, you should use this because, but people saying, I need this because it's obviously the way to do things.
Alastair (11:24):
Right. So, well, there's actually two of us at say at Google working on this, myself and, uh, Shaq at Fluor, uh, who's also in the London office with me, well, in the London office, uh, meeting somewhere or not, not actually in London. Um, so, um, yeah, so Shaq Fleur and I are working in this, but yeah, so we're, we've got a bunch of kind of technical issues we have to work through, but so we're just started trying to put together some case studies to show mostly kind of what kind of specifications might you write? You know, what the properties you want to, uh, try to, uh, check, uh, and the approach we're taking is we write the properties in a way that they can also be used with our property based testing library. So to do some kind of fuzz testing. Uh, so we're trying to write this, we're willing to just start it.
Alastair (12:18):
So we haven't got very far in it, but we're trying to, uh, offer series of case studies where we go, you know what, in this case, um, this is the way to specify this. And in this case, tastes and cat catches pretty much all the bugs is not a problem for using a formal tool would not add much in this case. There's a loss of tricky corner cases, and we think you would get something and so on and trying to kind of explore what the advantages are, uh, with the idea that we can use that, to teach people how to, uh, how to use our tools. And when people say, Hey, what your tool is good for, we'll actually be able to give them, uh, an answer with some confidence.
Joey (12:59):
So it sounds like you're trying to automatically even identify places where people might get mileage from using better formal approaches. And the idea would be to avoid this, this scenario where somebody takes a bunch of time writing a specification, for example, and then applies it to a program. And it turns out everything was, was fine from the get go. And then they realized maybe that wasn't worth their time.
Alastair (13:23):
Uh, a bit of that, I mean, building a specification is just incredibly hard work. I mean, that's the main thing I did at arm for the last eight years was building a specification of the architecture and, uh, you know, for something like that for processor, um, where there's lots of potential different users it's worth doing, but most of the time you put a lot of effort into integrating a specification and you're not actually going to get much value from it. Um, or you have a really simple specification, but you also have quite simple implementation. And then, so it turns out that you're a specification in your implementation of almost identical, in which case, you know, sure. It's easy enough to do, but are you actually lately find many bugs if, if you're just checking that the code is equivalent to some almost identical cord, so yeah.
Alastair (14:16):
Yeah. Specifications are just, uh, incredibly hard. So we're also kind of wondering, kind of like, what can we do to, uh, to avoid having to write like full functional specifications and, uh, you know, the things that the, uh, uh, loss of the automatic verification tools we used for our foresee, as you just go looking for memory allocation, errors, and buffer overflows, and other things like that, which the, not what you want the program to you don't check what the program is doing. Check it's doing the vape thing. You check, it's not doing the wrong thing. So you knew sure. It shouldn't be debt D referencing no pointers. So you check for that. And the nice thing is that seems specification for all programs. So the specification effort is, is like zero or it's like, what command line flags shall I use this time? It's, you know, it's, it's really easy. Uh, so yeah, we're interested in kind of like how we can keep the specification effort, uh, really low as well.
Joey (15:14):
I think, I think another thing I took away, I read the paper that you published recently. And I, and I think we have similar approaches in a lot of our work is the idea that if you can get someone using that tool and start to understand what's possible, uh, then their own curiosity might drive them. If you have the quick static analysis that gives you some of the bugs, but not all, but they sort of have this inkling feeling that maybe they missed something over in this area. If only the tool can know a little more than all of a sudden, uh, the developers asking the questions and that learning curve gets so much easier at that point, when they start asking, how do I, how do I show more? How do I take the next step? All of a sudden somebody is not telling them to write a specification, rather they're going out and doing it because they want to make things better. Yeah.
Alastair (16:05):
And the thing is, what's the gateway drug that's going to get them started in this and kind of want to do more
Joey (16:11):
And, and the gateway. Yeah. And we've seen things like, I think Facebook infer is obviously Springs to mind when, when you mentioned quick static analysis, that, that turn things up. And I think rust as a whole could be viewed in, in this way, right. We're seeing lots of people switching to rest from CNC plus plus. And why, why are people doing that?
Alastair (16:35):
Right? And the nice thing is they're doing it because they're tired of having these stupid bugs in their code. They've actually unemploy secular. They want more reliable code. Uh, right. You look at the kind of various projects that companies are doing involving vast. And it's usually kind of bugs in this piece of code would be really bad. Therefore we can justify the effort of, you know, having to learn a new language before we can get started and not having such good tool support because it's LEDs. And you know, all the other costs of using a funny new language are justified because they want the higher quality a result. And that's great because if we can offer them a little bit higher quality, then they're open to it. Whereas if I take some random C or C plus plus a full grammar, they may care about kind of improving quality, but they may care about performance much more. And that, that may be their, the focus with first programmers. You're pretty sure that the kind of quality of the results is important to them,
Shpat (17:41):
By the way, the paper, I think the paper jury was referring to just for people who might not be aware, um, uh, it's called towards making formal methods, normal meeting developers, where they are. Um, and you've recently published it with a bunch of other co-authors we'll we'll share the paper. We found it very interesting. I'm sure. Joey has a bunch of questions about it. I'm curious from your point of view, what the main takeaway from, from this work was.
Alastair (18:05):
So it's, I guess it's a mixture of things because the paper's about maybe like three or four things. So one is a, maybe the main idea is this kind of meeting the developers where they are. So what that means is you say, well, I could him for the early adopters who will pick up a new tool and try just because, you know, they want to see is this any use to me, it looks fun, whatever. And they're willing to put up with quite a bit of pen to a, to do that, but that's not most programmers. Most programmers are, well, let's maybe a fair number of programmers spoon us, but there's also ones who kind of like, they're already kind of like busy. They don't have a lot of spare time and, uh, they've got a job to do and, uh, you know, a D a deadline to do it by.
Alastair (18:54):
And so what you want to do there is not say, Hey, I've got this exciting new tool that requires a bunch of training, and it's going to crash every now and then, and once accepts all your code and an, a list of other things, which the early adopters will put up with you and said, once to be able to say, here's this tool, uh, it's actually not so very different from what you normally do, right? So the meeting developers where they are, is saying, what, what, what do they normally do? Well, there, the role running tests of all doing code review, they're all, you know, a fair number of them are fuzzing, you know, there's things like that. So it's like, are there any of those that we can kind of like benefit from and, uh, make formal verification enough like that, that the training is fairly minimal and it's just like, you know, here's a different tool to use.
Alastair (19:43):
And so that's kind of what we're trying to kinda like, who can to, uh, with this kind of property-based testing approach we're taking, it's like, okay, this is a way of doing fuzzing. Oh, programmer. Yeah. Fuzzing. I'm familiar with that. I know something about your set. Uh, but this, this way of fussing is going to a find the obscure corner cases, random values won't catch, okay. There's a bit of extra value. And hopefully if that actually comes out, when they actually try it, then they go, okay, this is doing something that, uh, you know, I wasn't getting before
Shpat (20:18):
Difference between, um, developers that are actually working on something. Well, every, you know, most developers are working on something, but people who have time to just try something for the sake of trying things versus, you know, use it in an actual project that they're delivering for some of these tools that require a lot of effort and investment of time. I could see how that's a, that's a hard sell, um, yet, you know, in our mind, sometimes at least in mine, there's this view of like, if somebody who will the time to try this thing, because the value might be there, but th the truth is that people have been doing things this way for a while, and it's not like it, you know, the whole world isn't, this software is crashing and burning, but not, not as much as you would expect. I see what you mean. It takes a lot of kind of effort for things to be effortless, uh, in, in a way that people will
Joey (21:10):
Well, and, and even, even early adopters have pain thresholds, right? Like they're early adopters. Aren't these people that you can just torture with the worst tools. Cause they're so excited, right? Everybody's got a point where they're going to put something down and say, this is not worth my time. And a lot of formal methods of PR approaches and a lot of the tools out there today, I don't think of have even gotten under the threshold for all. But the earliest of adopters who I think we would call PhD students and in, in most corners, right? It's, it's somebody with somebody with a full-time job that is not doing early adoption work is probably going to shy away from a decent fraction of the tools out there. So bringing that pain threshold down is really important, but it's also a real interdisciplinary problem. I'd say, like, it's not, I think it's not something that just people like, like you and I can solve on our own because we aren't great at user experience.
Alastair (22:06):
Well, I think there's something that say Jean Young was talking about in the, uh, in that kind of fair first podcast you did about, uh, yeah. Just trying to make it, uh, look at what progress as developers are doing, kind of what they need to understand, to use something, how to meet that, to kind of fit into their workflow. And that's kind of, yeah. I mean, that was the kind of the core of the paper was I'd actually never worked with user experience researchers before. So it was kind of interesting, just kind of getting together with them and trying to kind of like figure out kind of what they knew that they could bring to this and persuade them that, you know, the kind of problems I had with the kinds of thing that they might be interested in thinking about. And, uh, it turned out that a so Google and a, you mentioned Facebook earlier, they've both got this thing of doing a kind of fair in the code review process is when the short static analysis results, because programmers are still kind of like willing to change kind of, uh, the code at that point.
Alastair (23:14):
If you wait until the weekend, before you run your verification again, and you then show them a bug involving code, they worked last week. It's like, no, I'm, I'm done. I can add that to my priority list. We actually add it up here. But for the, for the day, then here is where I think this one deserves to go, uh, but get it to them as the code has been reviewed. And, uh, then the reviewers will, uh, kind of start going, no, actually we should fix this. No,
Joey (23:44):
Yeah, that's, there's no question that it's, uh, the sooner, the better, you know, the, the best possible is the, is the red squiggly underline as they're, as they're typing it. And from there, the priority just continues to decline and yeah, the, the, the Facebook and for insight is that it hits the threshold of where, where it's too far down on that priority list. It hits that very quickly. Um, that's that that fall off is, is quicker, I think, than I would have expected, uh, until I had more experience with, with developers development. And, um, of course the paper that just says it really plainly that they observed that I, one of my favorite parts of, of the paper that you wrote is that it does actually have this, this really diverse author list, including not just formal methods researchers, but I believe product managers, as well as, um, full on UX researchers and the paper, actually, you can tell, I can tell which bits were, were not written by the formal methods people, because all of a sudden I had this part where I couldn't understand anything, and I had a bunch more research to do to start learning about UX stuff.
Joey (24:52):
And it was really cool to see that in your paper
Alastair (24:55):
Yes. As it was, as we were writing the paper, they'd start referring to bits of work. And I go, can you give me a citation for that? And it add a citation. And it's like, okay, now I'll go and read the paper or whatever. So I knew what they just said, that, that, yeah, that was one of the really fun things working on. It was just kind of like being exposed to that and then going, oh, right. There's a bunch of stuff I can read here and people have solved problems, which kind of overlap with what we've done. So, uh, let's just read a bunch of it. Yeah.
Joey (25:23):
Good job. Picking that one up. Cause I didn't actually ask you a question. I just said something nice. And let you talk. So you still had something to say, but, but I realized after the fact that I had just sort of, you know, just, just complimented you and then expected you to say something. So, uh, but yeah, well, so, and I guess, like, I think a lot of people's familiarity with you might be from Googling papers and landing on your website. You undertook this really cool project to catalog all the papers you read for a year, which by the way, was sort of an insane number of papers even by I think, many academic standards. Can you tell us a little about that? Yeah,
Alastair (26:00):
So it was, uh, I guess it came out of a, as I was finishing off my PhD and, uh, which was a couple of years ago, uh, and kind of preparing for the defense and just thinking about what I'm doing, I thought, okay, well I'll reread all the papers that I cite. And then I'm of course cursing how many I cited and, and, uh, so on. And I, I read them in, uh, in chronological order from oldest first. And it was really fun seeing the way that fueled, uh, had developed. So it's like, okay, I quite enjoy just the rereading of the papers. And, uh, I also knew that, uh, so I'm living in Cambridge, England, which is about a one hour train rate from, uh, from London, uh, if we're, uh, the offices. So it was just changing a to work at Google. And so it's like, Hmm, what should I do in that one hour each way? And, uh, you know, obviously I could read books and listen to podcasts, but I'm probably going to read papers. So, uh, so I thought it'd be fun just to kind of try to rate, say summaries of them. And yeah, I know a large number of papers because, you know, five days a week, you know, I have quite a lot of opportunity to read papers. So
Shpat (27:15):
Yeah, that explains the number, which is 122 papers that you read and summarize for people to kind of have access to the summaries from your point of view on your website.
Alastair (27:26):
Yeah. And it became harder to do at once. Uh, once I moved to working from home because the commute was that bit shorter. Um, so instead that can like read a paper, oh, I'll summarize it tonight. And then I never would. So
Shpat (27:40):
Just like the developers with a, with a bug at the end of the stack,
Joey (27:45):
Summarize it tonight. I've been, I've been feeling that pain to my, um, my Nintendo hours have dropped way off since I stopped riding the bus to work. So, you know, you and I are in the same, in the same boat here for sure. Um, barely, barely timing, you know, we can find time now. So going, going back to your, your paper now, um, there was though the whole thing slightly revolves around this, this prototype that you've built at Google. And it, I think a prototype because it came together remarkably quickly. Um, but it still sort of seems like it's maybe given you some, some useful early results. Can you tell us a little bit about what you built? Right.
Alastair (28:26):
So we wanted to build on this idea of kind of making things feel like testing or fussing. And, uh, one of the, uh, when the libraries that say people use for testing, uh, Russ programs, there's something called prop test and, uh, it's our property-based testing library. So anyone who's familiar with a quick check for Haskell or quick check for cork, or, you know, hypothesis for Python will we'll have used one of these. And it's basically, it's a it's of a fuzzer with a good user interface for seeing here's the kind of random values I want to generate. And here's how to generate structured random values. Then you have some code the set runs, and that could make continued some assertions that feel some arithmetic that overflows some, you know, uh, sessions that fail where wherever it is that say going on in your code. And then it acts like a Faso.
Alastair (29:24):
It generates random values until it finds something which feels, and then when it finds something, it tries to shrink the value down and produce a simpler value. So it is quite, it's quite nice a library. It it's quite easy to use a few try using it is kind of quite effective for where random values are, have a decent chance of finding a problems. So it's, it's pretty good. Um, and so what we want to do is say, okay, can we use that same interface for verification? So instead of creating random values, recreate, uh, kind of symbolic values, and then the verifier kind of tracks, how there was a used through the full gram, it hits an assertion of whatever, and it tries to find some values, some concrete values that will make it feel. And so that's the basic idea. So we just kind of took the prop test, eh, API and re implemented it, uh, on top of our, a verification API.
Alastair (30:21):
And so that's, that's working pretty well. Um, I'm actually spending a lot of time at the moment, just working my way through coroner's of rust, which turns out don't work because they make the, uh, our verification tool, uh, unhappy. So, uh, let me see, uh, this morning I was dealing with one to do with their memory allocation and I managed to get that one fixed. And then I found that some Russ cord was, uh, checking, do you have this factor, a instruction available because I want to use it to accelerate this piece of code. And so I have tomorrow, I'll try to figure out how to solve that one. So there's just lots of things for how to get, uh, tools, which were originally designed for verifying C code, trying to, uh, adapt them to verify a voskhod. I think industry often finds kind of new problems that nobody had really understood was a problem worth solving.
Alastair (31:18):
And so it kind of, hopefully you get academics to do that. Uh, but yeah, you're right. We build on top of all our academic work. So at the moment I'm mostly using the CLI symbolic execution tool, which is from a kind of Imperial college London, where just in the process of merging in some support for Seehorn, which from university of Waterloo. And, uh, and we've also got some support for a crux mural, which comes from Galois of course. So, uh, yeah, we're building, you know, all those things were actually, I mean, I don't think I can build a better verifier then those people can, in fact, I'm quite certain I can't, so I'm going okay, well, what can I do that, that does add value, eh, and, and then kind of make that available so that can the community, as a whole can figure out how they want to verify us code, how they need to change the tools to let them do that. And yeah, just, uh, just generally get better support for rust verification out there.
Joey (32:19):
And so just to reiterate what you've done with this prototype, you've basically taken this thing that people are already using in rust because they find it useful this prop test, um, and you've you found a way to hook up. It sounds like multiple industrial and academic tools in such a way that they can all a user can smoothly transition from the prop tests that they're already into using these tools and probably get better results than they were getting in the first place. Is that an accurate summary of, right?
Alastair (32:47):
Yeah. So the, yeah, one of them is to be able to kind of very easily swap back and forth, uh, kind of between different tools because, you know, sometimes fuzzing is going to be, you know, all the needs or it might even be better in some cases, uh, sometimes they need kind of the kind of analysis that, you know, a formal tool can do, but again, there's kind of differences, you know, depending on the scale of what they're doing and so on, you might want to use one tool or another. So if there can be just one interface that you use for all your formal verification and ideally a fair chunk of your testing, I, I think you kind of got the best of both worlds
Joey (33:26):
And even amongst the more formal tools, um, I don't understand exactly how you're using them all, but there's even a range there. Right. I think, um, Clea is sort of doing this, this feedback loop, as you mentioned, between trying to do a concrete exploration. So trying to generate basically smarter test cases from your fuzzer, whereas something like crux smear, um, is really about getting more thorough guarantees across your test. And so even, even amongst these formal tools, there's actually, uh, a spectrum of, of use and application. Right,
Alastair (33:59):
Right. You can, you can get CLI to a bit reluctantly, a kind of check everything and, uh, but it's, it's more comfortable looking for a, you know, for, for bugs are generating test cases for you. Uh, whereas yeah, something like crux smear is going to be kind of trying to check property as a whole. Um, and yeah, they're gonna, they're gonna scale different ways. Uh, CLI tends to have a, a problem where it has this kind of time explosion where it's a finds too many paths to check. And so you, eh, you get this kind of explosion from the number of paths, uh, a tool like a crux smear, if I'm actually used it enough to be sure that it does suffer from this, but it's, that kind of tool tends to suffer from using far too much memory and making, uh, kind of a SMT solvers, very unhappy. So yeah, you're going to switch back and forth. It might even be within the same program. You're verifying one that when we've another bit, the other way. So
Joey (35:08):
As you were talking, I actually realized that as we were, as we were making jokes about people with incredibly high pain tolerance is that you are, you are definitely an early adopter with an incredibly high pain tolerance to be, uh, taking not one but three, uh, verification tools to out of academia. Um, and, and mashing them together into a, into a prototype you've unquestionably qualified for the pain tolerance metal at this point.
Alastair (35:37):
Well, thank you. But I actually managed to trick my colleague gash at flew into doing two of them. So,
Joey (35:45):
All right, so you get the, you get the silver metal in this case. We won't give you the gold shack. It gets the gold. Yeah, not bad anyways.
Shpat (35:53):
Well, sir. It was a privilege to talk to you. Thank you for spending this time With us.
Alastair (35:58):
Oh, thank you. This is great. Thank you.
New Speaker (36:01):
Yeah. This was another episode of building better systems. See you all next up.