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.
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?
Yeah, so, uh, very first I'm going to say, no, there's no lies here, right?
That would be a bit aggressive.
Okay, sure.
an amazing programming language, which provides Fantastic, fantastic
compile time guarantees that most other languages will not provide you.
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.
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?
That's, that's a wonderful way to say it.
And you use an interesting word in there called proof,
Uh huh.
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.
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.
So the And just, because there are a couple of people who are
terrified of this keyword, unsafe.
will.
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.
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
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.
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.
Okay.
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.
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?
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.
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,
Yeah, I think I think the word, uh, which would be appropriate here is semantics.
right?
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.
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
Right,
this funny,
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?
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.
Mmm.
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 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.
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,
Yeah, they're modeling.
Well, at least LAPLUS is definitely a, a, Click here.
Mm hmm.
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.
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,
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.
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.
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
Okay.
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.
Incredible.
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
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.
the box.
But you can by encoding a custom property, yes.
Wow.
give you the ability to, ability to, yeah.
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,
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,
Floating point is much harder than integers, which is why I brought it up.
Oh yeah,
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,
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?
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.
That's extremely exciting.
Do you think that the, although I'm just going to wait for my
dog to decide to stop barking.
Sure.
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?
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,
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?
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,
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.
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.
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,
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.
I'm right.
I love tokens.
Here's, here's a thousand.
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.
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.
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.
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,
get a second line.
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,
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?
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.
Same in Finland, right?
They don't have checkbooks.
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.
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.
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?
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,
We don't talk about these things.
yeah.
Yeah.
It turns out it's just software.
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,
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.
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?
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.
tell you exactly when I thought that.
Okay.
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.
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.
Sure.
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.
I've seen a few of those recently.
Okay.
Yeah.
Right.
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.
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,
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.
still spell knife with a K
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.
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.
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.
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.
Yeah,
me at the end.
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.
I
in, in, on that side where people know that if they were to work on this, that,
and like solve one of these challenges,
Um.
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.
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,
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.
only nice, but required
opinion.
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.
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.
Thank you.
Thank you very much.
And, uh, I hope it's sooner than 20 years.
Yeah.
Right.
Okay.
People can take their bets.
You've been listening to Compose, a podcast for software developers interested
in the Rust programming language.
My name is Tim McNamara, also known as timclicks, and you can find
further resources at timclicks.
dev.
At timclicks.
dev you'll find tutorials, videos and articles all geared around helping you
to get better at the Rust programming language to build a better planet.
If you've enjoyed this episode, then here's a suggestion.
Try to apply formal verification to one of your projects today.
Check the show notes for resources
Check the show notes for links to resources for you to get started.
Take care.
Have fun.
I'll see you on the next episode.