Rahul Kumar: Why verify Rust’s standard library?

AWS and the Rust Foundation are jointly sponsoring an initiative to verify the Rust standard library. Learn why from the initiative's creator, Rahul Kumar.

Rahul Kumar, Senior Applied Science Manager at AWS, is interviewed by Tim about his team’s ambitious effort to bring formal verification to mainstream programming.

Summary

As background, AWS and the Rust Foundation are co-sponsoring an effort formally verify Rust’s standard library. In November 2024, they jointly announced an initiative to award the winners of several challenges that apply formal methods to verify Rust’s stdlib.

We discover that this effort is at least partially underpinned by an aspiration to demonstrate that formal verification is a way to keep AI programmers on track, by being able to verify that the programs they generate actually do what they say they do.

Rahul describes a future where we can provide instructions to an AI and know that when they say it’s complete, we can have trust that the job is actually complete.

AI is also beneficial in accelerating us unprecedented levels. Uh, when it comes to development of products and services and code—do I, do I not want that? Of course, of course I want that. But do I want appropriate guardrails around it? Which help me develop confidence that, yes, I know that this AI gave me the right thing. And that's where formal verification comes in. That's where this effort comes in. Because formal verification is the answer. for producing those guardrails. Formal verification is the answer for producing those guardrails.

Highlights

  • What formal verification is and why it’s important, especially for Rust’s unsafe code
  • An overview of the Kani model checker, the verification tool that’s developed by Rahul’s team
  • How Kani differs from other tools like Miri
  • Kani’s ability to prove custom correctness properties
  • Efforts to bring contracts into the Rust programming language
  • The benefits and challenges of verifying Rust’s standard library
    • “The Rust standard library will challenge our tools. It will make us push the boundary. And that’s fantastic.”
  • How formal verification can enable a new era of AI-assisted programming with appropriate guardrails
    • “Formal verification is the answer for producing those guardrails.”
  • How the verification initiative and its challenges work
  • We learn that CMU students have already started
    • “One team cannot actually do this. I need a lot more support. And then, I realized the Rust community is an amazing community.”

Whether you’re an experienced Rust developer or just getting started, this episode provides valuable insights into the future of the language and software verification. Tune in now to learn more about this exciting project that can shape the way we build software.

Transcript

Introduction to Rahul Kumar and His Work

[00:00:00] Rahul Kumar: So my name is Rahul Kumar and I’m a Senior Applied Science Manager at AWS. I lead a team that works on Rust verification, C code verification, And, uh, we are very, very passionate about bringing formal methods into, uh, the mainstream, especially for Rust, which is what this work is about and what I’m going to talk about a bit more. Uh, previously, I worked at Microsoft, Microsoft Research. I worked on decode verification um, a little bit of empirical software engineering techniques. And then, uh, before that, I also worked on the Europa Clipper mission at NASA JPL. So, very exciting.

Understanding Formal Verification in Rust

[00:01:14] Tim: The first question to ask, I suppose, is , what is formal verification? But can I actually intercept myself by asking something else, which is , I thought Rust was a safe programming language and you made a special note to say, that you are especially interested in verifying Rust.

And so, can you describe to me, like, what the dist, like, how Rust is sort of, like, uh, is Rust lying to us? Like, what’s, what ne, what are, what are the holes that need to be filled?

[00:01:47] Rahul Kumar: Yeah, so, uh, very first I’m going to say, no, there’s no lies here, right? That would be a bit aggressive.

[00:01:55] Tim: Okay, sure.

[00:01:56] Rahul Kumar: an amazing programming language, which provides Fantastic, fantastic compile time guarantees that most other languages will not provide you.

The Role of Unsafe Code in Rust

[00:02:07] Rahul Kumar: Rust does have an escape path to perform certain functions. And, uh, that’s called the unsafe part of Rust. It provides you so called superpowers to, achieve what you’re looking to, to do. there are various reasons why one may choose to adopt those. So, number one, no lies. Number two, no lies. Yes, we have an escape path, and at that point the compiler will stop giving you guarantees that it traditionally would in SafeRust. Now, does that mean? That basically means that the compiler is expecting some sort of human assist, or potentially AI assist in the future, to, to enable you to give the guarantees for yourself.

[00:02:57] Tim: So I would normally describe this as the burden of proof kind of shifts from the compiler to you as the programmer. Do you kind of, how does that sentence fit with you?

[00:03:09] Rahul Kumar: That’s, that’s a wonderful way to say it. And you use an interesting word in there called proof,

[00:03:15] Tim: Uh huh.

[00:03:16] Rahul Kumar: Because the compiler is actually in the safe world, giving you proof that you’re okay, but in the unsafe world, it is not giving you that proof. while you may run this particular piece of code a million times and never have an issue, have a guarantee, which is what the proof will give you at the end. And yes, the burden of proof is on the programmer.

[00:03:41] Tim: Right. I, I need to kind of, uh, I did an undergraduate degree in philosophy actually. Um, and just kind of like, this is sort of bringing up like old neurons are activated about like, Inductive and versus deductive logic and the fact that essentially it doesn’t matter how many times it’s right if we if you can’t guarantee that Uh that it might never be wrong.

You you still never have um that kind of quality and uh, I sure yeah. Yeah. No, absolutely.

Challenges and Motivations for Using Unsafe Rust

[00:04:14] Tim: So the And just, because there are a couple of people who are terrified of this keyword, unsafe.

[00:04:20] Rahul Kumar: will.

[00:04:24] Tim: is why we might use this escape hatch. And sometimes it’s impossible to avoid, such as if I want to talk to the operating system, or I need to talk to some, uh, other library.

That might be written in different programming language, uh, and it’s impossible for the Rust compiler to guarantee, make some, any, some sort of assertion or guarantee about programs that other, that live somewhere else, that, that those are, that’s one case where it might be impossible to avoid unsafe.

[00:04:58] Rahul Kumar: Yeah, uh, uh, you know, you want to, you want to use some foreign, uh, language interface or you want to dereference raw pointers, uh, the, the so called five superpowers that Rust has in, in all of those cases. Either you are functionally bound and you want to, to achieve a, a particular function at the end, or a functionality at the end, which you’re, you’re not able to do because of SafeRUS. Great, that’s a perfectly valid reason to do this, or maybe there is a performance concern because the SafeRUS could potentially introduce checks that you are not very interested in having. And it causes a performance slowdown. again, back

[00:05:50] Tim: so. At this point, it’s this temptation of, well, I could go faster. Like I essentially, uh, I know that there are, I know like in sort of scare quotes there, because I might be wrong. Like it turns out that humans are often wrong about these things, but you know, for as far as I can see as the programmer, uh, I am upholding invariance around memory safety and so forth.

And so I could, uh, essentially skip safety checks that the. Compiler would otherwise kind of inject and yeah, and then suddenly I’d get like a, let’s say, I don’t know, a two or 3 percent speed up in code that might be, yeah. Okay. Interesting.

[00:06:36] Rahul Kumar: Yeah, so imagine, uh, developer, uh, X, uh, tasked by their manager to take a piece of C code and manager says, you know, I want you to go make this in Rust because I’ve heard it’s safe and faster. And, uh, And developer X goes and rewrites it in Rust, in SafeRust, and turns out it’s actually the same performance as the C code, because there’s a bunch of safety injections in there. then they experiment and go into unsafe mode, and turns out it’s actually a lot faster, but now we don’t have a proof of correctness, which the SafeRust would have provided.

[00:07:19] Tim: Okay.

[00:07:21] Rahul Kumar: at that point, Yes, the burden of proof is on the developer and that’s a simple motivational example that this has happened in real life.

We have seen examples of this. Um, unsafe for us tends to have a very, very useful function and support it. The, the place that we are coming from is Even if it’s unsafe, why don’t we go provide you those assurances that would not have been possible before? And that’s amazing because, uh, now you can probably go into unsafe and achieve the functions that you want to achieve still have guarantees for the future.

Introduction to Formal Verification Tools

[00:08:11] Tim: So, and this is verification. So I expect that the term formal verification has, has a very precise technical meaning, do you want to, is that correct? And if so, do you want to flesh that out?

[00:08:24] Rahul Kumar: mathema yes, uh, we want to use mathematical logic. Uh, to prove properties about your programs and, and formal verification, in a sense, you know, you could say, well, I want to go verify a model of something. That’s fine as well, but the, the artifact that you are dealing with, which you are most interested in will exhibit certain properties, and we want to go prove properties about that, about that artifact, and we want to prove them Exclusively, unboundedly, impermanence, if you will.

Exploring Kani and Symbolic Execution

[00:09:04] Tim: I suppose one of the things that was fascinating to me about one of the tools that hopefully we’ll get to chat about called Kani was that it’s all symbolic. The actual code itself doesn’t really get executed and kind of get, as far as I can tell, gets translated and then run through an SAT solver and then, uh, yeah.

And so it’s, it’s, it’s almost as though. You’re operating with software, not as a set of instructions for a computer to kind of go from top to bottom through, like you might think of it scanning through assembly, but as a series of symbolic instructions, so much more sort of a high level, um, and just the structure of the way that the program is operating allows, um, The solver or that was the tooling to some, make some sort of inference or actually no deduction about correctness,

[00:10:03] Rahul Kumar: Yeah, I think I think the word, uh, which would be appropriate here is semantics.

[00:10:08] Tim: right?

[00:10:09] Rahul Kumar: So semantics and, and then specification, right? So, we, we take the, the input and we process it according to the semantics that are defined. And interestingly enough, there are situations with programming languages where semantics are undefined. And that’s something that we would like to also change.

The Importance of Rust Standard Library Verification

[00:10:36] Rahul Kumar: So attacking this core problem of let’s go verify the Rust standard library, let’s go verify the core library. Well, we’re, we’re now in a place where we’re challenging a community to actually formally define the semantics, right? Uh, there’s

[00:10:56] Tim: Right,

[00:10:57] Rahul Kumar: this funny,

[00:10:58] Tim: so if, uh, hopefully an example will pop into your head just immediately, but if essentially there’s a gap in the specification where it kind of provides wriggle room, which makes it essentially impossible to verify because there’s ambiguity there. Is that the problem that there is?

[00:11:17] Rahul Kumar: and, and a funny party trick, right, that, that used to be played, uh, in, in the math clubs was, Oh, let me prove 1 equals 0.

[00:11:26] Tim: Mmm.

[00:11:27] Rahul Kumar: the essential idea was that you’re dividing by x minus x, And you can go prove one equals zero to somebody who doesn’t realize that this particular semantics is not, is prohibited.

It’s not allowed. uh, uh, with the Russ or with a lot of programming languages, in fact, maybe all, I’m not sure, uh, it is, it is true that there are gaps in the defined semantics. And we would like to close out on that.

Formal Verification in Practice: Tools and Techniques

[00:12:00] Tim: Formal verification would I associate, or at least I have been associating with things like TLA or, uh, There are a couple of other modeling languages. Some are easier to use than others, but typically they are difficult and very complex and challenging. Um, uh, Do you have any thoughts on why these, uh, Uh, Why formal verification is so difficult for, let’s say most programmers, and that it seems like a very specialized topic.

[00:12:44] Rahul Kumar: So, so I will give you that it is specialized, uh, number one. Number two, I, I think that the examples you cite are also interesting because they’re not directly what a software engineer would go write and deploy at the end of the day,

[00:13:03] Tim: Yeah, they’re modeling. Well, at least LAPLUS is definitely a, a, Click here. Mm hmm.

[00:13:15] Rahul Kumar: Veris, uh, would fit into that domain where we’re actually trying to operate on the code that is being deployed. And one of the goals for us is to make this as automated as possible. So, yes, do you, do you, would we like you to specify properties? Absolutely. Right, because that’s something that you know about. You know your code. But do we want you to go create models? Probably not. We’re, we’re trying to do that for you. And we

for you.

[00:13:55] Tim: And so it sounds like one of the barriers has been, well, you need to, if you want to learn formal verification or at least some subset of the domain, then you need to go learn a modeling language and, uh, and create a specification. Whereas let’s say newer tools or the tools The Kani in particular, uh, essentially it’s just Rust code and, um, it’s actually embedded in the code that you’re actually running.

It’s not some separate artifact. And so, um, I mean, I personally, when I’ve used Kani have really appreciated that, that essentially the tooling kind of comes to me and that I don’t need to go out to something else and use a different workflow. I can just use Cargo, for example, to drive it. Um, I think. Um,

and,

[00:14:43] Rahul Kumar: uh, the ergonomics of making this real and scalable are so important. And, you know, uh, imagine being in a meeting where you go from discussing highly symbolic execution oriented algorithms, uh, and problems with them to, well, we think this should be Not start with a star, it should be an ampersand. Um, and, and, you know, both are amazingly valid. Because if you want to push formal verification to the next frontier, make it part of the mainline, is what it takes. You have to work on both ends of the spectrum. You can go make the best engine in the world, you don’t have a beautiful car on top of it, people aren’t really going to drive it.

[00:15:36] Tim: Yeah, I, I spend a lot of time picking at, uh, syntax as well, even though it feels in some sense, meaningless or trivial or somehow less important, but really nice. syntax. It kind of lends itself to really nice programs in a way. And, uh, and, and so the struggle is, is, is kind of real, I think, when you’re designing a language about, do we use curly braces?

Do we use angle braces? But, um, the, uh, the idea here is that we have a A tool, Kani in this case, which can take Rust code, uh, reason about it symbolically, uh, and essentially make some sort of guarantee or that the properties of correctness. Maintained through the use of unsafe, uh, surely, but surely the project is not yet done.

Are there kind of known limitations where, I mean, presumably that there are, you, you know, where the gaps are, I hope.

[00:16:55] Rahul Kumar: Right. So I have, I have, uh, two or three things to say here. So number one, it’s number one. Uh, yes, we do have limitations and we publish them and, and believe me, we are absolutely 100 percent on the ball about making sure we publish these because no false guarantee should be made. Right. Number two, uh, there is a distinction between these generic properties versus user oriented properties

[00:17:29] Tim: Okay.

[00:17:31] Rahul Kumar: right, and you can make Uh, you can, you can go check for certain UBs which come right out of the box with Connie because, hey, that just applies to everything in Rust, right? Uh, but then if you want to go say, I’m very highly interested that this particular variable never exceeds the value of 42. Okay, you can go write that property and prove it. And, uh, there’s a fascinating example. There’s a repository out there called HiFiTime. And there’s a blog post on the Connie blog about, uh, proving the correctness of HiFiTime. Uh, it’s a, it’s a time library for the, the solar system, if you will, operating across multiple, And, uh, Christopher Rabbitin, uh, who wrote the blog post with us or mostly by himself, uh, but we reviewed it, which was nice. Uh, of the first external contributions to the Connie blog, uh, picked up on Connie and used it to prove correctness of, of so many functions. For the next 36, 000 years.

[00:18:48] Tim: Incredible.

[00:18:50] Rahul Kumar: Right. And, and that’s, those are such custom properties that he’s working with, right? Uh, amazing stuff. Uh, AWS Firecracker, which, uh, is a VMM that is open source on GitHub. And, and we rely on that quite a bit. They have so many custom properties that they prove about, about their code base. And, and how they deal with certain issues. Those are fascinating, uh, user oriented functional properties that people are proving. In addition to the generic UBs that they

[00:19:26] Tim: Sure. So can I, just as a hypothetical, I’m not sure, like, I literally don’t know if this is possible. It would be wonderful to have a per, uh, let’s say a percentage type, which is encoded as floating point, although maybe it should be irrational using a, a, um, an instrument. But let’s say it’s not. And so I’m using floating and I want to guarantee that the use of my percentage is always between zero and one.

So essentially, um, it’s bounded with inside those, um, with, uh, is that something that I can ask? Kani to chick so that I should never be able to have.

[00:20:03] Rahul Kumar: the box. But you can by encoding a custom property, yes.

[00:20:10] Tim: Wow.

[00:20:11] Rahul Kumar: give you the ability to, ability to, yeah.

[00:20:14] Tim: Yeah. I, um, I’ve always kind of been in, uh, there’s a part of Ada, which I have always been fascinated by, which whereby you can have. Types which are constrained by their ranges rather than being, rather than having all integers available to you, you’ve just got some subset and, um, I’ve always wondered how that is implemented because the representation in memory is presumably just an integer, or for example, and, um,

[00:20:45] Rahul Kumar: so you bring up specifically floating points, which I think we have a bug on, but I’m not sure. Let me be clear about that. And we claim that in our list,

[00:20:57] Tim: Floating point is much harder than integers, which is why I brought it up. Oh yeah,

[00:21:01] Rahul Kumar: that’s kind of where I was going. Right? So if you’re sticking to integers, you’re sticking to integers. Yes, you can restrict it, uh, floating points. I believe we are, we’re trying to, there’s certain SIMD instructions where we’re, we’re have like a small issue. Um, modulo becomes interesting, you know,

uh, incomplete.

So,

[00:21:22] Tim: Look, I think, look, the fact that these are the goals that you’re striving for, and I know, I mean, it’s sort of incredible and, uh, I wonder how that would translate Through unsafe, like we’ve got, you’ve mentioned UBs are like a general thing, class of problems that we wish to avoid. So we want to remove the possibility of unsafe or sorry, undefined behavior.

Um, I suppose this would be classified at build time or at test time. Um, and. One question, Mark, that I, uh, that’s kind of lingering around is how Kani differs from other tools in its space that are achieving similar things, such as like the Mirri, uh, is an interpreter. So this operates in a significant, its model of operation is much different, isn’t it?

[00:22:19] Rahul Kumar: yes, yes, this is a great question. So, you know, there’s a, there’s a spectrum of tools. And, and each one, and every single tool comes with its benefits. Right. Uh, uh, you, you can start with, with basic dynamic execution. Uh, you can go to testing, you can go to fuzz testing, you can go into model checking, which is where Connie fits, right?

Then you go into deductive logic based tools and higher order logic based tools. Uh, spectrum is, is, is very important because, The effort that we have, you know, coming back to the Rust standard library verification effort, it’s not about Connie. It’s about ensuring that we can use this spectrum of tools to go give guarantees for the future. An effort, like at a very basic level, an effort is a collection of people who are trying to achieve a goal. And one of the first things they do is create a demonstration that, hey, I can go do something. And what we have done thus far is given a demonstration. And the hope is, the idea is that more and more people join this effort and bring in their specialties and their tools.

[00:23:52] Tim: That’s extremely exciting. Do you think that the, although I’m just going to wait for my dog to decide to stop barking.

[00:24:01] Rahul Kumar: Sure.

[00:24:02] Tim: I think someone just came home, which makes us excited. The, um,

here’s a question for you. Do you think there are a large number of tools that are sitting in the darkness waiting to kind of be revealed to the world?

[00:24:18] Rahul Kumar: I don’t know if sitting in the darkness is a phrase I would use, but there are, there are a lot of tools that, that can be used. Yeah. Look at tools like, uh, Cruzeau, I I Nia is a great example. I think that’s a wonderful tool. We are borrowing concepts from ideas. Uh, Veris is a great example. You know, Connie, of course, since we happen to be closely related to Connie, that’s how we wanted to make the demonstration and jumpstart. That’s it,

[00:24:55] Tim: So let’s talk about this, this kind of project. We started chatting before, uh, uh, on LinkedIn because I posted a note about something that I read, uh, that came as a joint effort from the Rust Foundation and AWS, and your name was attached, at least on the AWS side. So, uh, what is it that you’re trying to do?

The Future of Programming with AI and Formal Verification

[00:25:26] Rahul Kumar: Very simply put, we want to deliver the new era of programming language. So, you know, we live in a world where AI has already proven to be very useful for certain aspects. Um, Uh, I don’t know how much you use it per se, but you know, there’s people summarizing things, there’s people rewriting things, there’s people now starting to make 20 second videos, uh,

[00:25:59] Tim: Yeah, look, I, I, I actually am, uh, Increasingly surprised at how effective it is at getting me. I think when chat GPT first came out, it was like really good at getting me like a first draft for some sort of piece of content that I wanted to produce. And now that, um, and now the models and also the tooling around the models and some, uh, and, and the increasing capabilities around rag, which is, um, I can’t actually remember what it expands out to, but the ability that you could actually teach models about your custom, your own content means that.

It’s getting better and better at source code and relatively complex. The context windows are increasing. La la la la la. So, uh, I am, uh, I would say I am one of the people that are, that have high expectations for, for, um, for AI and its ability to remove a lot of tedium from the process of programming and a lot of mistakes.

Uh, I think that, uh, It is, um, but I’m also relatively skeptical. Like I’d rather be late and allow other people to feel the pain.

[00:27:16] Rahul Kumar: Yeah, absolutely. And, and, you know, I’m gonna tie AI back to a previous comment or discussion actually, that we had. You, you can go test something a million times and just because it doesn’t fail doesn’t mean it won’t fail, uh, and AI, we all know we’ve actually experienced the hallucinations to, to some degree where, uh, you’re like, well, that’s not exactly what I was looking for.

Now, AI is also, AI is also beneficial in accelerating us unprecedented levels. Uh, when it comes to development of products and services and code, do I, do I not want that? Of course, of course I want that. But do I want appropriate guardrails around it? Which help me develop confidence that, yes, I know that this AI gave me the right thing. And that’s where formal verification comes in. That’s where this effort comes in. Because formal verification is the answer. for producing those guardrails.

[00:28:22] Tim: Right. So, okay. So now you have told a model, please generate a piece of code or, you know, like fix this feature or fix this bug in, but, but you also need. But it kind of gets constrained by the fact that the tests must pass. And by the way, the tests are not just tests anymore. They’re formal verifications of correctness.

Um,

[00:28:47] Rahul Kumar: yeah. And that’s a very strong statement because Um, say you want to go update your library and it has dependencies. The AI says, sure, no problem. Here you go. Here’s a bunch of tokens. I’m just going to go spit them at you.

[00:29:02] Tim: I’m right. I love tokens. Here’s, here’s a thousand.

[00:29:07] Rahul Kumar: And then here’s Rahul sitting on his computer going, uh, should I commit this? Should I approve this for request? I’m not sure what’s going to happen here. But then, uh, the formal verification tool kicks in and says, Hey, guess what? We’ve just proved that this is great. It. Works. It’s equivalent to what you had before. for it.

[00:29:28] Tim: Hmm. Yeah. I, uh, and now essentially, well, yeah, that that’s just a huge new paradigm of writing software that, uh, you kind of have like this human augmentation. Um, and I think that will are immensely powerful, particularly at big, big, big places where you have lots of hulky projects that there’s never enough.

It’s really, I know that people say that we have these trillion dollar companies, but being someone who’s worked inside one of them, no one ever has budget for like massive rewrites. And so I think this will liberate a lot of, uh, of people. Yeah, one of the things I really appreciate about Rust is that you can feel, is the notion of this fearless concurrency.

That was the first, pretty much the first slogan that people really understood when Rust came, like first came out like 2012, 2013. Fearless concurrency was one, and uh, and the other one would be blazing fast. Rust. Those were the two things that really stuck. And now it sounds like what you’re saying is the future.

If we, if, if we get it right, like it’s not, it is literally a future that is not, there’s lots of things that might go wrong, but in principle, the tooling should get sufficient. Such that, that feeling of, uh, being fearless, essentially knowing that you can’t crash, uh uh, you can’t. Your programs will carry on because they’ll be correct.

You actually know that. That would be an immensely liberating feeling, um, for people that are building, which is amazing.

[00:31:28] Rahul Kumar: Yes. And you know, I, I’ll

a few decades, uh, which some people may or may not relate to, but the amount of times we had to reboot a computer, uh, and, and the, and the wastage that that produced, imagine if you never have to deal with that.

[00:31:49] Tim: is almost perfect. But yeah, no, no, and there are some very strange things. I mean, if people who, people who didn’t grow up or didn’t experience the dial up era of the internet. Well, never really. Once upon a time, you needed to literally plug the modem into the wall, like unplug the phone because you could either have a phone or the computer would be talking on the internet and you’d pay,

[00:32:21] Rahul Kumar: get a second line.

[00:32:22] Tim: right, right.

And, and, and things like email. It felt different because you on, on Outlook or like Thunderbird or whatever, there was a button like send and receive because literally you need to phone in and download things from messages that come in from the server and like re upload. Now we think of. Email is essentially instant messaging.

We’re always connected. The protocol actually expects that everything is asynchronous and so forth. It still operates in an era where the whole, uh, everything is disconnected and flaky, but messaging, is different. The internet feels different. It’s essentially,

[00:33:07] Rahul Kumar: and imagine the future computer scientist, which uses AI to but guarantees the work with formal verification. Like, you know, uh, you and I probably sat down in IDEs and wrote code and debug code. That’s going to be an extinct, antiquated activity. It’s like, at some point people are going to be like, Grandpa, so you used to have an IDE?

[00:33:37] Tim: yeah. Well, I think, I think of this, like my immediate, my, and it’s interesting, I’m just kind of thinking about my own response to your comment. My immediate was like, it’s kind of this, you know, this kind of back and it’s like, no way, Rahul, you, you, this is, this is nonsense. And then it’s like, what, pause? I think the same way about, uh, Financial transactions in America.

So in the United States, checks are used everywhere. New Zealand stopped accepting checks. Like banks don’t literally, you can’t seem to use a check in our country.

[00:34:17] Rahul Kumar: Same in Finland, right? They don’t have checkbooks.

[00:34:21] Tim: Yeah, it’s like, not a thing there’s, and, uh, uh, and so, and we don’t expect that messages are going to be, are going to be seen. I was going to say telegram or something like things change and, uh, the tools will get good enough. That the boring work of like literally typing, touching the keyboard, getting the program written will be done the hard part of the system design, the hard part of like developing the product, the, the finding how the components work and, and that will still, you’ll be driving that, but you’re essentially, you’ll be, yeah, you will be driving these, these AI agents to essentially create or co create.

Um, some sort of artifact and that will be difficult shift for many people. And, but I think that overall it’ll be. Like artisanal, artisanal software development where, you know, people will, it’s just like having like handmade, handmade shoes feels, uh, very, um, very old fashioned and very, I think I’m forgetting a word, but, but some people still like to have, to have, um, Shoes made by hand.

And lots of people would love to pay if they could. Um, and in Japan, we still have handmade shoes, but, um, in lots of places, but most people’s shoes are made in factories and, uh, and, and they’re mass produced. And so I think most software will be in some sense, mass produced.

[00:36:04] Rahul Kumar: well, and, Uh, And I think maybe the way I think about it is we’re moving one level of abstraction up, so it’s no longer about, about, Oh, how do I write this function? It’s more about, I’m writing this object. I’m creating this object, which knows how to interact with other objects. And then now we’re saying, don’t even worry about the object, Class. Don’t worry about that. Now move on to, let’s. modules that you’re working on. Your problem solving techniques are now coming into the module because the rest of the stuff we can go manage and we can do it with guardrails in place, with verification in place.

[00:36:52] Tim: The future that you’re describing here. I look, I think I, you know, it’s very, it’s very easy to, oh, like there’s a bootstrapping problem where if you start with a program, you need to kind of handwrite. The, the, the, the, the properties that you wish to kind of guarantee, blah, blah, blah. And, but yeah, but it’s just a kind of a fascinating idea.

So then the question that becomes like, why would, what is important about the Rust standard library as part of this overall process? Why is that the next thing to do?

[00:37:32] Rahul Kumar: Yeah, so, there’s two parts, or well, three parts to it. One, the Rust standard library, know, uh, contrary to popular belief, does have bugs in it which have been exposed in the past. Yes, uh,

[00:37:49] Tim: We don’t talk about these things.

[00:37:51] Rahul Kumar: yeah.

[00:37:52] Tim: Yeah. It turns out it’s just software.

[00:37:54] Rahul Kumar: so, so, When you want to build a house, where do you start? You start with the foundation and our foundation is the core and the standard library. if we can, not if, but when we make our tools actually do this for the core, the foundation automagically, yes, automagically, we can start making it work for everything else above it. And that’s the number one reason,

[00:38:29] Tim: So is part of the reason why that magic happens is once the tools are good enough to do it in the standard library, which is in some sense the most impactful, uh, you know, like, uh, library that Rust programmers have access to, um, then everywhere else should be at least no more difficult.

[00:38:51] Rahul Kumar: Yes. That’s a great insight on your part. That is, that is one of the ideas here, right? That the, the second point is the Rust Center Library will challenge our tools. will make us push the boundary. And that’s fantastic, right?

[00:39:11] Tim: Your, uh, I suppose that the, the fact that a lot of Rust programmers use non, the no standard attributes, such that essentially they turn off the standard library is slightly orthogonal to this, because if I’m just on an embedded device, I could still use the verification tools. They still exist. And, um, but essentially this is a big, ambitious, difficult project.

Um, and you’re attempting to use the, the, the program of work as a way to kind of recruit or, uh, essentially kind of gather a community of researchers to, uh, or at least this is kind of kind of, I’m trying to figure out where, at what point did you think Think, you know what we should do? We should turn this into like an X prize, like an awards.

Uh, you know, we should, we should essentially.

[00:40:13] Rahul Kumar: tell you exactly when I thought that.

[00:40:15] Tim: Okay.

[00:40:16] Rahul Kumar: It’s when I realized the amount of unsafe code in the Rust standard library. And, okay, one team cannot actually do this. I need a lot more support. And then, you know, uh, I, believe the Rust community is an amazing community. It has been a fascinating community for me, at least. I realized, well, I think that people would like to contribute because three reasons. Number one, benefits everyone, right? This benefits, it benefits people who are building on top of Rust, creating their applications, their scenarios. It benefits people who are developing Rust. It benefits academia, students, uh, researchers, industry. Uh, it’s a win, win, win, win. And, uh, I thought, well, okay, but you know, if I just go post a message saying, Hey, let’s go verify the Rust library, well, it’s probably going to get drowned in the, in the plethora and the sea of, of, uh, all the messages that are being posted. So the effort was born out of let’s make it more organized and let’s jumpstart this. Because I think there’s a lot of people who are motivated out there who want to do something like this, this gives them a great cause.

[00:41:47] Tim: Hmm. Okay. Yeah, the Rust community is not, by the Rust community, the messages, where the message are presumably you would have sent if you would have sort of say, Hi, by the way, I’m looking for, would have been like the Zulip channel, like the main one, presumably.

[00:42:03] Rahul Kumar: Sure.

[00:42:04] Tim: I find myself lost in there all the time. So, uh, I get, I can imagine that, yeah, it’s very highly likely that your message would have been like either, either ignored or you would have generated such a heated discussion that it would have been like, let’s, yeah.

[00:42:25] Rahul Kumar: I’ve seen a few of those recently.

[00:42:27] Tim: Okay. Yeah. Right.

Collaborative Efforts and Academic Contributions

[00:42:29] Tim: Um, there is actually an effort outside of AWS that I noticed that you posted about. So I, uh, there was, I saw a YouTube video from CMU students, uh, about verifying the standard library. And your name is attached there somehow. So what’s your relationship with the university, with the academic project?

And, uh, presumably there’s some wider context that I think would be really nice to hear about.

[00:43:02] Rahul Kumar: Yeah. Oh, I mean, you are up to date, obviously. Uh, so, uh, CMU has, um, uh, uh, an initiative, um, an innovators initiative, which, uh, where they, they do what’s called a practicum project, these are students who end up spending a semester selecting what projects they want to work on from a, a proposed set of projects. Uh, just so,

[00:43:33] Tim: I was going to interject very slightly just in case there’s any listeners that know Latin. I’ve always called that practicum, but practicum, I, anyway, the, I’m like, uh, yeah, it’s funny how we have kind of the like English holds on in tiny, tiny fragments of like, uh, and let’s say a more learned age, although much more colonial and far.

[00:44:00] Rahul Kumar: still spell knife with a K

[00:44:02] Tim: Yeah, sure. That’s right. Yeah. The K N thing. I don’t get like knife, knave. Anyway, sorry. I completely derailed you. And yes, so we have practicum, which, uh, probably provides an opportunity for students to work on an industry project. That’s just normally how these things are structured.

[00:44:20] Rahul Kumar: There’s actually a wide variety of sponsors who come there. Uh, they’re, they’re from either academia or industry. And, uh, uh, we got, so I got the opportunity to present this idea for verifying the Rust standard library, and we ended up with four teams, four very wonderful teams, I might add, uh, four plus one students each, uh, four students, one, one kind of, uh, program manager person, uh, a couple of faculty members, and they took on four challenges. You know, let me, me tell you, uh, not all of these students had any formal verification background. Some of them did not have any Rust background. Yes, that reaction is correct.

[00:45:17] Tim: Yeah. And I’m sorry if any of them is audio only. Yeah. I’m, I’m like, so they’re sitting here kind of like slightly puzzled or startled. Amazed. I can’t quite tell. I don’t know which adjective is correct, but that’s fascinating.

[00:45:30] Rahul Kumar: And Each team took on a challenge. Uh, we completed a couple of challenges. Uh, the other two are, are almost finished. And students happen to be engaged even after the work is done. They have created blog posts, videos. They learned how to write Kani harnesses. They learned about Rust semantics. They pushed Kani to a new level.

They were filing issues against Kani saying this doesn’t work. Was absolutely inspirational see these students take this idea and actually make it a reality. And, you know, in my head, I thought, wow, this is the birth of a new generation of, computer scientists.

[00:46:17] Tim: Yeah,

[00:46:18] Rahul Kumar: me at the end.

[00:46:21] Tim: that’s also, I, yeah, I, there are like multiple levels in which I’m amazed. And the first of all, like being able to recruit four teams of multiple researchers, uh, most of all that is like, uh, like that, that, that, that isn’t like an acknowledgement of essentially the gravity or, uh, of, of, of, of this effort, um, and the way that it’s perceived and the importance of Rust.

Rust is no longer, I think I’ve been saying this for like about a year, Rust is no longer a new language. Like Rust is novel anymore in the sense of it’s not considered unsafe. Sorry, wrong term. It’s not considered kind of a, I don’t think that there will be companies that look at Rust and think, ah, right, right.

That’s a, that’s, that’s a, yeah, totally. And.

[00:47:19] Rahul Kumar: I

[00:47:21] Tim: in, in, on that side where people know that if they were to work on this, that, and like solve one of these challenges,

[00:47:31] Rahul Kumar: Um.

[00:47:33] Tim: large impact all around the world. Um, the other level was that, yeah, these people were, sorry, these students were relatively new either to formal verification, Rust or both, still were able to make Really strong forward progress, which means that the tools themselves, such as Kani and its ability to have custom properties and harnesses, uh, is is learnable.

And that’s very, very positive. Um, and then this continuing engagement and being able to create content about exploration and blog posts and so forth is a very nice finishing touch because it means that people have been sufficiently engaged to share, which means that, uh, they, they, you know, the whole process was fulfilling.

I mean, I don’t want to gush too much about this effort and, uh, but no, no, no, it’s, it’s, it’s, very ambitious and I am extremely excited that someone has decided to use their position, uh, and like their expertise in the networks to drive this. And so I, so thank you to you.

[00:48:50] Rahul Kumar: Oh, thank you, Tim. I, I, I have a lot of people to thank, uh, you know, uh, the Rust Foundation has been amazing during this process. Uh, Amazon itself has actually put money forward and, and my leadership has been very supportive. People like you who understand, my team has just done so much work. I mean, We started the year with zero verified functions, and we ended the year with 255 or a few more now verified functions, basically one a day, uh, if you will. Uh, that’s really cool. And, and next year, you know, we wanna increase the order of magnitude. We want to get into the thousands, and we want to get this into the mainline, uh, the contracts. Rust is going to have contracts soon, and we’ve been a part of those discussions. It is a great thing to have contracts at the end of the day. a great thing to have formal verification come into this light, because I do believe those are the only guardrails has eventually. Um,

[00:50:10] Tim: Yeah, look, I mean, you can’t ask the AI to just write a test that will, it would be nice to make sure that, that the thing is doing what it says that it’s doing. And that it’s essentially not spiraling. Out into mayhem. Uh, and yes, the Rust compiler, you know, once it compiles, it runs and you kind of, you have some degree of assurance that you at least have a working program, but it would be nice to go that next extra step to say that you have a correct program.

Um, No. Amazing. And thank you all.

[00:50:50] Rahul Kumar: only nice, but required

opinion.

[00:50:54] Tim: Yeah, but see this is the, this is the whole frame of reference in which I’m currently operating in that at the moment we don’t have the idea that it’s possible to formally verify, kind of baked into the process. And so it’s seen by, at least, you know, you can tell that my.

Our own preconceptions are kind of like pushing against the idea that this could become a part of every day. In fact, it will become central to it because it will be the foundation that the rest of the program sits on, especially if this future comes true where the computer is doing a lot of the writing of the software.

Conclusion and Future Prospects

[00:51:41] Tim: And, uh, yeah, no, so thank you very much for sharing with, uh, with everybody, uh, the story of, um, of verifying the Rust standard library, as well as, uh, something which I was very unexpected to me, this idea of essentially, um, creating this secure foundation for a new paradigm of software development. And, um, in 20 years, we might have another conversation and find out, um, whether or not.

It happened or like what it actually looks like. So I, uh, I wish you all the best.

[00:52:14] Rahul Kumar: Thank you. Thank you very much. And, uh, I hope it’s sooner than 20 years.

[00:52:18] Tim: Yeah. Yeah. Right. Right. Okay. People can take their bets.