1
00:00:00,049 --> 00:00:07,749
So my name is Rahul Kumar and I'm a
Senior Applied Science Manager at AWS.
2
00:00:08,369 --> 00:00:15,695
I lead a team that works on Rust
verification, C code verification, And,
3
00:00:15,695 --> 00:00:23,494
uh, we are very, very passionate about
bringing formal methods into, uh, the
4
00:00:23,494 --> 00:00:28,035
mainstream, especially for Rust, which
is what this work is about and what
5
00:00:28,075 --> 00:00:29,374
I'm going to talk about a bit more.
6
00:00:30,174 --> 00:00:34,864
Uh, previously, I worked at
Microsoft, Microsoft Research.
7
00:00:35,635 --> 00:00:42,145
I worked on decode verification
um, a little bit of empirical
8
00:00:42,145 --> 00:00:44,045
software engineering techniques.
9
00:00:45,035 --> 00:00:49,494
And then, uh, before that, I also worked
on the Europa Clipper mission at NASA JPL.
10
00:00:50,304 --> 00:00:51,785
So, very exciting.
11
00:01:15,037 --> 00:01:18,687
The first question to ask, I suppose,
is , what is formal verification?
12
00:01:18,697 --> 00:01:23,667
But can I actually intercept myself
by asking something else, which is , I
13
00:01:23,697 --> 00:01:29,327
thought Rust was a safe programming
language and you made a special
14
00:01:29,327 --> 00:01:33,987
note to say, that you are especially
interested in verifying Rust.
15
00:01:34,037 --> 00:01:40,607
And so, can you describe to me, like,
what the dist, like, how Rust is sort
16
00:01:40,607 --> 00:01:42,437
of, like, uh, is Rust lying to us?
17
00:01:42,467 --> 00:01:45,687
Like, what's, what ne, what are, what
are the holes that need to be filled?
18
00:01:47,216 --> 00:01:52,716
Yeah, so, uh, very first I'm going to
say, no, there's no lies here, right?
19
00:01:53,526 --> 00:01:54,856
That would be a bit aggressive.
20
00:01:55,967 --> 00:01:56,517
Okay, sure.
21
00:01:56,546 --> 00:02:02,901
an amazing programming language,
which provides Fantastic, fantastic
22
00:02:03,141 --> 00:02:06,811
compile time guarantees that most
other languages will not provide you.
23
00:02:07,541 --> 00:02:12,261
Rust does have an escape path
to perform certain functions.
24
00:02:12,746 --> 00:02:15,576
And, uh, that's called
the unsafe part of Rust.
25
00:02:15,836 --> 00:02:22,186
It provides you so called superpowers to,
achieve what you're looking to, to do.
26
00:02:23,026 --> 00:02:26,646
there are various reasons why
one may choose to adopt those.
27
00:02:26,956 --> 00:02:29,186
So, number one, no lies.
28
00:02:29,186 --> 00:02:29,931
Number two, no lies.
29
00:02:30,281 --> 00:02:34,221
Yes, we have an escape path, and
at that point the compiler will
30
00:02:34,231 --> 00:02:38,221
stop giving you guarantees that it
traditionally would in SafeRust.
31
00:02:39,011 --> 00:02:40,861
Now, does that mean?
32
00:02:41,531 --> 00:02:47,171
That basically means that the compiler
is expecting some sort of human
33
00:02:47,231 --> 00:02:54,231
assist, or potentially AI assist
in the future, to, to enable you to
34
00:02:54,241 --> 00:02:55,781
give the guarantees for yourself.
35
00:02:57,272 --> 00:03:02,592
So I would normally describe this as
the burden of proof kind of shifts from
36
00:03:02,592 --> 00:03:04,722
the compiler to you as the programmer.
37
00:03:04,892 --> 00:03:08,732
Do you kind of, how does
that sentence fit with you?
38
00:03:09,841 --> 00:03:11,701
That's, that's a wonderful way to say it.
39
00:03:11,761 --> 00:03:15,001
And you use an interesting
word in there called proof,
40
00:03:15,452 --> 00:03:15,842
Uh huh.
41
00:03:16,821 --> 00:03:21,561
Because the compiler is actually in
the safe world, giving you proof that
42
00:03:21,561 --> 00:03:26,691
you're okay, but in the unsafe world,
it is not giving you that proof.
43
00:03:27,661 --> 00:03:32,341
while you may run this particular piece
of code a million times and never have
44
00:03:32,341 --> 00:03:37,101
an issue, have a guarantee, which is
what the proof will give you at the end.
45
00:03:37,431 --> 00:03:40,371
And yes, the burden of
proof is on the programmer.
46
00:03:41,402 --> 00:03:41,702
Right.
47
00:03:41,702 --> 00:03:46,142
I, I need to kind of, uh, I
did an undergraduate degree
48
00:03:46,142 --> 00:03:47,232
in philosophy actually.
49
00:03:47,272 --> 00:03:55,112
Um, and just kind of like, this is sort of
bringing up like old neurons are activated
50
00:03:55,192 --> 00:03:59,957
about like, Inductive and versus deductive
logic and the fact that essentially
51
00:04:00,277 --> 00:04:03,007
it doesn't matter how many times it's
right if we if you can't guarantee
52
00:04:03,007 --> 00:04:05,417
that Uh that it might never be wrong.
53
00:04:05,467 --> 00:04:13,127
You you still never have um that
kind of quality and uh, I sure yeah.
54
00:04:13,127 --> 00:04:13,317
Yeah.
55
00:04:13,317 --> 00:04:14,137
No, absolutely.
56
00:04:14,167 --> 00:04:18,067
So the And just, because there
are a couple of people who are
57
00:04:18,127 --> 00:04:20,117
terrified of this keyword, unsafe.
58
00:04:20,511 --> 00:04:23,901
will.
59
00:04:24,167 --> 00:04:27,987
is why we might use this escape hatch.
60
00:04:27,997 --> 00:04:32,107
And sometimes it's impossible to
avoid, such as if I want to talk
61
00:04:32,107 --> 00:04:38,467
to the operating system, or I need
to talk to some, uh, other library.
62
00:04:38,977 --> 00:04:44,787
That might be written in different
programming language, uh, and it's
63
00:04:44,787 --> 00:04:47,927
impossible for the Rust compiler to
guarantee, make some, any, some sort of
64
00:04:47,927 --> 00:04:52,957
assertion or guarantee about programs that
other, that live somewhere else, that,
65
00:04:53,197 --> 00:04:57,147
that those are, that's one case where
it might be impossible to avoid unsafe.
66
00:04:58,821 --> 00:05:04,551
Yeah, uh, uh, you know, you want to,
you want to use some foreign, uh,
67
00:05:04,561 --> 00:05:10,181
language interface or you want to
dereference raw pointers, uh, the,
68
00:05:10,211 --> 00:05:15,761
the so called five superpowers that
Rust has in, in all of those cases.
69
00:05:16,576 --> 00:05:23,216
Either you are functionally bound and
you want to, to achieve a, a particular
70
00:05:23,246 --> 00:05:27,696
function at the end, or a functionality
at the end, which you're, you're
71
00:05:27,776 --> 00:05:29,866
not able to do because of SafeRUS.
72
00:05:30,126 --> 00:05:35,446
Great, that's a perfectly valid
reason to do this, or maybe there is a
73
00:05:35,466 --> 00:05:40,636
performance concern because the SafeRUS
could potentially introduce checks that
74
00:05:40,666 --> 00:05:45,146
you are not very interested in having.
75
00:05:45,451 --> 00:05:47,481
And it causes a performance slowdown.
76
00:05:48,971 --> 00:05:50,961
again, back
77
00:05:50,997 --> 00:05:51,087
so.
78
00:05:52,737 --> 00:05:59,217
At this point, it's this temptation
of, well, I could go faster.
79
00:05:59,517 --> 00:06:04,917
Like I essentially, uh, I know that
there are, I know like in sort of scare
80
00:06:04,917 --> 00:06:07,897
quotes there, because I might be wrong.
81
00:06:07,927 --> 00:06:11,117
Like it turns out that humans are
often wrong about these things, but you
82
00:06:11,117 --> 00:06:15,677
know, for as far as I can see as the
programmer, uh, I am upholding invariance
83
00:06:15,717 --> 00:06:17,497
around memory safety and so forth.
84
00:06:18,227 --> 00:06:22,647
And so I could, uh, essentially
skip safety checks that the.
85
00:06:23,047 --> 00:06:27,917
Compiler would otherwise kind of
inject and yeah, and then suddenly
86
00:06:27,917 --> 00:06:31,677
I'd get like a, let's say, I don't
know, a two or 3 percent speed
87
00:06:31,677 --> 00:06:34,827
up in code that might be, yeah.
88
00:06:34,917 --> 00:06:35,217
Okay.
89
00:06:35,337 --> 00:06:35,727
Interesting.
90
00:06:36,461 --> 00:06:44,101
Yeah, so imagine, uh, developer, uh, X,
uh, tasked by their manager to take a
91
00:06:44,121 --> 00:06:50,641
piece of C code and manager says, you
know, I want you to go make this in Rust
92
00:06:50,651 --> 00:06:52,521
because I've heard it's safe and faster.
93
00:06:53,311 --> 00:06:58,326
And, uh, And developer X goes and
rewrites it in Rust, in SafeRust,
94
00:06:58,336 --> 00:07:03,326
and turns out it's actually the same
performance as the C code, because there's
95
00:07:03,326 --> 00:07:05,556
a bunch of safety injections in there.
96
00:07:06,756 --> 00:07:11,646
then they experiment and go into
unsafe mode, and turns out it's
97
00:07:11,646 --> 00:07:16,856
actually a lot faster, but now we
don't have a proof of correctness,
98
00:07:16,876 --> 00:07:18,986
which the SafeRust would have provided.
99
00:07:19,947 --> 00:07:20,337
Okay.
100
00:07:21,076 --> 00:07:26,466
at that point, Yes, the burden of
proof is on the developer and that's
101
00:07:26,466 --> 00:07:30,576
a simple motivational example that
this has happened in real life.
102
00:07:30,606 --> 00:07:32,306
We have seen examples of this.
103
00:07:33,306 --> 00:07:42,236
Um, unsafe for us tends to have a very,
very useful function and support it.
104
00:07:43,216 --> 00:07:50,366
The, the place that we are coming from
is Even if it's unsafe, why don't we
105
00:07:50,366 --> 00:07:54,666
go provide you those assurances that
would not have been possible before?
106
00:07:55,626 --> 00:08:03,736
And that's amazing because, uh, now you
can probably go into unsafe and achieve
107
00:08:03,736 --> 00:08:10,076
the functions that you want to achieve
still have guarantees for the future.
108
00:08:11,402 --> 00:08:14,412
So, and this is verification.
109
00:08:14,642 --> 00:08:19,082
So I expect that the term formal
verification has, has a very
110
00:08:19,082 --> 00:08:22,502
precise technical meaning, do
you want to, is that correct?
111
00:08:22,502 --> 00:08:24,092
And if so, do you want to flesh that out?
112
00:08:24,926 --> 00:08:28,016
mathema yes, uh, we want
to use mathematical logic.
113
00:08:28,646 --> 00:08:37,896
Uh, to prove properties about your
programs and, and formal verification, in
114
00:08:37,896 --> 00:08:43,296
a sense, you know, you could say, well,
I want to go verify a model of something.
115
00:08:43,306 --> 00:08:47,686
That's fine as well, but the, the
artifact that you are dealing with,
116
00:08:47,706 --> 00:08:51,176
which you are most interested in
will exhibit certain properties,
117
00:08:51,206 --> 00:08:56,296
and we want to go prove properties
about that, about that artifact, and
118
00:08:56,296 --> 00:09:03,426
we want to prove them Exclusively,
unboundedly, impermanence, if you will.
119
00:09:04,626 --> 00:09:09,286
I suppose one of the things that was
fascinating to me about one of the tools
120
00:09:09,286 --> 00:09:13,816
that hopefully we'll get to chat about
called Kani was that it's all symbolic.
121
00:09:13,846 --> 00:09:17,946
The actual code itself doesn't really
get executed and kind of get, as far as
122
00:09:17,946 --> 00:09:26,346
I can tell, gets translated and then run
through an SAT solver and then, uh, yeah.
123
00:09:26,346 --> 00:09:30,316
And so it's, it's, it's almost as though.
124
00:09:30,921 --> 00:09:38,041
You're operating with software, not as a
set of instructions for a computer to kind
125
00:09:38,041 --> 00:09:41,521
of go from top to bottom through, like
you might think of it scanning through
126
00:09:41,521 --> 00:09:46,291
assembly, but as a series of symbolic
instructions, so much more sort of a high
127
00:09:46,291 --> 00:09:54,281
level, um, and just the structure of the
way that the program is operating allows,
128
00:09:54,281 --> 00:09:59,166
um, The solver or that was the tooling
to some, make some sort of inference or
129
00:09:59,166 --> 00:10:01,616
actually no deduction about correctness,
130
00:10:03,190 --> 00:10:08,430
Yeah, I think I think the word, uh, which
would be appropriate here is semantics.
131
00:10:08,676 --> 00:10:08,706
right?
132
00:10:09,400 --> 00:10:14,075
So semantics and, and
then specification, right?
133
00:10:14,365 --> 00:10:21,815
So, we, we take the, the input
and we process it according to
134
00:10:21,815 --> 00:10:23,775
the semantics that are defined.
135
00:10:24,585 --> 00:10:29,025
And interestingly enough, there are
situations with programming languages
136
00:10:29,805 --> 00:10:31,905
where semantics are undefined.
137
00:10:33,375 --> 00:10:35,955
And that's something that we
would like to also change.
138
00:10:36,450 --> 00:10:42,560
So attacking this core problem of let's
go verify the Rust standard library,
139
00:10:42,570 --> 00:10:44,250
let's go verify the core library.
140
00:10:44,490 --> 00:10:51,360
Well, we're, we're now in a place where
we're challenging a community to actually
141
00:10:51,370 --> 00:10:54,380
formally define the semantics, right?
142
00:10:54,830 --> 00:10:56,620
Uh, there's
143
00:10:56,691 --> 00:10:57,171
Right,
144
00:10:57,230 --> 00:10:58,030
this funny,
145
00:10:58,281 --> 00:11:03,971
so if, uh, hopefully an example will
pop into your head just immediately,
146
00:11:04,151 --> 00:11:08,131
but if essentially there's a gap in
the specification where it kind of
147
00:11:08,131 --> 00:11:12,421
provides wriggle room, which makes
it essentially impossible to verify
148
00:11:12,621 --> 00:11:14,711
because there's ambiguity there.
149
00:11:14,751 --> 00:11:16,981
Is that the problem that there is?
150
00:11:17,330 --> 00:11:21,190
and, and a funny party trick,
right, that, that used to be
151
00:11:21,220 --> 00:11:26,210
played, uh, in, in the math clubs
was, Oh, let me prove 1 equals 0.
152
00:11:26,851 --> 00:11:27,321
Mmm.
153
00:11:27,520 --> 00:11:34,695
the essential idea was that you're
dividing by x minus x, And you can go
154
00:11:34,695 --> 00:11:39,635
prove one equals zero to somebody who
doesn't realize that this particular
155
00:11:39,735 --> 00:11:41,935
semantics is not, is prohibited.
156
00:11:41,975 --> 00:11:42,885
It's not allowed.
157
00:11:44,135 --> 00:11:50,415
uh, uh, with the Russ or with a lot of
programming languages, in fact, maybe all,
158
00:11:50,415 --> 00:11:57,205
I'm not sure, uh, it is, it is true that
there are gaps in the defined semantics.
159
00:11:57,845 --> 00:11:59,705
And we would like to close out on that.
160
00:12:00,905 --> 00:12:06,975
Formal verification would I associate,
or at least I have been associating
161
00:12:06,975 --> 00:12:13,565
with things like TLA or, uh, There are
a couple of other modeling languages.
162
00:12:13,605 --> 00:12:17,105
Some are easier to use than others,
but typically they are difficult
163
00:12:17,475 --> 00:12:20,305
and very complex and challenging.
164
00:12:20,875 --> 00:12:32,585
Um, uh, Do you have any thoughts
on why these, uh, Uh, Why formal
165
00:12:32,585 --> 00:12:41,265
verification is so difficult for,
let's say most programmers, and that
166
00:12:41,275 --> 00:12:43,355
it seems like a very specialized topic.
167
00:12:44,555 --> 00:12:50,375
So, so I will give you that it
is specialized, uh, number one.
168
00:12:50,385 --> 00:12:54,465
Number two, I, I think that the
examples you cite are also interesting
169
00:12:54,465 --> 00:13:01,165
because they're not directly what
a software engineer would go write
170
00:13:01,185 --> 00:13:03,105
and deploy at the end of the day,
171
00:13:03,501 --> 00:13:04,321
Yeah, they're modeling.
172
00:13:04,341 --> 00:13:07,021
Well, at least LAPLUS is
definitely a, a, Click here.
173
00:13:07,021 --> 00:13:15,801
Mm hmm.
174
00:13:15,920 --> 00:13:22,130
Veris, uh, would fit into that domain
where we're actually trying to operate
175
00:13:22,240 --> 00:13:25,910
on the code that is being deployed.
176
00:13:26,670 --> 00:13:32,800
And one of the goals for us is to
make this as automated as possible.
177
00:13:33,545 --> 00:13:39,745
So, yes, do you, do you, would we
like you to specify properties?
178
00:13:40,445 --> 00:13:41,155
Absolutely.
179
00:13:42,085 --> 00:13:44,185
Right, because that's
something that you know about.
180
00:13:44,525 --> 00:13:45,415
You know your code.
181
00:13:46,185 --> 00:13:49,335
But do we want you to go create models?
182
00:13:49,585 --> 00:13:50,295
Probably not.
183
00:13:50,345 --> 00:13:52,605
We're, we're trying to do that for you.
184
00:13:53,315 --> 00:13:53,645
And we
185
00:13:54,275 --> 00:13:54,665
for you.
186
00:13:55,706 --> 00:13:59,476
And so it sounds like one of the barriers
has been, well, you need to, if you
187
00:13:59,476 --> 00:14:03,256
want to learn formal verification or at
least some subset of the domain, then
188
00:14:03,256 --> 00:14:08,606
you need to go learn a modeling language
and, uh, and create a specification.
189
00:14:08,826 --> 00:14:14,441
Whereas let's say newer tools or the
tools The Kani in particular, uh,
190
00:14:14,441 --> 00:14:20,711
essentially it's just Rust code and,
um, it's actually embedded in the
191
00:14:20,791 --> 00:14:22,241
code that you're actually running.
192
00:14:22,241 --> 00:14:23,571
It's not some separate artifact.
193
00:14:23,851 --> 00:14:29,861
And so, um, I mean, I personally,
when I've used Kani have really
194
00:14:29,861 --> 00:14:33,651
appreciated that, that essentially the
tooling kind of comes to me and that
195
00:14:33,651 --> 00:14:37,211
I don't need to go out to something
else and use a different workflow.
196
00:14:37,271 --> 00:14:40,061
I can just use Cargo,
for example, to drive it.
197
00:14:40,141 --> 00:14:40,801
Um, I think.
198
00:14:41,091 --> 00:14:41,661
Um,
199
00:14:42,421 --> 00:14:42,611
and,
200
00:14:43,811 --> 00:14:50,391
uh, the ergonomics of making this
real and scalable are so important.
201
00:14:50,711 --> 00:14:57,001
And, you know, uh, imagine being in a
meeting where you go from discussing
202
00:14:57,011 --> 00:15:03,811
highly symbolic execution oriented
algorithms, uh, and problems with them to,
203
00:15:04,031 --> 00:15:09,251
well, we think this should be Not start
with a star, it should be an ampersand.
204
00:15:09,681 --> 00:15:14,081
Um, and, and, you know,
both are amazingly valid.
205
00:15:14,871 --> 00:15:19,221
Because if you want to push formal
verification to the next frontier, make
206
00:15:19,221 --> 00:15:22,401
it part of the mainline, is what it takes.
207
00:15:22,741 --> 00:15:25,031
You have to work on both
ends of the spectrum.
208
00:15:26,651 --> 00:15:31,021
You can go make the best engine
in the world, you don't have a
209
00:15:31,021 --> 00:15:34,631
beautiful car on top of it, people
aren't really going to drive it.
210
00:15:36,182 --> 00:15:45,622
Yeah, I, I spend a lot of time picking at,
uh, syntax as well, even though it feels
211
00:15:46,152 --> 00:15:53,762
in some sense, meaningless or trivial or
somehow less important, but really nice.
212
00:15:54,082 --> 00:15:54,752
syntax.
213
00:15:54,862 --> 00:15:59,242
It kind of lends itself to
really nice programs in a way.
214
00:16:00,212 --> 00:16:05,982
And, uh, and, and so the struggle
is, is, is kind of real, I think,
215
00:16:05,992 --> 00:16:09,272
when you're designing a language
about, do we use curly braces?
216
00:16:09,272 --> 00:16:10,282
Do we use angle braces?
217
00:16:11,842 --> 00:16:21,542
But, um, the, uh, the idea here is
that we have a A tool, Kani in this
218
00:16:21,542 --> 00:16:30,682
case, which can take Rust code, uh,
reason about it symbolically, uh, and
219
00:16:30,712 --> 00:16:37,902
essentially make some sort of guarantee
or that the properties of correctness.
220
00:16:39,357 --> 00:16:46,367
Maintained through the use of
unsafe, uh, surely, but surely
221
00:16:46,367 --> 00:16:47,657
the project is not yet done.
222
00:16:48,157 --> 00:16:52,777
Are there kind of known limitations where,
I mean, presumably that there are, you,
223
00:16:52,937 --> 00:16:54,207
you know, where the gaps are, I hope.
224
00:16:55,407 --> 00:16:55,707
Right.
225
00:16:55,717 --> 00:16:58,697
So I have, I have, uh, two
or three things to say here.
226
00:16:58,887 --> 00:17:01,207
So number one, it's number one.
227
00:17:01,277 --> 00:17:07,377
Uh, yes, we do have limitations and we
publish them and, and believe me, we are
228
00:17:07,807 --> 00:17:15,567
absolutely 100 percent on the ball about
making sure we publish these because
229
00:17:15,967 --> 00:17:17,567
no false guarantee should be made.
230
00:17:18,847 --> 00:17:19,167
Right.
231
00:17:19,517 --> 00:17:25,057
Number two, uh, there is a distinction
between these generic properties
232
00:17:25,577 --> 00:17:28,347
versus user oriented properties
233
00:17:29,883 --> 00:17:30,363
Okay.
234
00:17:31,527 --> 00:17:36,302
right, and you can make Uh, you
can, you can go check for certain
235
00:17:36,312 --> 00:17:40,932
UBs which come right out of the box
with Connie because, hey, that just
236
00:17:40,932 --> 00:17:42,702
applies to everything in Rust, right?
237
00:17:43,122 --> 00:17:48,092
Uh, but then if you want to go
say, I'm very highly interested
238
00:17:48,352 --> 00:17:52,772
that this particular variable
never exceeds the value of 42.
239
00:17:53,972 --> 00:17:56,562
Okay, you can go write
that property and prove it.
240
00:17:57,277 --> 00:18:00,297
And, uh, there's a fascinating example.
241
00:18:00,307 --> 00:18:02,997
There's a repository out
there called HiFiTime.
242
00:18:02,997 --> 00:18:08,917
And there's a blog post on the
Connie blog about, uh, proving
243
00:18:08,917 --> 00:18:10,587
the correctness of HiFiTime.
244
00:18:11,157 --> 00:18:19,047
Uh, it's a, it's a time library for
the, the solar system, if you will,
245
00:18:19,167 --> 00:18:25,372
operating across multiple, And, uh,
Christopher Rabbitin, uh, who wrote the
246
00:18:25,372 --> 00:18:31,022
blog post with us or mostly by himself,
uh, but we reviewed it, which was nice.
247
00:18:31,382 --> 00:18:37,092
Uh, of the first external contributions
to the Connie blog, uh, picked
248
00:18:37,092 --> 00:18:43,762
up on Connie and used it to prove
correctness of, of so many functions.
249
00:18:44,827 --> 00:18:47,147
For the next 36, 000 years.
250
00:18:48,823 --> 00:18:49,293
Incredible.
251
00:18:50,297 --> 00:18:50,797
Right.
252
00:18:51,007 --> 00:18:55,167
And, and that's, those are such custom
properties that he's working with, right?
253
00:18:55,547 --> 00:18:57,077
Uh, amazing stuff.
254
00:18:57,377 --> 00:19:03,287
Uh, AWS Firecracker, which, uh, is
a VMM that is open source on GitHub.
255
00:19:03,287 --> 00:19:05,787
And, and we rely on that quite a bit.
256
00:19:06,167 --> 00:19:11,187
They have so many custom properties that
they prove about, about their code base.
257
00:19:11,507 --> 00:19:14,347
And, and how they deal
with certain issues.
258
00:19:15,162 --> 00:19:20,652
Those are fascinating, uh, user
oriented functional properties
259
00:19:20,652 --> 00:19:21,612
that people are proving.
260
00:19:22,912 --> 00:19:26,552
In addition to the generic UBs that they
261
00:19:26,593 --> 00:19:26,953
Sure.
262
00:19:27,373 --> 00:19:31,323
So can I, just as a hypothetical,
I'm not sure, like, I literally
263
00:19:31,323 --> 00:19:32,253
don't know if this is possible.
264
00:19:33,413 --> 00:19:37,673
It would be wonderful to have a per,
uh, let's say a percentage type,
265
00:19:37,703 --> 00:19:40,613
which is encoded as floating point,
although maybe it should be irrational
266
00:19:40,883 --> 00:19:43,283
using a, a, um, an instrument.
267
00:19:43,283 --> 00:19:44,183
But let's say it's not.
268
00:19:44,633 --> 00:19:50,513
And so I'm using floating and I want to
guarantee that the use of my percentage
269
00:19:50,543 --> 00:19:52,553
is always between zero and one.
270
00:19:52,703 --> 00:19:57,443
So essentially, um, it's bounded
with inside those, um, with, uh,
271
00:19:57,743 --> 00:19:59,423
is that something that I can ask?
272
00:19:59,663 --> 00:20:03,293
Kani to chick so that I
should never be able to have.
273
00:20:03,412 --> 00:20:04,462
the box.
274
00:20:05,702 --> 00:20:10,032
But you can by encoding
a custom property, yes.
275
00:20:10,643 --> 00:20:11,043
Wow.
276
00:20:11,182 --> 00:20:13,472
give you the ability to, ability to, yeah.
277
00:20:14,863 --> 00:20:15,103
Yeah.
278
00:20:15,103 --> 00:20:21,193
I, um, I've always kind of been
in, uh, there's a part of Ada,
279
00:20:21,193 --> 00:20:25,723
which I have always been fascinated
by, which whereby you can have.
280
00:20:26,153 --> 00:20:31,573
Types which are constrained by their
ranges rather than being, rather
281
00:20:31,573 --> 00:20:34,643
than having all integers available to
you, you've just got some subset and,
282
00:20:34,743 --> 00:20:40,903
um, I've always wondered how that is
implemented because the representation
283
00:20:40,903 --> 00:20:45,633
in memory is presumably just an
integer, or for example, and, um,
284
00:20:45,862 --> 00:20:48,782
so you bring up specifically
floating points, which I think we
285
00:20:48,782 --> 00:20:52,822
have a bug on, but I'm not sure.
286
00:20:53,102 --> 00:20:54,382
Let me be clear about that.
287
00:20:54,412 --> 00:20:56,412
And we claim that in our list,
288
00:20:57,813 --> 00:21:01,153
Floating point is much harder than
integers, which is why I brought it up.
289
00:21:01,223 --> 00:21:01,413
Oh yeah,
290
00:21:01,832 --> 00:21:03,022
that's kind of where I was going.
291
00:21:03,022 --> 00:21:03,302
Right?
292
00:21:03,302 --> 00:21:04,522
So if you're sticking to integers,
you're sticking to integers.
293
00:21:04,672 --> 00:21:06,922
Yes, you can restrict
it, uh, floating points.
294
00:21:06,922 --> 00:21:11,712
I believe we are, we're trying to,
there's certain SIMD instructions where
295
00:21:11,932 --> 00:21:14,292
we're, we're have like a small issue.
296
00:21:14,642 --> 00:21:19,262
Um, modulo becomes interesting, you know,
297
00:21:20,052 --> 00:21:21,072
uh, incomplete.
298
00:21:21,072 --> 00:21:21,522
So,
299
00:21:22,433 --> 00:21:26,423
Look, I think, look, the fact that
these are the goals that you're striving
300
00:21:26,423 --> 00:21:34,823
for, and I know, I mean, it's sort
of incredible and, uh, I wonder how
301
00:21:34,823 --> 00:21:40,288
that would translate Through unsafe,
like we've got, you've mentioned
302
00:21:40,288 --> 00:21:44,488
UBs are like a general thing, class
of problems that we wish to avoid.
303
00:21:44,488 --> 00:21:50,028
So we want to remove the possibility
of unsafe or sorry, undefined behavior.
304
00:21:50,648 --> 00:21:55,488
Um, I suppose this would be classified
at build time or at test time.
305
00:21:55,868 --> 00:21:57,608
Um, and.
306
00:21:58,748 --> 00:22:06,828
One question, Mark, that I, uh, that's
kind of lingering around is how Kani
307
00:22:06,848 --> 00:22:10,718
differs from other tools in its space
that are achieving similar things, such
308
00:22:10,718 --> 00:22:14,078
as like the Mirri, uh, is an interpreter.
309
00:22:14,078 --> 00:22:16,878
So this operates in a significant,
its model of operation is
310
00:22:17,318 --> 00:22:18,188
much different, isn't it?
311
00:22:19,712 --> 00:22:22,062
yes, yes, this is a great question.
312
00:22:22,062 --> 00:22:24,912
So, you know, there's a,
there's a spectrum of tools.
313
00:22:25,492 --> 00:22:31,502
And, and each one, and every single
tool comes with its benefits.
314
00:22:31,927 --> 00:22:32,397
Right.
315
00:22:32,827 --> 00:22:39,197
Uh, uh, you, you can start with,
with basic dynamic execution.
316
00:22:39,997 --> 00:22:43,617
Uh, you can go to testing, you
can go to fuzz testing, you can
317
00:22:43,617 --> 00:22:47,107
go into model checking, which
is where Connie fits, right?
318
00:22:47,137 --> 00:22:53,417
Then you go into deductive logic based
tools and higher order logic based tools.
319
00:22:53,687 --> 00:23:01,437
Uh, spectrum is, is, is very important
because, The effort that we have,
320
00:23:01,477 --> 00:23:04,177
you know, coming back to the Rust
standard library verification
321
00:23:04,177 --> 00:23:07,217
effort, it's not about Connie.
322
00:23:08,417 --> 00:23:17,087
It's about ensuring that we can
use this spectrum of tools to go
323
00:23:17,097 --> 00:23:18,787
give guarantees for the future.
324
00:23:19,987 --> 00:23:25,607
An effort, like at a very basic level,
an effort is a collection of people
325
00:23:25,837 --> 00:23:28,947
who are trying to achieve a goal.
326
00:23:29,217 --> 00:23:32,537
And one of the first things they
do is create a demonstration
327
00:23:32,547 --> 00:23:35,337
that, hey, I can go do something.
328
00:23:36,837 --> 00:23:41,922
And what we have done thus
far is given a demonstration.
329
00:23:43,362 --> 00:23:49,222
And the hope is, the idea is that more
and more people join this effort and bring
330
00:23:49,222 --> 00:23:51,662
in their specialties and their tools.
331
00:23:52,862 --> 00:23:54,722
That's extremely exciting.
332
00:23:54,732 --> 00:23:58,592
Do you think that the, although
I'm just going to wait for my
333
00:23:58,592 --> 00:24:00,702
dog to decide to stop barking.
334
00:24:01,091 --> 00:24:01,371
Sure.
335
00:24:02,571 --> 00:24:04,901
I think someone just came
home, which makes us excited.
336
00:24:05,471 --> 00:24:06,701
The, um,
337
00:24:07,901 --> 00:24:09,421
here's a question for you.
338
00:24:09,691 --> 00:24:12,641
Do you think there are a large
number of tools that are sitting
339
00:24:12,811 --> 00:24:16,831
in the darkness waiting to kind
of be revealed to the world?
340
00:24:18,031 --> 00:24:25,181
I don't know if sitting in the darkness is
a phrase I would use, but there are, there
341
00:24:25,211 --> 00:24:28,201
are a lot of tools that, that can be used.
342
00:24:28,201 --> 00:24:28,711
Yeah.
343
00:24:29,041 --> 00:24:34,481
Look at tools like, uh, Cruzeau,
I I Nia is a great example.
344
00:24:34,981 --> 00:24:36,881
I think that's a wonderful tool.
345
00:24:37,071 --> 00:24:39,511
We are borrowing concepts from ideas.
346
00:24:39,841 --> 00:24:41,721
Uh, Veris is a great example.
347
00:24:42,401 --> 00:24:48,021
You know, Connie, of course, since
we happen to be closely related to
348
00:24:48,031 --> 00:24:52,951
Connie, that's how we wanted to make
the demonstration and jumpstart.
349
00:24:54,221 --> 00:24:54,711
That's it,
350
00:24:55,882 --> 00:24:58,772
So let's talk about this,
this kind of project.
351
00:24:59,972 --> 00:25:07,622
We started chatting before, uh, uh,
on LinkedIn because I posted a note
352
00:25:07,742 --> 00:25:16,442
about something that I read, uh, that
came as a joint effort from the Rust
353
00:25:16,442 --> 00:25:21,212
Foundation and AWS, and your name was
attached, at least on the AWS side.
354
00:25:21,582 --> 00:25:25,602
So, uh, what is it that
you're trying to do?
355
00:25:26,802 --> 00:25:35,302
Very simply put, we want to deliver
the new era of programming language.
356
00:25:36,942 --> 00:25:42,322
So, you know, we live in a world
where AI has already proven to be
357
00:25:42,322 --> 00:25:44,402
very useful for certain aspects.
358
00:25:45,592 --> 00:25:52,057
Um, Uh, I don't know how much you use
it per se, but you know, there's people
359
00:25:52,057 --> 00:25:56,097
summarizing things, there's people
rewriting things, there's people now
360
00:25:56,097 --> 00:25:59,217
starting to make 20 second videos, uh,
361
00:25:59,678 --> 00:26:07,978
Yeah, look, I, I, I actually am,
uh, Increasingly surprised at how
362
00:26:08,028 --> 00:26:09,638
effective it is at getting me.
363
00:26:09,668 --> 00:26:13,758
I think when chat GPT first came out, it
was like really good at getting me like
364
00:26:13,758 --> 00:26:17,398
a first draft for some sort of piece
of content that I wanted to produce.
365
00:26:17,398 --> 00:26:22,368
And now that, um, and now the models
and also the tooling around the models
366
00:26:22,368 --> 00:26:27,388
and some, uh, and, and the increasing
capabilities around rag, which is,
367
00:26:27,428 --> 00:26:30,548
um, I can't actually remember what it
expands out to, but the ability that you
368
00:26:30,548 --> 00:26:35,258
could actually teach models about your
custom, your own content means that.
369
00:26:36,353 --> 00:26:38,693
It's getting better and better at
source code and relatively complex.
370
00:26:40,013 --> 00:26:41,483
The context windows are increasing.
371
00:26:41,483 --> 00:26:42,163
La la la la la.
372
00:26:42,523 --> 00:26:51,873
So, uh, I am, uh, I would say I am
one of the people that are, that
373
00:26:51,883 --> 00:26:58,673
have high expectations for, for, um,
for AI and its ability to remove a
374
00:26:58,673 --> 00:27:03,673
lot of tedium from the process of
programming and a lot of mistakes.
375
00:27:03,753 --> 00:27:10,128
Uh, I think that, uh, It is, um,
but I'm also relatively skeptical.
376
00:27:10,138 --> 00:27:14,708
Like I'd rather be late and allow
other people to feel the pain.
377
00:27:16,447 --> 00:27:17,317
Yeah, absolutely.
378
00:27:17,647 --> 00:27:23,267
And, and, you know, I'm gonna tie
AI back to a previous comment or
379
00:27:23,267 --> 00:27:24,612
discussion actually, that we had.
380
00:27:25,342 --> 00:27:29,342
You, you can go test something a million
times and just because it doesn't fail
381
00:27:29,342 --> 00:27:35,062
doesn't mean it won't fail, uh, and AI,
we all know we've actually experienced
382
00:27:35,062 --> 00:27:40,512
the hallucinations to, to some degree
where, uh, you're like, well, that's
383
00:27:40,512 --> 00:27:41,922
not exactly what I was looking for.
384
00:27:42,162 --> 00:27:49,062
Now, AI is also, AI is also beneficial
in accelerating us unprecedented levels.
385
00:27:49,777 --> 00:27:55,167
Uh, when it comes to development
of products and services and
386
00:27:55,167 --> 00:27:58,697
code, do I, do I not want that?
387
00:27:58,737 --> 00:28:00,547
Of course, of course I want that.
388
00:28:00,987 --> 00:28:04,017
But do I want appropriate
guardrails around it?
389
00:28:04,407 --> 00:28:10,167
Which help me develop confidence
that, yes, I know that this
390
00:28:10,207 --> 00:28:11,387
AI gave me the right thing.
391
00:28:11,817 --> 00:28:14,007
And that's where formal
verification comes in.
392
00:28:14,437 --> 00:28:16,737
That's where this effort comes in.
393
00:28:17,027 --> 00:28:19,697
Because formal verification is the answer.
394
00:28:20,372 --> 00:28:21,892
for producing those guardrails.
395
00:28:22,853 --> 00:28:23,273
Right.
396
00:28:23,313 --> 00:28:24,333
So, okay.
397
00:28:24,453 --> 00:28:31,213
So now you have told a model, please
generate a piece of code or, you
398
00:28:31,213 --> 00:28:34,913
know, like fix this feature or fix
this bug in, but, but you also need.
399
00:28:35,688 --> 00:28:39,238
But it kind of gets constrained by
the fact that the tests must pass.
400
00:28:39,278 --> 00:28:42,208
And by the way, the tests
are not just tests anymore.
401
00:28:42,418 --> 00:28:44,818
They're formal verifications
of correctness.
402
00:28:45,118 --> 00:28:45,628
Um,
403
00:28:47,067 --> 00:28:47,427
yeah.
404
00:28:48,217 --> 00:28:52,757
And that's a very strong statement
because Um, say you want to go update
405
00:28:52,757 --> 00:28:55,817
your library and it has dependencies.
406
00:28:56,807 --> 00:28:58,257
The AI says, sure, no problem.
407
00:28:59,157 --> 00:28:59,587
Here you go.
408
00:28:59,647 --> 00:29:00,677
Here's a bunch of tokens.
409
00:29:01,047 --> 00:29:02,307
I'm just going to go spit them at you.
410
00:29:02,498 --> 00:29:03,538
I'm right.
411
00:29:04,738 --> 00:29:05,318
I love tokens.
412
00:29:05,318 --> 00:29:06,848
Here's, here's a thousand.
413
00:29:07,827 --> 00:29:12,387
And then here's Rahul sitting on his
computer going, uh, should I commit this?
414
00:29:12,397 --> 00:29:13,897
Should I approve this for request?
415
00:29:13,927 --> 00:29:15,667
I'm not sure what's going to happen here.
416
00:29:16,377 --> 00:29:20,477
But then, uh, the formal verification
tool kicks in and says, Hey, guess what?
417
00:29:20,497 --> 00:29:23,097
We've just proved that this is great.
418
00:29:23,207 --> 00:29:23,377
It.
419
00:29:23,682 --> 00:29:24,242
Works.
420
00:29:24,492 --> 00:29:26,442
It's equivalent to what you had before.
421
00:29:27,142 --> 00:29:27,432
for it.
422
00:29:28,323 --> 00:29:29,093
Hmm.
423
00:29:29,823 --> 00:29:30,193
Yeah.
424
00:29:30,213 --> 00:29:35,963
I, uh, and now essentially, well, yeah,
that that's just a huge new paradigm
425
00:29:36,353 --> 00:29:41,413
of writing software that, uh, you kind
of have like this human augmentation.
426
00:29:41,693 --> 00:29:47,933
Um, and I think that will are immensely
powerful, particularly at big, big,
427
00:29:47,943 --> 00:29:54,023
big places where you have lots of hulky
projects that there's never enough.
428
00:29:54,083 --> 00:29:57,183
It's really, I know that people say
that we have these trillion dollar
429
00:29:57,183 --> 00:30:02,303
companies, but being someone who's
worked inside one of them, no one ever
430
00:30:02,303 --> 00:30:04,383
has budget for like massive rewrites.
431
00:30:04,743 --> 00:30:11,053
And so I think this will
liberate a lot of, uh, of people.
432
00:30:12,688 --> 00:30:18,588
Yeah, one of the things I really
appreciate about Rust is that
433
00:30:19,218 --> 00:30:25,008
you can feel, is the notion
of this fearless concurrency.
434
00:30:26,498 --> 00:30:30,858
That was the first, pretty much
the first slogan that people really
435
00:30:30,878 --> 00:30:35,108
understood when Rust came, like
first came out like 2012, 2013.
436
00:30:35,688 --> 00:30:41,678
Fearless concurrency was one, and uh,
and the other one would be blazing fast.
437
00:30:41,678 --> 00:30:41,728
Rust.
438
00:30:42,078 --> 00:30:44,418
Those were the two
things that really stuck.
439
00:30:46,218 --> 00:30:49,848
And now it sounds like what
you're saying is the future.
440
00:30:49,848 --> 00:30:53,748
If we, if, if we get it right, like
it's not, it is literally a future
441
00:30:53,748 --> 00:30:57,928
that is not, there's lots of things
that might go wrong, but in principle,
442
00:30:58,658 --> 00:31:00,458
the tooling should get sufficient.
443
00:31:00,548 --> 00:31:06,608
Such that, that feeling of, uh, being
fearless, essentially knowing that
444
00:31:06,608 --> 00:31:13,128
you can't crash, uh uh, you can't.
445
00:31:14,723 --> 00:31:18,843
Your programs will carry on
because they'll be correct.
446
00:31:18,953 --> 00:31:20,513
You actually know that.
447
00:31:20,693 --> 00:31:24,833
That would be an immensely liberating
feeling, um, for people that
448
00:31:24,953 --> 00:31:27,863
are building, which is amazing.
449
00:31:28,967 --> 00:31:29,387
Yes.
450
00:31:29,627 --> 00:31:31,817
And you know, I, I'll
451
00:31:32,567 --> 00:31:37,497
a few decades, uh, which some people
may or may not relate to, but the
452
00:31:37,497 --> 00:31:42,757
amount of times we had to reboot a
computer, uh, and, and the, and the
453
00:31:42,757 --> 00:31:47,917
wastage that that produced, imagine
if you never have to deal with that.
454
00:31:49,117 --> 00:31:50,562
is almost perfect.
455
00:31:50,962 --> 00:31:55,952
But yeah, no, no, and there
are some very strange things.
456
00:31:55,952 --> 00:32:01,962
I mean, if people who, people who
didn't grow up or didn't experience
457
00:32:01,962 --> 00:32:03,622
the dial up era of the internet.
458
00:32:04,882 --> 00:32:06,112
Well, never really.
459
00:32:07,312 --> 00:32:12,892
Once upon a time, you needed to literally
plug the modem into the wall, like
460
00:32:12,962 --> 00:32:18,942
unplug the phone because you could either
have a phone or the computer would be
461
00:32:18,942 --> 00:32:21,112
talking on the internet and you'd pay,
462
00:32:21,386 --> 00:32:22,456
get a second line.
463
00:32:22,722 --> 00:32:23,422
right, right.
464
00:32:24,622 --> 00:32:26,772
And, and, and things like email.
465
00:32:27,962 --> 00:32:33,812
It felt different because you on, on
Outlook or like Thunderbird or whatever,
466
00:32:34,672 --> 00:32:40,252
there was a button like send and receive
because literally you need to phone in and
467
00:32:40,262 --> 00:32:42,982
download things from messages that come
in from the server and like re upload.
468
00:32:43,242 --> 00:32:44,477
Now we think of.
469
00:32:44,777 --> 00:32:47,037
Email is essentially instant messaging.
470
00:32:47,127 --> 00:32:48,447
We're always connected.
471
00:32:48,887 --> 00:32:52,397
The protocol actually expects that
everything is asynchronous and so forth.
472
00:32:52,397 --> 00:32:58,217
It still operates in an era where the
whole, uh, everything is disconnected
473
00:32:58,397 --> 00:33:04,412
and flaky, but messaging, is different.
474
00:33:04,432 --> 00:33:05,822
The internet feels different.
475
00:33:05,822 --> 00:33:06,872
It's essentially,
476
00:33:07,156 --> 00:33:15,411
and imagine the future computer
scientist, which uses AI to but guarantees
477
00:33:15,411 --> 00:33:17,131
the work with formal verification.
478
00:33:18,381 --> 00:33:22,981
Like, you know, uh, you and
I probably sat down in IDEs
479
00:33:22,981 --> 00:33:25,741
and wrote code and debug code.
480
00:33:27,211 --> 00:33:30,441
That's going to be an
extinct, antiquated activity.
481
00:33:31,641 --> 00:33:34,071
It's like, at some point people
are going to be like, Grandpa,
482
00:33:34,071 --> 00:33:36,231
so you used to have an IDE?
483
00:33:37,592 --> 00:33:37,992
yeah.
484
00:33:38,002 --> 00:33:42,222
Well, I think, I think of this, like
my immediate, my, and it's interesting,
485
00:33:42,222 --> 00:33:46,632
I'm just kind of thinking about
my own response to your comment.
486
00:33:47,212 --> 00:33:49,842
My immediate was like, it's kind of
this, you know, this kind of back
487
00:33:49,842 --> 00:33:55,352
and it's like, no way, Rahul, you,
you, this is, this is nonsense.
488
00:33:55,892 --> 00:33:57,632
And then it's like, what, pause?
489
00:33:58,622 --> 00:34:05,987
I think the same way about, uh,
Financial transactions in America.
490
00:34:06,217 --> 00:34:10,627
So in the United States,
checks are used everywhere.
491
00:34:11,877 --> 00:34:13,447
New Zealand stopped accepting checks.
492
00:34:13,477 --> 00:34:17,067
Like banks don't literally, you can't
seem to use a check in our country.
493
00:34:17,686 --> 00:34:18,696
Same in Finland, right?
494
00:34:18,696 --> 00:34:19,926
They don't have checkbooks.
495
00:34:21,007 --> 00:34:30,457
Yeah, it's like, not a thing
there's, and, uh, uh, and so, and
496
00:34:30,557 --> 00:34:34,297
we don't expect that messages are
going to be, are going to be seen.
497
00:34:34,337 --> 00:34:38,517
I was going to say telegram or
something like things change and,
498
00:34:39,117 --> 00:34:43,277
uh, the tools will get good enough.
499
00:34:44,122 --> 00:34:52,382
That the boring work of like literally
typing, touching the keyboard, getting
500
00:34:52,692 --> 00:34:59,082
the program written will be done the
hard part of the system design, the hard
501
00:34:59,082 --> 00:35:04,322
part of like developing the product, the,
the finding how the components work and,
502
00:35:04,322 --> 00:35:09,462
and that will still, you'll be driving
that, but you're essentially, you'll be,
503
00:35:09,662 --> 00:35:14,182
yeah, you will be driving these, these AI
agents to essentially create or co create.
504
00:35:15,217 --> 00:35:22,297
Um, some sort of artifact and that will
be difficult shift for many people.
505
00:35:22,797 --> 00:35:27,387
And, but I think that overall it'll be.
506
00:35:28,587 --> 00:35:32,287
Like artisanal, artisanal software
development where, you know, people
507
00:35:32,287 --> 00:35:36,817
will, it's just like having like
handmade, handmade shoes feels, uh,
508
00:35:37,117 --> 00:35:43,747
very, um, very old fashioned and very,
I think I'm forgetting a word, but,
509
00:35:44,097 --> 00:35:47,822
but some people still like to have,
to have, um, Shoes made by hand.
510
00:35:47,892 --> 00:35:50,042
And lots of people would
love to pay if they could.
511
00:35:50,292 --> 00:35:54,442
Um, and in Japan, we still have handmade
shoes, but, um, in lots of places, but
512
00:35:54,892 --> 00:35:59,882
most people's shoes are made in factories
and, uh, and, and they're mass produced.
513
00:36:00,152 --> 00:36:03,412
And so I think most software will
be in some sense, mass produced.
514
00:36:04,612 --> 00:36:10,257
well, and, Uh, And I think maybe
the way I think about it is we're
515
00:36:10,257 --> 00:36:16,837
moving one level of abstraction
up, so it's no longer about, about,
516
00:36:17,197 --> 00:36:18,957
Oh, how do I write this function?
517
00:36:18,957 --> 00:36:21,517
It's more about, I'm writing this object.
518
00:36:21,547 --> 00:36:25,257
I'm creating this object, which knows
how to interact with other objects.
519
00:36:25,557 --> 00:36:32,037
And then now we're saying, don't
even worry about the object, Class.
520
00:36:32,087 --> 00:36:32,917
Don't worry about that.
521
00:36:33,137 --> 00:36:35,047
Now move on to, let's.
522
00:36:35,827 --> 00:36:37,917
modules that you're working on.
523
00:36:38,267 --> 00:36:42,117
Your problem solving techniques are
now coming into the module because
524
00:36:42,117 --> 00:36:49,007
the rest of the stuff we can go manage
and we can do it with guardrails in
525
00:36:49,007 --> 00:36:51,037
place, with verification in place.
526
00:36:52,523 --> 00:36:54,143
The future that you're describing here.
527
00:36:54,163 --> 00:36:59,353
I look, I think I, you know, it's
very, it's very easy to, oh, like
528
00:36:59,473 --> 00:37:02,123
there's a bootstrapping problem
where if you start with a program,
529
00:37:02,153 --> 00:37:03,473
you need to kind of handwrite.
530
00:37:03,983 --> 00:37:06,943
The, the, the, the, the
properties that you wish to kind
531
00:37:06,943 --> 00:37:08,283
of guarantee, blah, blah, blah.
532
00:37:08,843 --> 00:37:13,983
And, but yeah, but it's just
a kind of a fascinating idea.
533
00:37:14,043 --> 00:37:20,353
So then the question that becomes
like, why would, what is important
534
00:37:20,453 --> 00:37:25,893
about the Rust standard library
as part of this overall process?
535
00:37:27,093 --> 00:37:31,143
Why is that the next thing to do?
536
00:37:32,372 --> 00:37:36,622
Yeah, so, there's two parts,
or well, three parts to it.
537
00:37:36,972 --> 00:37:45,022
One, the Rust standard library, know, uh,
contrary to popular belief, does have bugs
538
00:37:45,022 --> 00:37:47,262
in it which have been exposed in the past.
539
00:37:47,932 --> 00:37:49,492
Yes, uh,
540
00:37:49,623 --> 00:37:50,793
We don't talk about these things.
541
00:37:51,862 --> 00:37:52,192
yeah.
542
00:37:52,473 --> 00:37:52,713
Yeah.
543
00:37:52,753 --> 00:37:53,583
It turns out it's just software.
544
00:37:54,783 --> 00:37:59,768
so, so, When you want to build
a house, where do you start?
545
00:38:00,968 --> 00:38:03,768
You start with the foundation
and our foundation is the
546
00:38:03,768 --> 00:38:04,958
core and the standard library.
547
00:38:05,718 --> 00:38:14,318
if we can, not if, but when we make
our tools actually do this for the
548
00:38:14,328 --> 00:38:22,838
core, the foundation automagically,
yes, automagically, we can start making
549
00:38:22,838 --> 00:38:25,668
it work for everything else above it.
550
00:38:26,723 --> 00:38:28,533
And that's the number one reason,
551
00:38:29,224 --> 00:38:32,964
So is part of the reason why that
magic happens is once the tools are
552
00:38:32,964 --> 00:38:36,334
good enough to do it in the standard
library, which is in some sense the
553
00:38:36,334 --> 00:38:43,174
most impactful, uh, you know, like,
uh, library that Rust programmers have
554
00:38:43,214 --> 00:38:50,434
access to, um, then everywhere else
should be at least no more difficult.
555
00:38:51,634 --> 00:38:51,974
Yes.
556
00:38:51,994 --> 00:38:53,614
That's a great insight on your part.
557
00:38:53,734 --> 00:38:56,384
That is, that is one of
the ideas here, right?
558
00:38:56,694 --> 00:39:02,464
That the, the second point is the Rust
Center Library will challenge our tools.
559
00:39:03,344 --> 00:39:06,674
will make us push the boundary.
560
00:39:07,684 --> 00:39:10,304
And that's fantastic, right?
561
00:39:11,785 --> 00:39:20,955
Your, uh, I suppose that the, the fact
that a lot of Rust programmers use non,
562
00:39:21,075 --> 00:39:25,285
the no standard attributes, such that
essentially they turn off the standard
563
00:39:25,285 --> 00:39:30,685
library is slightly orthogonal to this,
because if I'm just on an embedded device,
564
00:39:31,130 --> 00:39:32,800
I could still use the verification tools.
565
00:39:32,800 --> 00:39:33,630
They still exist.
566
00:39:33,880 --> 00:39:39,960
And, um, but essentially this is a
big, ambitious, difficult project.
567
00:39:40,250 --> 00:39:46,630
Um, and you're attempting to use the, the,
the program of work as a way to kind of
568
00:39:46,630 --> 00:39:56,440
recruit or, uh, essentially kind of gather
a community of researchers to, uh, or at
569
00:39:56,440 --> 00:40:04,430
least this is kind of kind of, I'm trying
to figure out where, at what point did you
570
00:40:04,430 --> 00:40:06,375
think Think, you know what we should do?
571
00:40:06,965 --> 00:40:10,205
We should turn this into like
an X prize, like an awards.
572
00:40:10,555 --> 00:40:13,095
Uh, you know, we should,
we should essentially.
573
00:40:13,184 --> 00:40:14,924
tell you exactly when I thought that.
574
00:40:15,285 --> 00:40:15,615
Okay.
575
00:40:16,624 --> 00:40:21,044
It's when I realized the amount of
unsafe code in the Rust standard library.
576
00:40:21,694 --> 00:40:26,014
And, okay, one team
cannot actually do this.
577
00:40:26,624 --> 00:40:28,684
I need a lot more support.
578
00:40:29,064 --> 00:40:37,734
And then, you know, uh, I, believe the
Rust community is an amazing community.
579
00:40:38,679 --> 00:40:42,159
It has been a fascinating
community for me, at least.
580
00:40:42,899 --> 00:40:46,799
I realized, well, I think
that people would like to
581
00:40:46,799 --> 00:40:49,969
contribute because three reasons.
582
00:40:49,969 --> 00:40:54,309
Number one, benefits everyone, right?
583
00:40:54,369 --> 00:40:59,029
This benefits, it benefits people who
are building on top of Rust, creating
584
00:40:59,029 --> 00:41:01,029
their applications, their scenarios.
585
00:41:01,349 --> 00:41:04,079
It benefits people who
are developing Rust.
586
00:41:04,289 --> 00:41:10,349
It benefits academia, students,
uh, researchers, industry.
587
00:41:10,849 --> 00:41:12,949
Uh, it's a win, win, win, win.
588
00:41:13,699 --> 00:41:19,449
And, uh, I thought, well, okay, but
you know, if I just go post a message
589
00:41:19,449 --> 00:41:22,979
saying, Hey, let's go verify the
Rust library, well, it's probably
590
00:41:22,979 --> 00:41:27,459
going to get drowned in the, in the
plethora and the sea of, of, uh, all
591
00:41:27,459 --> 00:41:28,889
the messages that are being posted.
592
00:41:29,949 --> 00:41:34,739
So the effort was born out of
let's make it more organized
593
00:41:34,799 --> 00:41:36,389
and let's jumpstart this.
594
00:41:36,819 --> 00:41:39,849
Because I think there's a lot of
people who are motivated out there
595
00:41:40,939 --> 00:41:46,699
who want to do something like this,
this gives them a great cause.
596
00:41:47,415 --> 00:41:47,665
Hmm.
597
00:41:48,575 --> 00:41:48,605
Okay.
598
00:41:49,805 --> 00:41:54,455
Yeah, the Rust community is not, by
the Rust community, the messages,
599
00:41:54,485 --> 00:41:57,055
where the message are presumably you
would have sent if you would have sort
600
00:41:57,055 --> 00:42:00,275
of say, Hi, by the way, I'm looking
for, would have been like the Zulip
601
00:42:00,605 --> 00:42:02,975
channel, like the main one, presumably.
602
00:42:03,244 --> 00:42:03,634
Sure.
603
00:42:04,075 --> 00:42:08,095
I find myself lost in there all the time.
604
00:42:08,305 --> 00:42:14,915
So, uh, I get, I can imagine that,
yeah, it's very highly likely that your
605
00:42:14,915 --> 00:42:20,555
message would have been like either,
either ignored or you would have
606
00:42:20,555 --> 00:42:25,175
generated such a heated discussion that
it would have been like, let's, yeah.
607
00:42:25,284 --> 00:42:26,904
I've seen a few of those recently.
608
00:42:27,160 --> 00:42:27,760
Okay.
609
00:42:27,890 --> 00:42:28,070
Yeah.
610
00:42:28,070 --> 00:42:28,340
Right.
611
00:42:29,540 --> 00:42:37,920
Um, there is actually an effort outside of
AWS that I noticed that you posted about.
612
00:42:37,920 --> 00:42:45,800
So I, uh, there was, I saw a YouTube
video from CMU students, uh, about
613
00:42:45,810 --> 00:42:47,620
verifying the standard library.
614
00:42:48,230 --> 00:42:51,090
And your name is attached there somehow.
615
00:42:51,150 --> 00:42:54,910
So what's your relationship with the
university, with the academic project?
616
00:42:54,940 --> 00:43:00,200
And, uh, presumably there's some
wider context that I think would
617
00:43:00,200 --> 00:43:01,380
be really nice to hear about.
618
00:43:02,580 --> 00:43:03,060
Yeah.
619
00:43:03,060 --> 00:43:05,600
Oh, I mean, you are up to date, obviously.
620
00:43:05,910 --> 00:43:13,410
Uh, so, uh, CMU has, um, uh, uh, an
initiative, um, an innovators initiative,
621
00:43:14,630 --> 00:43:20,730
which, uh, where they, they do what's
called a practicum project, these are
622
00:43:20,730 --> 00:43:27,720
students who end up spending a semester
selecting what projects they want to work
623
00:43:27,720 --> 00:43:30,560
on from a, a proposed set of projects.
624
00:43:31,720 --> 00:43:32,480
Uh, just so,
625
00:43:33,606 --> 00:43:35,596
I was going to interject very
slightly just in case there's
626
00:43:35,596 --> 00:43:37,086
any listeners that know Latin.
627
00:43:37,436 --> 00:43:43,904
I've always called that practicum,
but practicum, I, anyway, the, I'm
628
00:43:43,904 --> 00:43:52,241
like, uh, yeah, it's funny how we
have kind of the like English holds
629
00:43:52,241 --> 00:43:57,651
on in tiny, tiny fragments of like,
uh, and let's say a more learned age,
630
00:43:57,801 --> 00:44:00,401
although much more colonial and far.
631
00:44:00,430 --> 00:44:02,170
still spell knife with a K
632
00:44:02,376 --> 00:44:02,986
Yeah, sure.
633
00:44:03,196 --> 00:44:03,776
That's right.
634
00:44:03,976 --> 00:44:04,336
Yeah.
635
00:44:04,676 --> 00:44:05,906
The K N thing.
636
00:44:05,936 --> 00:44:07,446
I don't get like knife, knave.
637
00:44:07,726 --> 00:44:08,836
Anyway, sorry.
638
00:44:08,886 --> 00:44:10,276
I completely derailed you.
639
00:44:10,566 --> 00:44:15,606
And yes, so we have practicum, which,
uh, probably provides an opportunity for
640
00:44:15,606 --> 00:44:17,386
students to work on an industry project.
641
00:44:17,416 --> 00:44:19,576
That's just normally how
these things are structured.
642
00:44:20,310 --> 00:44:23,560
There's actually a wide variety
of sponsors who come there.
643
00:44:24,140 --> 00:44:27,690
Uh, they're, they're from
either academia or industry.
644
00:44:28,125 --> 00:44:35,235
And, uh, uh, we got, so I got the
opportunity to present this idea for
645
00:44:35,235 --> 00:44:41,985
verifying the Rust standard library,
and we ended up with four teams, four
646
00:44:41,985 --> 00:44:48,095
very wonderful teams, I might add, uh,
four plus one students each, uh, four
647
00:44:48,125 --> 00:44:54,895
students, one, one kind of, uh, program
manager person, uh, a couple of faculty
648
00:44:54,895 --> 00:44:58,715
members, and they took on four challenges.
649
00:44:59,770 --> 00:45:07,700
You know, let me, me tell you, uh,
not all of these students had any
650
00:45:07,860 --> 00:45:09,610
formal verification background.
651
00:45:10,810 --> 00:45:13,860
Some of them did not
have any Rust background.
652
00:45:15,060 --> 00:45:17,300
Yes, that reaction is correct.
653
00:45:17,726 --> 00:45:17,946
Yeah.
654
00:45:17,946 --> 00:45:20,316
And I'm sorry if any
of them is audio only.
655
00:45:21,766 --> 00:45:21,976
Yeah.
656
00:45:21,976 --> 00:45:25,016
I'm, I'm like, so they're sitting here
kind of like slightly puzzled or startled.
657
00:45:25,066 --> 00:45:25,596
Amazed.
658
00:45:25,596 --> 00:45:26,336
I can't quite tell.
659
00:45:26,426 --> 00:45:29,336
I don't know which adjective is
correct, but that's fascinating.
660
00:45:30,850 --> 00:45:34,530
And Each team took on a challenge.
661
00:45:34,860 --> 00:45:37,650
Uh, we completed a couple of challenges.
662
00:45:37,930 --> 00:45:40,690
Uh, the other two are,
are almost finished.
663
00:45:41,050 --> 00:45:45,170
And students happen to be engaged
even after the work is done.
664
00:45:45,190 --> 00:45:47,830
They have created blog posts, videos.
665
00:45:48,280 --> 00:45:50,770
They learned how to write Kani harnesses.
666
00:45:51,080 --> 00:45:53,040
They learned about Rust semantics.
667
00:45:53,340 --> 00:45:55,720
They pushed Kani to a new level.
668
00:45:55,720 --> 00:45:59,090
They were filing issues against
Kani saying this doesn't work.
669
00:46:00,290 --> 00:46:07,450
Was absolutely inspirational see
these students take this idea
670
00:46:08,460 --> 00:46:09,900
and actually make it a reality.
671
00:46:09,910 --> 00:46:14,380
And, you know, in my head, I thought,
wow, this is the birth of a new
672
00:46:14,380 --> 00:46:17,100
generation of, computer scientists.
673
00:46:17,501 --> 00:46:17,991
Yeah,
674
00:46:18,650 --> 00:46:19,750
me at the end.
675
00:46:21,201 --> 00:46:26,021
that's also, I, yeah, I, there are like
multiple levels in which I'm amazed.
676
00:46:27,221 --> 00:46:32,671
And the first of all, like being able
to recruit four teams of multiple
677
00:46:32,671 --> 00:46:38,671
researchers, uh, most of all that is like,
uh, like that, that, that, that isn't
678
00:46:38,961 --> 00:46:45,641
like an acknowledgement of essentially
the gravity or, uh, of, of, of, of
679
00:46:45,641 --> 00:46:49,971
this effort, um, and the way that it's
perceived and the importance of Rust.
680
00:46:51,051 --> 00:46:55,021
Rust is no longer, I think I've been
saying this for like about a year,
681
00:46:55,261 --> 00:46:56,741
Rust is no longer a new language.
682
00:46:57,971 --> 00:47:06,751
Like Rust is novel anymore in the
sense of it's not considered unsafe.
683
00:47:07,581 --> 00:47:08,311
Sorry, wrong term.
684
00:47:08,551 --> 00:47:13,401
It's not considered kind of a, I don't
think that there will be companies that
685
00:47:13,401 --> 00:47:16,001
look at Rust and think, ah, right, right.
686
00:47:16,011 --> 00:47:18,011
That's a, that's, that's a, yeah, totally.
687
00:47:18,351 --> 00:47:18,801
And.
688
00:47:19,426 --> 00:47:21,102
I
689
00:47:21,411 --> 00:47:28,051
in, in, on that side where people know
that if they were to work on this, that,
690
00:47:28,461 --> 00:47:30,481
and like solve one of these challenges,
691
00:47:31,159 --> 00:47:32,835
Um.
692
00:47:33,361 --> 00:47:36,811
large impact all around the world.
693
00:47:37,531 --> 00:47:41,051
Um, the other level was that, yeah,
these people were, sorry, these
694
00:47:41,051 --> 00:47:46,011
students were relatively new either
to formal verification, Rust or both,
695
00:47:46,291 --> 00:47:50,166
still were able to make Really strong
forward progress, which means that
696
00:47:50,196 --> 00:47:54,126
the tools themselves, such as Kani and
its ability to have custom properties
697
00:47:54,126 --> 00:47:57,316
and harnesses, uh, is is learnable.
698
00:47:57,736 --> 00:48:00,216
And that's very, very positive.
699
00:48:00,666 --> 00:48:07,126
Um, and then this continuing engagement
and being able to create content about
700
00:48:07,186 --> 00:48:12,236
exploration and blog posts and so
forth is a very nice finishing touch
701
00:48:12,256 --> 00:48:18,356
because it means that people have been
sufficiently engaged to share, which
702
00:48:18,386 --> 00:48:22,326
means that, uh, they, they, you know,
the whole process was fulfilling.
703
00:48:22,336 --> 00:48:29,926
I mean, I don't want to gush too much
about this effort and, uh, but no, no, no,
704
00:48:29,926 --> 00:48:40,001
it's, it's, it's, very ambitious and I am
extremely excited that someone has decided
705
00:48:41,421 --> 00:48:46,411
to use their position, uh, and like their
expertise in the networks to drive this.
706
00:48:46,411 --> 00:48:48,701
And so I, so thank you to you.
707
00:48:50,450 --> 00:48:51,550
Oh, thank you, Tim.
708
00:48:51,600 --> 00:48:57,250
I, I, I have a lot of people to thank,
uh, you know, uh, the Rust Foundation
709
00:48:57,260 --> 00:48:59,250
has been amazing during this process.
710
00:48:59,720 --> 00:49:05,660
Uh, Amazon itself has actually
put money forward and, and my
711
00:49:05,660 --> 00:49:08,470
leadership has been very supportive.
712
00:49:08,750 --> 00:49:16,350
People like you who understand, my
team has just done so much work.
713
00:49:16,370 --> 00:49:22,385
I mean, We started the year with
zero verified functions, and
714
00:49:22,385 --> 00:49:28,195
we ended the year with 255 or a
few more now verified functions,
715
00:49:28,705 --> 00:49:32,245
basically one a day, uh, if you will.
716
00:49:32,635 --> 00:49:35,335
Uh, that's really cool.
717
00:49:35,335 --> 00:49:38,815
And, and next year, you know, we
wanna increase the order of magnitude.
718
00:49:38,815 --> 00:49:41,955
We want to get into the thousands,
and we want to get this into
719
00:49:41,955 --> 00:49:44,405
the mainline, uh, the contracts.
720
00:49:45,445 --> 00:49:50,415
Rust is going to have contracts soon, and
we've been a part of those discussions.
721
00:49:51,615 --> 00:49:56,195
It is a great thing to have
contracts at the end of the day.
722
00:49:57,105 --> 00:50:03,075
a great thing to have formal
verification come into this light,
723
00:50:03,175 --> 00:50:08,865
because I do believe those are the
only guardrails has eventually.
724
00:50:09,655 --> 00:50:10,225
Um,
725
00:50:10,571 --> 00:50:18,111
Yeah, look, I mean, you can't ask the AI
to just write a test that will, it would
726
00:50:18,121 --> 00:50:24,331
be nice to make sure that, that the thing
is doing what it says that it's doing.
727
00:50:24,491 --> 00:50:27,951
And that it's essentially not spiraling.
728
00:50:29,161 --> 00:50:30,731
Out into mayhem.
729
00:50:30,991 --> 00:50:35,831
Uh, and yes, the Rust compiler, you know,
once it compiles, it runs and you kind of,
730
00:50:36,201 --> 00:50:42,141
you have some degree of assurance that you
at least have a working program, but it
731
00:50:42,141 --> 00:50:46,341
would be nice to go that next extra step
to say that you have a correct program.
732
00:50:46,841 --> 00:50:48,836
Um, No.
733
00:50:48,836 --> 00:50:49,526
Amazing.
734
00:50:49,706 --> 00:50:50,636
And thank you all.
735
00:50:50,715 --> 00:50:52,565
only nice, but required
736
00:50:53,215 --> 00:50:53,715
opinion.
737
00:50:54,915 --> 00:50:58,545
Yeah, but see this is the, this is
the whole frame of reference in which
738
00:50:59,055 --> 00:51:06,915
I'm currently operating in that at
the moment we don't have the idea
739
00:51:06,975 --> 00:51:12,565
that it's possible to formally verify,
kind of baked into the process.
740
00:51:12,805 --> 00:51:17,965
And so it's seen by, at least,
you know, you can tell that my.
741
00:51:18,480 --> 00:51:22,080
Our own preconceptions are kind of
like pushing against the idea that
742
00:51:22,080 --> 00:51:26,260
this could become a part of every day.
743
00:51:26,260 --> 00:51:30,590
In fact, it will become central to
it because it will be the foundation
744
00:51:30,860 --> 00:51:35,680
that the rest of the program sits
on, especially if this future comes
745
00:51:35,680 --> 00:51:41,210
true where the computer is doing a
lot of the writing of the software.
746
00:51:41,660 --> 00:51:48,220
And, uh, yeah, no, so thank you very much
for sharing with, uh, with everybody,
747
00:51:48,430 --> 00:51:53,590
uh, the story of, um, of verifying the
Rust standard library, as well as, uh,
748
00:51:53,590 --> 00:51:57,170
something which I was very unexpected
to me, this idea of essentially, um,
749
00:51:57,360 --> 00:52:01,780
creating this secure foundation for a
new paradigm of software development.
750
00:52:01,890 --> 00:52:05,510
And, um, in 20 years, we might
have another conversation and
751
00:52:05,510 --> 00:52:07,450
find out, um, whether or not.
752
00:52:07,950 --> 00:52:10,030
It happened or like what
it actually looks like.
753
00:52:10,030 --> 00:52:12,890
So I, uh, I wish you all the best.
754
00:52:14,284 --> 00:52:14,574
Thank you.
755
00:52:14,824 --> 00:52:15,754
Thank you very much.
756
00:52:15,814 --> 00:52:18,514
And, uh, I hope it's sooner than 20 years.
757
00:52:18,790 --> 00:52:19,140
Yeah.
758
00:52:19,190 --> 00:52:19,460
Yeah.
759
00:52:20,770 --> 00:52:21,060
Right.
760
00:52:21,290 --> 00:52:21,500
Right.
761
00:52:21,530 --> 00:52:21,960
Okay.
762
00:52:23,580 --> 00:52:24,590
People can take their bets.
763
00:52:27,026 --> 00:52:31,356
You've been listening to Compose, a
podcast for software developers interested
764
00:52:31,356 --> 00:52:32,736
in the Rust programming language.
765
00:52:33,766 --> 00:52:37,826
My name is Tim McNamara, also known
as timclicks, and you can find
766
00:52:37,836 --> 00:52:40,726
further resources at timclicks.
767
00:52:40,726 --> 00:52:40,896
dev.
768
00:52:42,016 --> 00:52:42,906
At timclicks.
769
00:52:42,946 --> 00:52:48,666
dev you'll find tutorials, videos and
articles all geared around helping you
770
00:52:48,666 --> 00:52:52,236
to get better at the Rust programming
language to build a better planet.
771
00:52:53,876 --> 00:52:57,746
If you've enjoyed this episode,
then here's a suggestion.
772
00:52:58,766 --> 00:53:03,036
Try to apply formal verification
to one of your projects today.
773
00:53:03,866 --> 00:53:05,386
Check the show notes for resources
774
00:53:06,536 --> 00:53:11,436
Check the show notes for links to
resources for you to get started.
775
00:53:13,386 --> 00:53:14,026
Take care.
776
00:53:14,136 --> 00:53:14,726
Have fun.
777
00:53:14,726 --> 00:53:16,206
I'll see you on the next episode.
00:00:00,049 --> 00:00:07,749
So my name is Rahul Kumar and I'm a
Senior Applied Science Manager at AWS.
2
00:00:08,369 --> 00:00:15,695
I lead a team that works on Rust
verification, C code verification, And,
3
00:00:15,695 --> 00:00:23,494
uh, we are very, very passionate about
bringing formal methods into, uh, the
4
00:00:23,494 --> 00:00:28,035
mainstream, especially for Rust, which
is what this work is about and what
5
00:00:28,075 --> 00:00:29,374
I'm going to talk about a bit more.
6
00:00:30,174 --> 00:00:34,864
Uh, previously, I worked at
Microsoft, Microsoft Research.
7
00:00:35,635 --> 00:00:42,145
I worked on decode verification
um, a little bit of empirical
8
00:00:42,145 --> 00:00:44,045
software engineering techniques.
9
00:00:45,035 --> 00:00:49,494
And then, uh, before that, I also worked
on the Europa Clipper mission at NASA JPL.
10
00:00:50,304 --> 00:00:51,785
So, very exciting.
11
00:01:15,037 --> 00:01:18,687
The first question to ask, I suppose,
is , what is formal verification?
12
00:01:18,697 --> 00:01:23,667
But can I actually intercept myself
by asking something else, which is , I
13
00:01:23,697 --> 00:01:29,327
thought Rust was a safe programming
language and you made a special
14
00:01:29,327 --> 00:01:33,987
note to say, that you are especially
interested in verifying Rust.
15
00:01:34,037 --> 00:01:40,607
And so, can you describe to me, like,
what the dist, like, how Rust is sort
16
00:01:40,607 --> 00:01:42,437
of, like, uh, is Rust lying to us?
17
00:01:42,467 --> 00:01:45,687
Like, what's, what ne, what are, what
are the holes that need to be filled?
18
00:01:47,216 --> 00:01:52,716
Yeah, so, uh, very first I'm going to
say, no, there's no lies here, right?
19
00:01:53,526 --> 00:01:54,856
That would be a bit aggressive.
20
00:01:55,967 --> 00:01:56,517
Okay, sure.
21
00:01:56,546 --> 00:02:02,901
an amazing programming language,
which provides Fantastic, fantastic
22
00:02:03,141 --> 00:02:06,811
compile time guarantees that most
other languages will not provide you.
23
00:02:07,541 --> 00:02:12,261
Rust does have an escape path
to perform certain functions.
24
00:02:12,746 --> 00:02:15,576
And, uh, that's called
the unsafe part of Rust.
25
00:02:15,836 --> 00:02:22,186
It provides you so called superpowers to,
achieve what you're looking to, to do.
26
00:02:23,026 --> 00:02:26,646
there are various reasons why
one may choose to adopt those.
27
00:02:26,956 --> 00:02:29,186
So, number one, no lies.
28
00:02:29,186 --> 00:02:29,931
Number two, no lies.
29
00:02:30,281 --> 00:02:34,221
Yes, we have an escape path, and
at that point the compiler will
30
00:02:34,231 --> 00:02:38,221
stop giving you guarantees that it
traditionally would in SafeRust.
31
00:02:39,011 --> 00:02:40,861
Now, does that mean?
32
00:02:41,531 --> 00:02:47,171
That basically means that the compiler
is expecting some sort of human
33
00:02:47,231 --> 00:02:54,231
assist, or potentially AI assist
in the future, to, to enable you to
34
00:02:54,241 --> 00:02:55,781
give the guarantees for yourself.
35
00:02:57,272 --> 00:03:02,592
So I would normally describe this as
the burden of proof kind of shifts from
36
00:03:02,592 --> 00:03:04,722
the compiler to you as the programmer.
37
00:03:04,892 --> 00:03:08,732
Do you kind of, how does
that sentence fit with you?
38
00:03:09,841 --> 00:03:11,701
That's, that's a wonderful way to say it.
39
00:03:11,761 --> 00:03:15,001
And you use an interesting
word in there called proof,
40
00:03:15,452 --> 00:03:15,842
Uh huh.
41
00:03:16,821 --> 00:03:21,561
Because the compiler is actually in
the safe world, giving you proof that
42
00:03:21,561 --> 00:03:26,691
you're okay, but in the unsafe world,
it is not giving you that proof.
43
00:03:27,661 --> 00:03:32,341
while you may run this particular piece
of code a million times and never have
44
00:03:32,341 --> 00:03:37,101
an issue, have a guarantee, which is
what the proof will give you at the end.
45
00:03:37,431 --> 00:03:40,371
And yes, the burden of
proof is on the programmer.
46
00:03:41,402 --> 00:03:41,702
Right.
47
00:03:41,702 --> 00:03:46,142
I, I need to kind of, uh, I
did an undergraduate degree
48
00:03:46,142 --> 00:03:47,232
in philosophy actually.
49
00:03:47,272 --> 00:03:55,112
Um, and just kind of like, this is sort of
bringing up like old neurons are activated
50
00:03:55,192 --> 00:03:59,957
about like, Inductive and versus deductive
logic and the fact that essentially
51
00:04:00,277 --> 00:04:03,007
it doesn't matter how many times it's
right if we if you can't guarantee
52
00:04:03,007 --> 00:04:05,417
that Uh that it might never be wrong.
53
00:04:05,467 --> 00:04:13,127
You you still never have um that
kind of quality and uh, I sure yeah.
54
00:04:13,127 --> 00:04:13,317
Yeah.
55
00:04:13,317 --> 00:04:14,137
No, absolutely.
56
00:04:14,167 --> 00:04:18,067
So the And just, because there
are a couple of people who are
57
00:04:18,127 --> 00:04:20,117
terrified of this keyword, unsafe.
58
00:04:20,511 --> 00:04:23,901
will.
59
00:04:24,167 --> 00:04:27,987
is why we might use this escape hatch.
60
00:04:27,997 --> 00:04:32,107
And sometimes it's impossible to
avoid, such as if I want to talk
61
00:04:32,107 --> 00:04:38,467
to the operating system, or I need
to talk to some, uh, other library.
62
00:04:38,977 --> 00:04:44,787
That might be written in different
programming language, uh, and it's
63
00:04:44,787 --> 00:04:47,927
impossible for the Rust compiler to
guarantee, make some, any, some sort of
64
00:04:47,927 --> 00:04:52,957
assertion or guarantee about programs that
other, that live somewhere else, that,
65
00:04:53,197 --> 00:04:57,147
that those are, that's one case where
it might be impossible to avoid unsafe.
66
00:04:58,821 --> 00:05:04,551
Yeah, uh, uh, you know, you want to,
you want to use some foreign, uh,
67
00:05:04,561 --> 00:05:10,181
language interface or you want to
dereference raw pointers, uh, the,
68
00:05:10,211 --> 00:05:15,761
the so called five superpowers that
Rust has in, in all of those cases.
69
00:05:16,576 --> 00:05:23,216
Either you are functionally bound and
you want to, to achieve a, a particular
70
00:05:23,246 --> 00:05:27,696
function at the end, or a functionality
at the end, which you're, you're
71
00:05:27,776 --> 00:05:29,866
not able to do because of SafeRUS.
72
00:05:30,126 --> 00:05:35,446
Great, that's a perfectly valid
reason to do this, or maybe there is a
73
00:05:35,466 --> 00:05:40,636
performance concern because the SafeRUS
could potentially introduce checks that
74
00:05:40,666 --> 00:05:45,146
you are not very interested in having.
75
00:05:45,451 --> 00:05:47,481
And it causes a performance slowdown.
76
00:05:48,971 --> 00:05:50,961
again, back
77
00:05:50,997 --> 00:05:51,087
so.
78
00:05:52,737 --> 00:05:59,217
At this point, it's this temptation
of, well, I could go faster.
79
00:05:59,517 --> 00:06:04,917
Like I essentially, uh, I know that
there are, I know like in sort of scare
80
00:06:04,917 --> 00:06:07,897
quotes there, because I might be wrong.
81
00:06:07,927 --> 00:06:11,117
Like it turns out that humans are
often wrong about these things, but you
82
00:06:11,117 --> 00:06:15,677
know, for as far as I can see as the
programmer, uh, I am upholding invariance
83
00:06:15,717 --> 00:06:17,497
around memory safety and so forth.
84
00:06:18,227 --> 00:06:22,647
And so I could, uh, essentially
skip safety checks that the.
85
00:06:23,047 --> 00:06:27,917
Compiler would otherwise kind of
inject and yeah, and then suddenly
86
00:06:27,917 --> 00:06:31,677
I'd get like a, let's say, I don't
know, a two or 3 percent speed
87
00:06:31,677 --> 00:06:34,827
up in code that might be, yeah.
88
00:06:34,917 --> 00:06:35,217
Okay.
89
00:06:35,337 --> 00:06:35,727
Interesting.
90
00:06:36,461 --> 00:06:44,101
Yeah, so imagine, uh, developer, uh, X,
uh, tasked by their manager to take a
91
00:06:44,121 --> 00:06:50,641
piece of C code and manager says, you
know, I want you to go make this in Rust
92
00:06:50,651 --> 00:06:52,521
because I've heard it's safe and faster.
93
00:06:53,311 --> 00:06:58,326
And, uh, And developer X goes and
rewrites it in Rust, in SafeRust,
94
00:06:58,336 --> 00:07:03,326
and turns out it's actually the same
performance as the C code, because there's
95
00:07:03,326 --> 00:07:05,556
a bunch of safety injections in there.
96
00:07:06,756 --> 00:07:11,646
then they experiment and go into
unsafe mode, and turns out it's
97
00:07:11,646 --> 00:07:16,856
actually a lot faster, but now we
don't have a proof of correctness,
98
00:07:16,876 --> 00:07:18,986
which the SafeRust would have provided.
99
00:07:19,947 --> 00:07:20,337
Okay.
100
00:07:21,076 --> 00:07:26,466
at that point, Yes, the burden of
proof is on the developer and that's
101
00:07:26,466 --> 00:07:30,576
a simple motivational example that
this has happened in real life.
102
00:07:30,606 --> 00:07:32,306
We have seen examples of this.
103
00:07:33,306 --> 00:07:42,236
Um, unsafe for us tends to have a very,
very useful function and support it.
104
00:07:43,216 --> 00:07:50,366
The, the place that we are coming from
is Even if it's unsafe, why don't we
105
00:07:50,366 --> 00:07:54,666
go provide you those assurances that
would not have been possible before?
106
00:07:55,626 --> 00:08:03,736
And that's amazing because, uh, now you
can probably go into unsafe and achieve
107
00:08:03,736 --> 00:08:10,076
the functions that you want to achieve
still have guarantees for the future.
108
00:08:11,402 --> 00:08:14,412
So, and this is verification.
109
00:08:14,642 --> 00:08:19,082
So I expect that the term formal
verification has, has a very
110
00:08:19,082 --> 00:08:22,502
precise technical meaning, do
you want to, is that correct?
111
00:08:22,502 --> 00:08:24,092
And if so, do you want to flesh that out?
112
00:08:24,926 --> 00:08:28,016
mathema yes, uh, we want
to use mathematical logic.
113
00:08:28,646 --> 00:08:37,896
Uh, to prove properties about your
programs and, and formal verification, in
114
00:08:37,896 --> 00:08:43,296
a sense, you know, you could say, well,
I want to go verify a model of something.
115
00:08:43,306 --> 00:08:47,686
That's fine as well, but the, the
artifact that you are dealing with,
116
00:08:47,706 --> 00:08:51,176
which you are most interested in
will exhibit certain properties,
117
00:08:51,206 --> 00:08:56,296
and we want to go prove properties
about that, about that artifact, and
118
00:08:56,296 --> 00:09:03,426
we want to prove them Exclusively,
unboundedly, impermanence, if you will.
119
00:09:04,626 --> 00:09:09,286
I suppose one of the things that was
fascinating to me about one of the tools
120
00:09:09,286 --> 00:09:13,816
that hopefully we'll get to chat about
called Kani was that it's all symbolic.
121
00:09:13,846 --> 00:09:17,946
The actual code itself doesn't really
get executed and kind of get, as far as
122
00:09:17,946 --> 00:09:26,346
I can tell, gets translated and then run
through an SAT solver and then, uh, yeah.
123
00:09:26,346 --> 00:09:30,316
And so it's, it's, it's almost as though.
124
00:09:30,921 --> 00:09:38,041
You're operating with software, not as a
set of instructions for a computer to kind
125
00:09:38,041 --> 00:09:41,521
of go from top to bottom through, like
you might think of it scanning through
126
00:09:41,521 --> 00:09:46,291
assembly, but as a series of symbolic
instructions, so much more sort of a high
127
00:09:46,291 --> 00:09:54,281
level, um, and just the structure of the
way that the program is operating allows,
128
00:09:54,281 --> 00:09:59,166
um, The solver or that was the tooling
to some, make some sort of inference or
129
00:09:59,166 --> 00:10:01,616
actually no deduction about correctness,
130
00:10:03,190 --> 00:10:08,430
Yeah, I think I think the word, uh, which
would be appropriate here is semantics.
131
00:10:08,676 --> 00:10:08,706
right?
132
00:10:09,400 --> 00:10:14,075
So semantics and, and
then specification, right?
133
00:10:14,365 --> 00:10:21,815
So, we, we take the, the input
and we process it according to
134
00:10:21,815 --> 00:10:23,775
the semantics that are defined.
135
00:10:24,585 --> 00:10:29,025
And interestingly enough, there are
situations with programming languages
136
00:10:29,805 --> 00:10:31,905
where semantics are undefined.
137
00:10:33,375 --> 00:10:35,955
And that's something that we
would like to also change.
138
00:10:36,450 --> 00:10:42,560
So attacking this core problem of let's
go verify the Rust standard library,
139
00:10:42,570 --> 00:10:44,250
let's go verify the core library.
140
00:10:44,490 --> 00:10:51,360
Well, we're, we're now in a place where
we're challenging a community to actually
141
00:10:51,370 --> 00:10:54,380
formally define the semantics, right?
142
00:10:54,830 --> 00:10:56,620
Uh, there's
143
00:10:56,691 --> 00:10:57,171
Right,
144
00:10:57,230 --> 00:10:58,030
this funny,
145
00:10:58,281 --> 00:11:03,971
so if, uh, hopefully an example will
pop into your head just immediately,
146
00:11:04,151 --> 00:11:08,131
but if essentially there's a gap in
the specification where it kind of
147
00:11:08,131 --> 00:11:12,421
provides wriggle room, which makes
it essentially impossible to verify
148
00:11:12,621 --> 00:11:14,711
because there's ambiguity there.
149
00:11:14,751 --> 00:11:16,981
Is that the problem that there is?
150
00:11:17,330 --> 00:11:21,190
and, and a funny party trick,
right, that, that used to be
151
00:11:21,220 --> 00:11:26,210
played, uh, in, in the math clubs
was, Oh, let me prove 1 equals 0.
152
00:11:26,851 --> 00:11:27,321
Mmm.
153
00:11:27,520 --> 00:11:34,695
the essential idea was that you're
dividing by x minus x, And you can go
154
00:11:34,695 --> 00:11:39,635
prove one equals zero to somebody who
doesn't realize that this particular
155
00:11:39,735 --> 00:11:41,935
semantics is not, is prohibited.
156
00:11:41,975 --> 00:11:42,885
It's not allowed.
157
00:11:44,135 --> 00:11:50,415
uh, uh, with the Russ or with a lot of
programming languages, in fact, maybe all,
158
00:11:50,415 --> 00:11:57,205
I'm not sure, uh, it is, it is true that
there are gaps in the defined semantics.
159
00:11:57,845 --> 00:11:59,705
And we would like to close out on that.
160
00:12:00,905 --> 00:12:06,975
Formal verification would I associate,
or at least I have been associating
161
00:12:06,975 --> 00:12:13,565
with things like TLA or, uh, There are
a couple of other modeling languages.
162
00:12:13,605 --> 00:12:17,105
Some are easier to use than others,
but typically they are difficult
163
00:12:17,475 --> 00:12:20,305
and very complex and challenging.
164
00:12:20,875 --> 00:12:32,585
Um, uh, Do you have any thoughts
on why these, uh, Uh, Why formal
165
00:12:32,585 --> 00:12:41,265
verification is so difficult for,
let's say most programmers, and that
166
00:12:41,275 --> 00:12:43,355
it seems like a very specialized topic.
167
00:12:44,555 --> 00:12:50,375
So, so I will give you that it
is specialized, uh, number one.
168
00:12:50,385 --> 00:12:54,465
Number two, I, I think that the
examples you cite are also interesting
169
00:12:54,465 --> 00:13:01,165
because they're not directly what
a software engineer would go write
170
00:13:01,185 --> 00:13:03,105
and deploy at the end of the day,
171
00:13:03,501 --> 00:13:04,321
Yeah, they're modeling.
172
00:13:04,341 --> 00:13:07,021
Well, at least LAPLUS is
definitely a, a, Click here.
173
00:13:07,021 --> 00:13:15,801
Mm hmm.
174
00:13:15,920 --> 00:13:22,130
Veris, uh, would fit into that domain
where we're actually trying to operate
175
00:13:22,240 --> 00:13:25,910
on the code that is being deployed.
176
00:13:26,670 --> 00:13:32,800
And one of the goals for us is to
make this as automated as possible.
177
00:13:33,545 --> 00:13:39,745
So, yes, do you, do you, would we
like you to specify properties?
178
00:13:40,445 --> 00:13:41,155
Absolutely.
179
00:13:42,085 --> 00:13:44,185
Right, because that's
something that you know about.
180
00:13:44,525 --> 00:13:45,415
You know your code.
181
00:13:46,185 --> 00:13:49,335
But do we want you to go create models?
182
00:13:49,585 --> 00:13:50,295
Probably not.
183
00:13:50,345 --> 00:13:52,605
We're, we're trying to do that for you.
184
00:13:53,315 --> 00:13:53,645
And we
185
00:13:54,275 --> 00:13:54,665
for you.
186
00:13:55,706 --> 00:13:59,476
And so it sounds like one of the barriers
has been, well, you need to, if you
187
00:13:59,476 --> 00:14:03,256
want to learn formal verification or at
least some subset of the domain, then
188
00:14:03,256 --> 00:14:08,606
you need to go learn a modeling language
and, uh, and create a specification.
189
00:14:08,826 --> 00:14:14,441
Whereas let's say newer tools or the
tools The Kani in particular, uh,
190
00:14:14,441 --> 00:14:20,711
essentially it's just Rust code and,
um, it's actually embedded in the
191
00:14:20,791 --> 00:14:22,241
code that you're actually running.
192
00:14:22,241 --> 00:14:23,571
It's not some separate artifact.
193
00:14:23,851 --> 00:14:29,861
And so, um, I mean, I personally,
when I've used Kani have really
194
00:14:29,861 --> 00:14:33,651
appreciated that, that essentially the
tooling kind of comes to me and that
195
00:14:33,651 --> 00:14:37,211
I don't need to go out to something
else and use a different workflow.
196
00:14:37,271 --> 00:14:40,061
I can just use Cargo,
for example, to drive it.
197
00:14:40,141 --> 00:14:40,801
Um, I think.
198
00:14:41,091 --> 00:14:41,661
Um,
199
00:14:42,421 --> 00:14:42,611
and,
200
00:14:43,811 --> 00:14:50,391
uh, the ergonomics of making this
real and scalable are so important.
201
00:14:50,711 --> 00:14:57,001
And, you know, uh, imagine being in a
meeting where you go from discussing
202
00:14:57,011 --> 00:15:03,811
highly symbolic execution oriented
algorithms, uh, and problems with them to,
203
00:15:04,031 --> 00:15:09,251
well, we think this should be Not start
with a star, it should be an ampersand.
204
00:15:09,681 --> 00:15:14,081
Um, and, and, you know,
both are amazingly valid.
205
00:15:14,871 --> 00:15:19,221
Because if you want to push formal
verification to the next frontier, make
206
00:15:19,221 --> 00:15:22,401
it part of the mainline, is what it takes.
207
00:15:22,741 --> 00:15:25,031
You have to work on both
ends of the spectrum.
208
00:15:26,651 --> 00:15:31,021
You can go make the best engine
in the world, you don't have a
209
00:15:31,021 --> 00:15:34,631
beautiful car on top of it, people
aren't really going to drive it.
210
00:15:36,182 --> 00:15:45,622
Yeah, I, I spend a lot of time picking at,
uh, syntax as well, even though it feels
211
00:15:46,152 --> 00:15:53,762
in some sense, meaningless or trivial or
somehow less important, but really nice.
212
00:15:54,082 --> 00:15:54,752
syntax.
213
00:15:54,862 --> 00:15:59,242
It kind of lends itself to
really nice programs in a way.
214
00:16:00,212 --> 00:16:05,982
And, uh, and, and so the struggle
is, is, is kind of real, I think,
215
00:16:05,992 --> 00:16:09,272
when you're designing a language
about, do we use curly braces?
216
00:16:09,272 --> 00:16:10,282
Do we use angle braces?
217
00:16:11,842 --> 00:16:21,542
But, um, the, uh, the idea here is
that we have a A tool, Kani in this
218
00:16:21,542 --> 00:16:30,682
case, which can take Rust code, uh,
reason about it symbolically, uh, and
219
00:16:30,712 --> 00:16:37,902
essentially make some sort of guarantee
or that the properties of correctness.
220
00:16:39,357 --> 00:16:46,367
Maintained through the use of
unsafe, uh, surely, but surely
221
00:16:46,367 --> 00:16:47,657
the project is not yet done.
222
00:16:48,157 --> 00:16:52,777
Are there kind of known limitations where,
I mean, presumably that there are, you,
223
00:16:52,937 --> 00:16:54,207
you know, where the gaps are, I hope.
224
00:16:55,407 --> 00:16:55,707
Right.
225
00:16:55,717 --> 00:16:58,697
So I have, I have, uh, two
or three things to say here.
226
00:16:58,887 --> 00:17:01,207
So number one, it's number one.
227
00:17:01,277 --> 00:17:07,377
Uh, yes, we do have limitations and we
publish them and, and believe me, we are
228
00:17:07,807 --> 00:17:15,567
absolutely 100 percent on the ball about
making sure we publish these because
229
00:17:15,967 --> 00:17:17,567
no false guarantee should be made.
230
00:17:18,847 --> 00:17:19,167
Right.
231
00:17:19,517 --> 00:17:25,057
Number two, uh, there is a distinction
between these generic properties
232
00:17:25,577 --> 00:17:28,347
versus user oriented properties
233
00:17:29,883 --> 00:17:30,363
Okay.
234
00:17:31,527 --> 00:17:36,302
right, and you can make Uh, you
can, you can go check for certain
235
00:17:36,312 --> 00:17:40,932
UBs which come right out of the box
with Connie because, hey, that just
236
00:17:40,932 --> 00:17:42,702
applies to everything in Rust, right?
237
00:17:43,122 --> 00:17:48,092
Uh, but then if you want to go
say, I'm very highly interested
238
00:17:48,352 --> 00:17:52,772
that this particular variable
never exceeds the value of 42.
239
00:17:53,972 --> 00:17:56,562
Okay, you can go write
that property and prove it.
240
00:17:57,277 --> 00:18:00,297
And, uh, there's a fascinating example.
241
00:18:00,307 --> 00:18:02,997
There's a repository out
there called HiFiTime.
242
00:18:02,997 --> 00:18:08,917
And there's a blog post on the
Connie blog about, uh, proving
243
00:18:08,917 --> 00:18:10,587
the correctness of HiFiTime.
244
00:18:11,157 --> 00:18:19,047
Uh, it's a, it's a time library for
the, the solar system, if you will,
245
00:18:19,167 --> 00:18:25,372
operating across multiple, And, uh,
Christopher Rabbitin, uh, who wrote the
246
00:18:25,372 --> 00:18:31,022
blog post with us or mostly by himself,
uh, but we reviewed it, which was nice.
247
00:18:31,382 --> 00:18:37,092
Uh, of the first external contributions
to the Connie blog, uh, picked
248
00:18:37,092 --> 00:18:43,762
up on Connie and used it to prove
correctness of, of so many functions.
249
00:18:44,827 --> 00:18:47,147
For the next 36, 000 years.
250
00:18:48,823 --> 00:18:49,293
Incredible.
251
00:18:50,297 --> 00:18:50,797
Right.
252
00:18:51,007 --> 00:18:55,167
And, and that's, those are such custom
properties that he's working with, right?
253
00:18:55,547 --> 00:18:57,077
Uh, amazing stuff.
254
00:18:57,377 --> 00:19:03,287
Uh, AWS Firecracker, which, uh, is
a VMM that is open source on GitHub.
255
00:19:03,287 --> 00:19:05,787
And, and we rely on that quite a bit.
256
00:19:06,167 --> 00:19:11,187
They have so many custom properties that
they prove about, about their code base.
257
00:19:11,507 --> 00:19:14,347
And, and how they deal
with certain issues.
258
00:19:15,162 --> 00:19:20,652
Those are fascinating, uh, user
oriented functional properties
259
00:19:20,652 --> 00:19:21,612
that people are proving.
260
00:19:22,912 --> 00:19:26,552
In addition to the generic UBs that they
261
00:19:26,593 --> 00:19:26,953
Sure.
262
00:19:27,373 --> 00:19:31,323
So can I, just as a hypothetical,
I'm not sure, like, I literally
263
00:19:31,323 --> 00:19:32,253
don't know if this is possible.
264
00:19:33,413 --> 00:19:37,673
It would be wonderful to have a per,
uh, let's say a percentage type,
265
00:19:37,703 --> 00:19:40,613
which is encoded as floating point,
although maybe it should be irrational
266
00:19:40,883 --> 00:19:43,283
using a, a, um, an instrument.
267
00:19:43,283 --> 00:19:44,183
But let's say it's not.
268
00:19:44,633 --> 00:19:50,513
And so I'm using floating and I want to
guarantee that the use of my percentage
269
00:19:50,543 --> 00:19:52,553
is always between zero and one.
270
00:19:52,703 --> 00:19:57,443
So essentially, um, it's bounded
with inside those, um, with, uh,
271
00:19:57,743 --> 00:19:59,423
is that something that I can ask?
272
00:19:59,663 --> 00:20:03,293
Kani to chick so that I
should never be able to have.
273
00:20:03,412 --> 00:20:04,462
the box.
274
00:20:05,702 --> 00:20:10,032
But you can by encoding
a custom property, yes.
275
00:20:10,643 --> 00:20:11,043
Wow.
276
00:20:11,182 --> 00:20:13,472
give you the ability to, ability to, yeah.
277
00:20:14,863 --> 00:20:15,103
Yeah.
278
00:20:15,103 --> 00:20:21,193
I, um, I've always kind of been
in, uh, there's a part of Ada,
279
00:20:21,193 --> 00:20:25,723
which I have always been fascinated
by, which whereby you can have.
280
00:20:26,153 --> 00:20:31,573
Types which are constrained by their
ranges rather than being, rather
281
00:20:31,573 --> 00:20:34,643
than having all integers available to
you, you've just got some subset and,
282
00:20:34,743 --> 00:20:40,903
um, I've always wondered how that is
implemented because the representation
283
00:20:40,903 --> 00:20:45,633
in memory is presumably just an
integer, or for example, and, um,
284
00:20:45,862 --> 00:20:48,782
so you bring up specifically
floating points, which I think we
285
00:20:48,782 --> 00:20:52,822
have a bug on, but I'm not sure.
286
00:20:53,102 --> 00:20:54,382
Let me be clear about that.
287
00:20:54,412 --> 00:20:56,412
And we claim that in our list,
288
00:20:57,813 --> 00:21:01,153
Floating point is much harder than
integers, which is why I brought it up.
289
00:21:01,223 --> 00:21:01,413
Oh yeah,
290
00:21:01,832 --> 00:21:03,022
that's kind of where I was going.
291
00:21:03,022 --> 00:21:03,302
Right?
292
00:21:03,302 --> 00:21:04,522
So if you're sticking to integers,
you're sticking to integers.
293
00:21:04,672 --> 00:21:06,922
Yes, you can restrict
it, uh, floating points.
294
00:21:06,922 --> 00:21:11,712
I believe we are, we're trying to,
there's certain SIMD instructions where
295
00:21:11,932 --> 00:21:14,292
we're, we're have like a small issue.
296
00:21:14,642 --> 00:21:19,262
Um, modulo becomes interesting, you know,
297
00:21:20,052 --> 00:21:21,072
uh, incomplete.
298
00:21:21,072 --> 00:21:21,522
So,
299
00:21:22,433 --> 00:21:26,423
Look, I think, look, the fact that
these are the goals that you're striving
300
00:21:26,423 --> 00:21:34,823
for, and I know, I mean, it's sort
of incredible and, uh, I wonder how
301
00:21:34,823 --> 00:21:40,288
that would translate Through unsafe,
like we've got, you've mentioned
302
00:21:40,288 --> 00:21:44,488
UBs are like a general thing, class
of problems that we wish to avoid.
303
00:21:44,488 --> 00:21:50,028
So we want to remove the possibility
of unsafe or sorry, undefined behavior.
304
00:21:50,648 --> 00:21:55,488
Um, I suppose this would be classified
at build time or at test time.
305
00:21:55,868 --> 00:21:57,608
Um, and.
306
00:21:58,748 --> 00:22:06,828
One question, Mark, that I, uh, that's
kind of lingering around is how Kani
307
00:22:06,848 --> 00:22:10,718
differs from other tools in its space
that are achieving similar things, such
308
00:22:10,718 --> 00:22:14,078
as like the Mirri, uh, is an interpreter.
309
00:22:14,078 --> 00:22:16,878
So this operates in a significant,
its model of operation is
310
00:22:17,318 --> 00:22:18,188
much different, isn't it?
311
00:22:19,712 --> 00:22:22,062
yes, yes, this is a great question.
312
00:22:22,062 --> 00:22:24,912
So, you know, there's a,
there's a spectrum of tools.
313
00:22:25,492 --> 00:22:31,502
And, and each one, and every single
tool comes with its benefits.
314
00:22:31,927 --> 00:22:32,397
Right.
315
00:22:32,827 --> 00:22:39,197
Uh, uh, you, you can start with,
with basic dynamic execution.
316
00:22:39,997 --> 00:22:43,617
Uh, you can go to testing, you
can go to fuzz testing, you can
317
00:22:43,617 --> 00:22:47,107
go into model checking, which
is where Connie fits, right?
318
00:22:47,137 --> 00:22:53,417
Then you go into deductive logic based
tools and higher order logic based tools.
319
00:22:53,687 --> 00:23:01,437
Uh, spectrum is, is, is very important
because, The effort that we have,
320
00:23:01,477 --> 00:23:04,177
you know, coming back to the Rust
standard library verification
321
00:23:04,177 --> 00:23:07,217
effort, it's not about Connie.
322
00:23:08,417 --> 00:23:17,087
It's about ensuring that we can
use this spectrum of tools to go
323
00:23:17,097 --> 00:23:18,787
give guarantees for the future.
324
00:23:19,987 --> 00:23:25,607
An effort, like at a very basic level,
an effort is a collection of people
325
00:23:25,837 --> 00:23:28,947
who are trying to achieve a goal.
326
00:23:29,217 --> 00:23:32,537
And one of the first things they
do is create a demonstration
327
00:23:32,547 --> 00:23:35,337
that, hey, I can go do something.
328
00:23:36,837 --> 00:23:41,922
And what we have done thus
far is given a demonstration.
329
00:23:43,362 --> 00:23:49,222
And the hope is, the idea is that more
and more people join this effort and bring
330
00:23:49,222 --> 00:23:51,662
in their specialties and their tools.
331
00:23:52,862 --> 00:23:54,722
That's extremely exciting.
332
00:23:54,732 --> 00:23:58,592
Do you think that the, although
I'm just going to wait for my
333
00:23:58,592 --> 00:24:00,702
dog to decide to stop barking.
334
00:24:01,091 --> 00:24:01,371
Sure.
335
00:24:02,571 --> 00:24:04,901
I think someone just came
home, which makes us excited.
336
00:24:05,471 --> 00:24:06,701
The, um,
337
00:24:07,901 --> 00:24:09,421
here's a question for you.
338
00:24:09,691 --> 00:24:12,641
Do you think there are a large
number of tools that are sitting
339
00:24:12,811 --> 00:24:16,831
in the darkness waiting to kind
of be revealed to the world?
340
00:24:18,031 --> 00:24:25,181
I don't know if sitting in the darkness is
a phrase I would use, but there are, there
341
00:24:25,211 --> 00:24:28,201
are a lot of tools that, that can be used.
342
00:24:28,201 --> 00:24:28,711
Yeah.
343
00:24:29,041 --> 00:24:34,481
Look at tools like, uh, Cruzeau,
I I Nia is a great example.
344
00:24:34,981 --> 00:24:36,881
I think that's a wonderful tool.
345
00:24:37,071 --> 00:24:39,511
We are borrowing concepts from ideas.
346
00:24:39,841 --> 00:24:41,721
Uh, Veris is a great example.
347
00:24:42,401 --> 00:24:48,021
You know, Connie, of course, since
we happen to be closely related to
348
00:24:48,031 --> 00:24:52,951
Connie, that's how we wanted to make
the demonstration and jumpstart.
349
00:24:54,221 --> 00:24:54,711
That's it,
350
00:24:55,882 --> 00:24:58,772
So let's talk about this,
this kind of project.
351
00:24:59,972 --> 00:25:07,622
We started chatting before, uh, uh,
on LinkedIn because I posted a note
352
00:25:07,742 --> 00:25:16,442
about something that I read, uh, that
came as a joint effort from the Rust
353
00:25:16,442 --> 00:25:21,212
Foundation and AWS, and your name was
attached, at least on the AWS side.
354
00:25:21,582 --> 00:25:25,602
So, uh, what is it that
you're trying to do?
355
00:25:26,802 --> 00:25:35,302
Very simply put, we want to deliver
the new era of programming language.
356
00:25:36,942 --> 00:25:42,322
So, you know, we live in a world
where AI has already proven to be
357
00:25:42,322 --> 00:25:44,402
very useful for certain aspects.
358
00:25:45,592 --> 00:25:52,057
Um, Uh, I don't know how much you use
it per se, but you know, there's people
359
00:25:52,057 --> 00:25:56,097
summarizing things, there's people
rewriting things, there's people now
360
00:25:56,097 --> 00:25:59,217
starting to make 20 second videos, uh,
361
00:25:59,678 --> 00:26:07,978
Yeah, look, I, I, I actually am,
uh, Increasingly surprised at how
362
00:26:08,028 --> 00:26:09,638
effective it is at getting me.
363
00:26:09,668 --> 00:26:13,758
I think when chat GPT first came out, it
was like really good at getting me like
364
00:26:13,758 --> 00:26:17,398
a first draft for some sort of piece
of content that I wanted to produce.
365
00:26:17,398 --> 00:26:22,368
And now that, um, and now the models
and also the tooling around the models
366
00:26:22,368 --> 00:26:27,388
and some, uh, and, and the increasing
capabilities around rag, which is,
367
00:26:27,428 --> 00:26:30,548
um, I can't actually remember what it
expands out to, but the ability that you
368
00:26:30,548 --> 00:26:35,258
could actually teach models about your
custom, your own content means that.
369
00:26:36,353 --> 00:26:38,693
It's getting better and better at
source code and relatively complex.
370
00:26:40,013 --> 00:26:41,483
The context windows are increasing.
371
00:26:41,483 --> 00:26:42,163
La la la la la.
372
00:26:42,523 --> 00:26:51,873
So, uh, I am, uh, I would say I am
one of the people that are, that
373
00:26:51,883 --> 00:26:58,673
have high expectations for, for, um,
for AI and its ability to remove a
374
00:26:58,673 --> 00:27:03,673
lot of tedium from the process of
programming and a lot of mistakes.
375
00:27:03,753 --> 00:27:10,128
Uh, I think that, uh, It is, um,
but I'm also relatively skeptical.
376
00:27:10,138 --> 00:27:14,708
Like I'd rather be late and allow
other people to feel the pain.
377
00:27:16,447 --> 00:27:17,317
Yeah, absolutely.
378
00:27:17,647 --> 00:27:23,267
And, and, you know, I'm gonna tie
AI back to a previous comment or
379
00:27:23,267 --> 00:27:24,612
discussion actually, that we had.
380
00:27:25,342 --> 00:27:29,342
You, you can go test something a million
times and just because it doesn't fail
381
00:27:29,342 --> 00:27:35,062
doesn't mean it won't fail, uh, and AI,
we all know we've actually experienced
382
00:27:35,062 --> 00:27:40,512
the hallucinations to, to some degree
where, uh, you're like, well, that's
383
00:27:40,512 --> 00:27:41,922
not exactly what I was looking for.
384
00:27:42,162 --> 00:27:49,062
Now, AI is also, AI is also beneficial
in accelerating us unprecedented levels.
385
00:27:49,777 --> 00:27:55,167
Uh, when it comes to development
of products and services and
386
00:27:55,167 --> 00:27:58,697
code, do I, do I not want that?
387
00:27:58,737 --> 00:28:00,547
Of course, of course I want that.
388
00:28:00,987 --> 00:28:04,017
But do I want appropriate
guardrails around it?
389
00:28:04,407 --> 00:28:10,167
Which help me develop confidence
that, yes, I know that this
390
00:28:10,207 --> 00:28:11,387
AI gave me the right thing.
391
00:28:11,817 --> 00:28:14,007
And that's where formal
verification comes in.
392
00:28:14,437 --> 00:28:16,737
That's where this effort comes in.
393
00:28:17,027 --> 00:28:19,697
Because formal verification is the answer.
394
00:28:20,372 --> 00:28:21,892
for producing those guardrails.
395
00:28:22,853 --> 00:28:23,273
Right.
396
00:28:23,313 --> 00:28:24,333
So, okay.
397
00:28:24,453 --> 00:28:31,213
So now you have told a model, please
generate a piece of code or, you
398
00:28:31,213 --> 00:28:34,913
know, like fix this feature or fix
this bug in, but, but you also need.
399
00:28:35,688 --> 00:28:39,238
But it kind of gets constrained by
the fact that the tests must pass.
400
00:28:39,278 --> 00:28:42,208
And by the way, the tests
are not just tests anymore.
401
00:28:42,418 --> 00:28:44,818
They're formal verifications
of correctness.
402
00:28:45,118 --> 00:28:45,628
Um,
403
00:28:47,067 --> 00:28:47,427
yeah.
404
00:28:48,217 --> 00:28:52,757
And that's a very strong statement
because Um, say you want to go update
405
00:28:52,757 --> 00:28:55,817
your library and it has dependencies.
406
00:28:56,807 --> 00:28:58,257
The AI says, sure, no problem.
407
00:28:59,157 --> 00:28:59,587
Here you go.
408
00:28:59,647 --> 00:29:00,677
Here's a bunch of tokens.
409
00:29:01,047 --> 00:29:02,307
I'm just going to go spit them at you.
410
00:29:02,498 --> 00:29:03,538
I'm right.
411
00:29:04,738 --> 00:29:05,318
I love tokens.
412
00:29:05,318 --> 00:29:06,848
Here's, here's a thousand.
413
00:29:07,827 --> 00:29:12,387
And then here's Rahul sitting on his
computer going, uh, should I commit this?
414
00:29:12,397 --> 00:29:13,897
Should I approve this for request?
415
00:29:13,927 --> 00:29:15,667
I'm not sure what's going to happen here.
416
00:29:16,377 --> 00:29:20,477
But then, uh, the formal verification
tool kicks in and says, Hey, guess what?
417
00:29:20,497 --> 00:29:23,097
We've just proved that this is great.
418
00:29:23,207 --> 00:29:23,377
It.
419
00:29:23,682 --> 00:29:24,242
Works.
420
00:29:24,492 --> 00:29:26,442
It's equivalent to what you had before.
421
00:29:27,142 --> 00:29:27,432
for it.
422
00:29:28,323 --> 00:29:29,093
Hmm.
423
00:29:29,823 --> 00:29:30,193
Yeah.
424
00:29:30,213 --> 00:29:35,963
I, uh, and now essentially, well, yeah,
that that's just a huge new paradigm
425
00:29:36,353 --> 00:29:41,413
of writing software that, uh, you kind
of have like this human augmentation.
426
00:29:41,693 --> 00:29:47,933
Um, and I think that will are immensely
powerful, particularly at big, big,
427
00:29:47,943 --> 00:29:54,023
big places where you have lots of hulky
projects that there's never enough.
428
00:29:54,083 --> 00:29:57,183
It's really, I know that people say
that we have these trillion dollar
429
00:29:57,183 --> 00:30:02,303
companies, but being someone who's
worked inside one of them, no one ever
430
00:30:02,303 --> 00:30:04,383
has budget for like massive rewrites.
431
00:30:04,743 --> 00:30:11,053
And so I think this will
liberate a lot of, uh, of people.
432
00:30:12,688 --> 00:30:18,588
Yeah, one of the things I really
appreciate about Rust is that
433
00:30:19,218 --> 00:30:25,008
you can feel, is the notion
of this fearless concurrency.
434
00:30:26,498 --> 00:30:30,858
That was the first, pretty much
the first slogan that people really
435
00:30:30,878 --> 00:30:35,108
understood when Rust came, like
first came out like 2012, 2013.
436
00:30:35,688 --> 00:30:41,678
Fearless concurrency was one, and uh,
and the other one would be blazing fast.
437
00:30:41,678 --> 00:30:41,728
Rust.
438
00:30:42,078 --> 00:30:44,418
Those were the two
things that really stuck.
439
00:30:46,218 --> 00:30:49,848
And now it sounds like what
you're saying is the future.
440
00:30:49,848 --> 00:30:53,748
If we, if, if we get it right, like
it's not, it is literally a future
441
00:30:53,748 --> 00:30:57,928
that is not, there's lots of things
that might go wrong, but in principle,
442
00:30:58,658 --> 00:31:00,458
the tooling should get sufficient.
443
00:31:00,548 --> 00:31:06,608
Such that, that feeling of, uh, being
fearless, essentially knowing that
444
00:31:06,608 --> 00:31:13,128
you can't crash, uh uh, you can't.
445
00:31:14,723 --> 00:31:18,843
Your programs will carry on
because they'll be correct.
446
00:31:18,953 --> 00:31:20,513
You actually know that.
447
00:31:20,693 --> 00:31:24,833
That would be an immensely liberating
feeling, um, for people that
448
00:31:24,953 --> 00:31:27,863
are building, which is amazing.
449
00:31:28,967 --> 00:31:29,387
Yes.
450
00:31:29,627 --> 00:31:31,817
And you know, I, I'll
451
00:31:32,567 --> 00:31:37,497
a few decades, uh, which some people
may or may not relate to, but the
452
00:31:37,497 --> 00:31:42,757
amount of times we had to reboot a
computer, uh, and, and the, and the
453
00:31:42,757 --> 00:31:47,917
wastage that that produced, imagine
if you never have to deal with that.
454
00:31:49,117 --> 00:31:50,562
is almost perfect.
455
00:31:50,962 --> 00:31:55,952
But yeah, no, no, and there
are some very strange things.
456
00:31:55,952 --> 00:32:01,962
I mean, if people who, people who
didn't grow up or didn't experience
457
00:32:01,962 --> 00:32:03,622
the dial up era of the internet.
458
00:32:04,882 --> 00:32:06,112
Well, never really.
459
00:32:07,312 --> 00:32:12,892
Once upon a time, you needed to literally
plug the modem into the wall, like
460
00:32:12,962 --> 00:32:18,942
unplug the phone because you could either
have a phone or the computer would be
461
00:32:18,942 --> 00:32:21,112
talking on the internet and you'd pay,
462
00:32:21,386 --> 00:32:22,456
get a second line.
463
00:32:22,722 --> 00:32:23,422
right, right.
464
00:32:24,622 --> 00:32:26,772
And, and, and things like email.
465
00:32:27,962 --> 00:32:33,812
It felt different because you on, on
Outlook or like Thunderbird or whatever,
466
00:32:34,672 --> 00:32:40,252
there was a button like send and receive
because literally you need to phone in and
467
00:32:40,262 --> 00:32:42,982
download things from messages that come
in from the server and like re upload.
468
00:32:43,242 --> 00:32:44,477
Now we think of.
469
00:32:44,777 --> 00:32:47,037
Email is essentially instant messaging.
470
00:32:47,127 --> 00:32:48,447
We're always connected.
471
00:32:48,887 --> 00:32:52,397
The protocol actually expects that
everything is asynchronous and so forth.
472
00:32:52,397 --> 00:32:58,217
It still operates in an era where the
whole, uh, everything is disconnected
473
00:32:58,397 --> 00:33:04,412
and flaky, but messaging, is different.
474
00:33:04,432 --> 00:33:05,822
The internet feels different.
475
00:33:05,822 --> 00:33:06,872
It's essentially,
476
00:33:07,156 --> 00:33:15,411
and imagine the future computer
scientist, which uses AI to but guarantees
477
00:33:15,411 --> 00:33:17,131
the work with formal verification.
478
00:33:18,381 --> 00:33:22,981
Like, you know, uh, you and
I probably sat down in IDEs
479
00:33:22,981 --> 00:33:25,741
and wrote code and debug code.
480
00:33:27,211 --> 00:33:30,441
That's going to be an
extinct, antiquated activity.
481
00:33:31,641 --> 00:33:34,071
It's like, at some point people
are going to be like, Grandpa,
482
00:33:34,071 --> 00:33:36,231
so you used to have an IDE?
483
00:33:37,592 --> 00:33:37,992
yeah.
484
00:33:38,002 --> 00:33:42,222
Well, I think, I think of this, like
my immediate, my, and it's interesting,
485
00:33:42,222 --> 00:33:46,632
I'm just kind of thinking about
my own response to your comment.
486
00:33:47,212 --> 00:33:49,842
My immediate was like, it's kind of
this, you know, this kind of back
487
00:33:49,842 --> 00:33:55,352
and it's like, no way, Rahul, you,
you, this is, this is nonsense.
488
00:33:55,892 --> 00:33:57,632
And then it's like, what, pause?
489
00:33:58,622 --> 00:34:05,987
I think the same way about, uh,
Financial transactions in America.
490
00:34:06,217 --> 00:34:10,627
So in the United States,
checks are used everywhere.
491
00:34:11,877 --> 00:34:13,447
New Zealand stopped accepting checks.
492
00:34:13,477 --> 00:34:17,067
Like banks don't literally, you can't
seem to use a check in our country.
493
00:34:17,686 --> 00:34:18,696
Same in Finland, right?
494
00:34:18,696 --> 00:34:19,926
They don't have checkbooks.
495
00:34:21,007 --> 00:34:30,457
Yeah, it's like, not a thing
there's, and, uh, uh, and so, and
496
00:34:30,557 --> 00:34:34,297
we don't expect that messages are
going to be, are going to be seen.
497
00:34:34,337 --> 00:34:38,517
I was going to say telegram or
something like things change and,
498
00:34:39,117 --> 00:34:43,277
uh, the tools will get good enough.
499
00:34:44,122 --> 00:34:52,382
That the boring work of like literally
typing, touching the keyboard, getting
500
00:34:52,692 --> 00:34:59,082
the program written will be done the
hard part of the system design, the hard
501
00:34:59,082 --> 00:35:04,322
part of like developing the product, the,
the finding how the components work and,
502
00:35:04,322 --> 00:35:09,462
and that will still, you'll be driving
that, but you're essentially, you'll be,
503
00:35:09,662 --> 00:35:14,182
yeah, you will be driving these, these AI
agents to essentially create or co create.
504
00:35:15,217 --> 00:35:22,297
Um, some sort of artifact and that will
be difficult shift for many people.
505
00:35:22,797 --> 00:35:27,387
And, but I think that overall it'll be.
506
00:35:28,587 --> 00:35:32,287
Like artisanal, artisanal software
development where, you know, people
507
00:35:32,287 --> 00:35:36,817
will, it's just like having like
handmade, handmade shoes feels, uh,
508
00:35:37,117 --> 00:35:43,747
very, um, very old fashioned and very,
I think I'm forgetting a word, but,
509
00:35:44,097 --> 00:35:47,822
but some people still like to have,
to have, um, Shoes made by hand.
510
00:35:47,892 --> 00:35:50,042
And lots of people would
love to pay if they could.
511
00:35:50,292 --> 00:35:54,442
Um, and in Japan, we still have handmade
shoes, but, um, in lots of places, but
512
00:35:54,892 --> 00:35:59,882
most people's shoes are made in factories
and, uh, and, and they're mass produced.
513
00:36:00,152 --> 00:36:03,412
And so I think most software will
be in some sense, mass produced.
514
00:36:04,612 --> 00:36:10,257
well, and, Uh, And I think maybe
the way I think about it is we're
515
00:36:10,257 --> 00:36:16,837
moving one level of abstraction
up, so it's no longer about, about,
516
00:36:17,197 --> 00:36:18,957
Oh, how do I write this function?
517
00:36:18,957 --> 00:36:21,517
It's more about, I'm writing this object.
518
00:36:21,547 --> 00:36:25,257
I'm creating this object, which knows
how to interact with other objects.
519
00:36:25,557 --> 00:36:32,037
And then now we're saying, don't
even worry about the object, Class.
520
00:36:32,087 --> 00:36:32,917
Don't worry about that.
521
00:36:33,137 --> 00:36:35,047
Now move on to, let's.
522
00:36:35,827 --> 00:36:37,917
modules that you're working on.
523
00:36:38,267 --> 00:36:42,117
Your problem solving techniques are
now coming into the module because
524
00:36:42,117 --> 00:36:49,007
the rest of the stuff we can go manage
and we can do it with guardrails in
525
00:36:49,007 --> 00:36:51,037
place, with verification in place.
526
00:36:52,523 --> 00:36:54,143
The future that you're describing here.
527
00:36:54,163 --> 00:36:59,353
I look, I think I, you know, it's
very, it's very easy to, oh, like
528
00:36:59,473 --> 00:37:02,123
there's a bootstrapping problem
where if you start with a program,
529
00:37:02,153 --> 00:37:03,473
you need to kind of handwrite.
530
00:37:03,983 --> 00:37:06,943
The, the, the, the, the
properties that you wish to kind
531
00:37:06,943 --> 00:37:08,283
of guarantee, blah, blah, blah.
532
00:37:08,843 --> 00:37:13,983
And, but yeah, but it's just
a kind of a fascinating idea.
533
00:37:14,043 --> 00:37:20,353
So then the question that becomes
like, why would, what is important
534
00:37:20,453 --> 00:37:25,893
about the Rust standard library
as part of this overall process?
535
00:37:27,093 --> 00:37:31,143
Why is that the next thing to do?
536
00:37:32,372 --> 00:37:36,622
Yeah, so, there's two parts,
or well, three parts to it.
537
00:37:36,972 --> 00:37:45,022
One, the Rust standard library, know, uh,
contrary to popular belief, does have bugs
538
00:37:45,022 --> 00:37:47,262
in it which have been exposed in the past.
539
00:37:47,932 --> 00:37:49,492
Yes, uh,
540
00:37:49,623 --> 00:37:50,793
We don't talk about these things.
541
00:37:51,862 --> 00:37:52,192
yeah.
542
00:37:52,473 --> 00:37:52,713
Yeah.
543
00:37:52,753 --> 00:37:53,583
It turns out it's just software.
544
00:37:54,783 --> 00:37:59,768
so, so, When you want to build
a house, where do you start?
545
00:38:00,968 --> 00:38:03,768
You start with the foundation
and our foundation is the
546
00:38:03,768 --> 00:38:04,958
core and the standard library.
547
00:38:05,718 --> 00:38:14,318
if we can, not if, but when we make
our tools actually do this for the
548
00:38:14,328 --> 00:38:22,838
core, the foundation automagically,
yes, automagically, we can start making
549
00:38:22,838 --> 00:38:25,668
it work for everything else above it.
550
00:38:26,723 --> 00:38:28,533
And that's the number one reason,
551
00:38:29,224 --> 00:38:32,964
So is part of the reason why that
magic happens is once the tools are
552
00:38:32,964 --> 00:38:36,334
good enough to do it in the standard
library, which is in some sense the
553
00:38:36,334 --> 00:38:43,174
most impactful, uh, you know, like,
uh, library that Rust programmers have
554
00:38:43,214 --> 00:38:50,434
access to, um, then everywhere else
should be at least no more difficult.
555
00:38:51,634 --> 00:38:51,974
Yes.
556
00:38:51,994 --> 00:38:53,614
That's a great insight on your part.
557
00:38:53,734 --> 00:38:56,384
That is, that is one of
the ideas here, right?
558
00:38:56,694 --> 00:39:02,464
That the, the second point is the Rust
Center Library will challenge our tools.
559
00:39:03,344 --> 00:39:06,674
will make us push the boundary.
560
00:39:07,684 --> 00:39:10,304
And that's fantastic, right?
561
00:39:11,785 --> 00:39:20,955
Your, uh, I suppose that the, the fact
that a lot of Rust programmers use non,
562
00:39:21,075 --> 00:39:25,285
the no standard attributes, such that
essentially they turn off the standard
563
00:39:25,285 --> 00:39:30,685
library is slightly orthogonal to this,
because if I'm just on an embedded device,
564
00:39:31,130 --> 00:39:32,800
I could still use the verification tools.
565
00:39:32,800 --> 00:39:33,630
They still exist.
566
00:39:33,880 --> 00:39:39,960
And, um, but essentially this is a
big, ambitious, difficult project.
567
00:39:40,250 --> 00:39:46,630
Um, and you're attempting to use the, the,
the program of work as a way to kind of
568
00:39:46,630 --> 00:39:56,440
recruit or, uh, essentially kind of gather
a community of researchers to, uh, or at
569
00:39:56,440 --> 00:40:04,430
least this is kind of kind of, I'm trying
to figure out where, at what point did you
570
00:40:04,430 --> 00:40:06,375
think Think, you know what we should do?
571
00:40:06,965 --> 00:40:10,205
We should turn this into like
an X prize, like an awards.
572
00:40:10,555 --> 00:40:13,095
Uh, you know, we should,
we should essentially.
573
00:40:13,184 --> 00:40:14,924
tell you exactly when I thought that.
574
00:40:15,285 --> 00:40:15,615
Okay.
575
00:40:16,624 --> 00:40:21,044
It's when I realized the amount of
unsafe code in the Rust standard library.
576
00:40:21,694 --> 00:40:26,014
And, okay, one team
cannot actually do this.
577
00:40:26,624 --> 00:40:28,684
I need a lot more support.
578
00:40:29,064 --> 00:40:37,734
And then, you know, uh, I, believe the
Rust community is an amazing community.
579
00:40:38,679 --> 00:40:42,159
It has been a fascinating
community for me, at least.
580
00:40:42,899 --> 00:40:46,799
I realized, well, I think
that people would like to
581
00:40:46,799 --> 00:40:49,969
contribute because three reasons.
582
00:40:49,969 --> 00:40:54,309
Number one, benefits everyone, right?
583
00:40:54,369 --> 00:40:59,029
This benefits, it benefits people who
are building on top of Rust, creating
584
00:40:59,029 --> 00:41:01,029
their applications, their scenarios.
585
00:41:01,349 --> 00:41:04,079
It benefits people who
are developing Rust.
586
00:41:04,289 --> 00:41:10,349
It benefits academia, students,
uh, researchers, industry.
587
00:41:10,849 --> 00:41:12,949
Uh, it's a win, win, win, win.
588
00:41:13,699 --> 00:41:19,449
And, uh, I thought, well, okay, but
you know, if I just go post a message
589
00:41:19,449 --> 00:41:22,979
saying, Hey, let's go verify the
Rust library, well, it's probably
590
00:41:22,979 --> 00:41:27,459
going to get drowned in the, in the
plethora and the sea of, of, uh, all
591
00:41:27,459 --> 00:41:28,889
the messages that are being posted.
592
00:41:29,949 --> 00:41:34,739
So the effort was born out of
let's make it more organized
593
00:41:34,799 --> 00:41:36,389
and let's jumpstart this.
594
00:41:36,819 --> 00:41:39,849
Because I think there's a lot of
people who are motivated out there
595
00:41:40,939 --> 00:41:46,699
who want to do something like this,
this gives them a great cause.
596
00:41:47,415 --> 00:41:47,665
Hmm.
597
00:41:48,575 --> 00:41:48,605
Okay.
598
00:41:49,805 --> 00:41:54,455
Yeah, the Rust community is not, by
the Rust community, the messages,
599
00:41:54,485 --> 00:41:57,055
where the message are presumably you
would have sent if you would have sort
600
00:41:57,055 --> 00:42:00,275
of say, Hi, by the way, I'm looking
for, would have been like the Zulip
601
00:42:00,605 --> 00:42:02,975
channel, like the main one, presumably.
602
00:42:03,244 --> 00:42:03,634
Sure.
603
00:42:04,075 --> 00:42:08,095
I find myself lost in there all the time.
604
00:42:08,305 --> 00:42:14,915
So, uh, I get, I can imagine that,
yeah, it's very highly likely that your
605
00:42:14,915 --> 00:42:20,555
message would have been like either,
either ignored or you would have
606
00:42:20,555 --> 00:42:25,175
generated such a heated discussion that
it would have been like, let's, yeah.
607
00:42:25,284 --> 00:42:26,904
I've seen a few of those recently.
608
00:42:27,160 --> 00:42:27,760
Okay.
609
00:42:27,890 --> 00:42:28,070
Yeah.
610
00:42:28,070 --> 00:42:28,340
Right.
611
00:42:29,540 --> 00:42:37,920
Um, there is actually an effort outside of
AWS that I noticed that you posted about.
612
00:42:37,920 --> 00:42:45,800
So I, uh, there was, I saw a YouTube
video from CMU students, uh, about
613
00:42:45,810 --> 00:42:47,620
verifying the standard library.
614
00:42:48,230 --> 00:42:51,090
And your name is attached there somehow.
615
00:42:51,150 --> 00:42:54,910
So what's your relationship with the
university, with the academic project?
616
00:42:54,940 --> 00:43:00,200
And, uh, presumably there's some
wider context that I think would
617
00:43:00,200 --> 00:43:01,380
be really nice to hear about.
618
00:43:02,580 --> 00:43:03,060
Yeah.
619
00:43:03,060 --> 00:43:05,600
Oh, I mean, you are up to date, obviously.
620
00:43:05,910 --> 00:43:13,410
Uh, so, uh, CMU has, um, uh, uh, an
initiative, um, an innovators initiative,
621
00:43:14,630 --> 00:43:20,730
which, uh, where they, they do what's
called a practicum project, these are
622
00:43:20,730 --> 00:43:27,720
students who end up spending a semester
selecting what projects they want to work
623
00:43:27,720 --> 00:43:30,560
on from a, a proposed set of projects.
624
00:43:31,720 --> 00:43:32,480
Uh, just so,
625
00:43:33,606 --> 00:43:35,596
I was going to interject very
slightly just in case there's
626
00:43:35,596 --> 00:43:37,086
any listeners that know Latin.
627
00:43:37,436 --> 00:43:43,904
I've always called that practicum,
but practicum, I, anyway, the, I'm
628
00:43:43,904 --> 00:43:52,241
like, uh, yeah, it's funny how we
have kind of the like English holds
629
00:43:52,241 --> 00:43:57,651
on in tiny, tiny fragments of like,
uh, and let's say a more learned age,
630
00:43:57,801 --> 00:44:00,401
although much more colonial and far.
631
00:44:00,430 --> 00:44:02,170
still spell knife with a K
632
00:44:02,376 --> 00:44:02,986
Yeah, sure.
633
00:44:03,196 --> 00:44:03,776
That's right.
634
00:44:03,976 --> 00:44:04,336
Yeah.
635
00:44:04,676 --> 00:44:05,906
The K N thing.
636
00:44:05,936 --> 00:44:07,446
I don't get like knife, knave.
637
00:44:07,726 --> 00:44:08,836
Anyway, sorry.
638
00:44:08,886 --> 00:44:10,276
I completely derailed you.
639
00:44:10,566 --> 00:44:15,606
And yes, so we have practicum, which,
uh, probably provides an opportunity for
640
00:44:15,606 --> 00:44:17,386
students to work on an industry project.
641
00:44:17,416 --> 00:44:19,576
That's just normally how
these things are structured.
642
00:44:20,310 --> 00:44:23,560
There's actually a wide variety
of sponsors who come there.
643
00:44:24,140 --> 00:44:27,690
Uh, they're, they're from
either academia or industry.
644
00:44:28,125 --> 00:44:35,235
And, uh, uh, we got, so I got the
opportunity to present this idea for
645
00:44:35,235 --> 00:44:41,985
verifying the Rust standard library,
and we ended up with four teams, four
646
00:44:41,985 --> 00:44:48,095
very wonderful teams, I might add, uh,
four plus one students each, uh, four
647
00:44:48,125 --> 00:44:54,895
students, one, one kind of, uh, program
manager person, uh, a couple of faculty
648
00:44:54,895 --> 00:44:58,715
members, and they took on four challenges.
649
00:44:59,770 --> 00:45:07,700
You know, let me, me tell you, uh,
not all of these students had any
650
00:45:07,860 --> 00:45:09,610
formal verification background.
651
00:45:10,810 --> 00:45:13,860
Some of them did not
have any Rust background.
652
00:45:15,060 --> 00:45:17,300
Yes, that reaction is correct.
653
00:45:17,726 --> 00:45:17,946
Yeah.
654
00:45:17,946 --> 00:45:20,316
And I'm sorry if any
of them is audio only.
655
00:45:21,766 --> 00:45:21,976
Yeah.
656
00:45:21,976 --> 00:45:25,016
I'm, I'm like, so they're sitting here
kind of like slightly puzzled or startled.
657
00:45:25,066 --> 00:45:25,596
Amazed.
658
00:45:25,596 --> 00:45:26,336
I can't quite tell.
659
00:45:26,426 --> 00:45:29,336
I don't know which adjective is
correct, but that's fascinating.
660
00:45:30,850 --> 00:45:34,530
And Each team took on a challenge.
661
00:45:34,860 --> 00:45:37,650
Uh, we completed a couple of challenges.
662
00:45:37,930 --> 00:45:40,690
Uh, the other two are,
are almost finished.
663
00:45:41,050 --> 00:45:45,170
And students happen to be engaged
even after the work is done.
664
00:45:45,190 --> 00:45:47,830
They have created blog posts, videos.
665
00:45:48,280 --> 00:45:50,770
They learned how to write Kani harnesses.
666
00:45:51,080 --> 00:45:53,040
They learned about Rust semantics.
667
00:45:53,340 --> 00:45:55,720
They pushed Kani to a new level.
668
00:45:55,720 --> 00:45:59,090
They were filing issues against
Kani saying this doesn't work.
669
00:46:00,290 --> 00:46:07,450
Was absolutely inspirational see
these students take this idea
670
00:46:08,460 --> 00:46:09,900
and actually make it a reality.
671
00:46:09,910 --> 00:46:14,380
And, you know, in my head, I thought,
wow, this is the birth of a new
672
00:46:14,380 --> 00:46:17,100
generation of, computer scientists.
673
00:46:17,501 --> 00:46:17,991
Yeah,
674
00:46:18,650 --> 00:46:19,750
me at the end.
675
00:46:21,201 --> 00:46:26,021
that's also, I, yeah, I, there are like
multiple levels in which I'm amazed.
676
00:46:27,221 --> 00:46:32,671
And the first of all, like being able
to recruit four teams of multiple
677
00:46:32,671 --> 00:46:38,671
researchers, uh, most of all that is like,
uh, like that, that, that, that isn't
678
00:46:38,961 --> 00:46:45,641
like an acknowledgement of essentially
the gravity or, uh, of, of, of, of
679
00:46:45,641 --> 00:46:49,971
this effort, um, and the way that it's
perceived and the importance of Rust.
680
00:46:51,051 --> 00:46:55,021
Rust is no longer, I think I've been
saying this for like about a year,
681
00:46:55,261 --> 00:46:56,741
Rust is no longer a new language.
682
00:46:57,971 --> 00:47:06,751
Like Rust is novel anymore in the
sense of it's not considered unsafe.
683
00:47:07,581 --> 00:47:08,311
Sorry, wrong term.
684
00:47:08,551 --> 00:47:13,401
It's not considered kind of a, I don't
think that there will be companies that
685
00:47:13,401 --> 00:47:16,001
look at Rust and think, ah, right, right.
686
00:47:16,011 --> 00:47:18,011
That's a, that's, that's a, yeah, totally.
687
00:47:18,351 --> 00:47:18,801
And.
688
00:47:19,426 --> 00:47:21,102
I
689
00:47:21,411 --> 00:47:28,051
in, in, on that side where people know
that if they were to work on this, that,
690
00:47:28,461 --> 00:47:30,481
and like solve one of these challenges,
691
00:47:31,159 --> 00:47:32,835
Um.
692
00:47:33,361 --> 00:47:36,811
large impact all around the world.
693
00:47:37,531 --> 00:47:41,051
Um, the other level was that, yeah,
these people were, sorry, these
694
00:47:41,051 --> 00:47:46,011
students were relatively new either
to formal verification, Rust or both,
695
00:47:46,291 --> 00:47:50,166
still were able to make Really strong
forward progress, which means that
696
00:47:50,196 --> 00:47:54,126
the tools themselves, such as Kani and
its ability to have custom properties
697
00:47:54,126 --> 00:47:57,316
and harnesses, uh, is is learnable.
698
00:47:57,736 --> 00:48:00,216
And that's very, very positive.
699
00:48:00,666 --> 00:48:07,126
Um, and then this continuing engagement
and being able to create content about
700
00:48:07,186 --> 00:48:12,236
exploration and blog posts and so
forth is a very nice finishing touch
701
00:48:12,256 --> 00:48:18,356
because it means that people have been
sufficiently engaged to share, which
702
00:48:18,386 --> 00:48:22,326
means that, uh, they, they, you know,
the whole process was fulfilling.
703
00:48:22,336 --> 00:48:29,926
I mean, I don't want to gush too much
about this effort and, uh, but no, no, no,
704
00:48:29,926 --> 00:48:40,001
it's, it's, it's, very ambitious and I am
extremely excited that someone has decided
705
00:48:41,421 --> 00:48:46,411
to use their position, uh, and like their
expertise in the networks to drive this.
706
00:48:46,411 --> 00:48:48,701
And so I, so thank you to you.
707
00:48:50,450 --> 00:48:51,550
Oh, thank you, Tim.
708
00:48:51,600 --> 00:48:57,250
I, I, I have a lot of people to thank,
uh, you know, uh, the Rust Foundation
709
00:48:57,260 --> 00:48:59,250
has been amazing during this process.
710
00:48:59,720 --> 00:49:05,660
Uh, Amazon itself has actually
put money forward and, and my
711
00:49:05,660 --> 00:49:08,470
leadership has been very supportive.
712
00:49:08,750 --> 00:49:16,350
People like you who understand, my
team has just done so much work.
713
00:49:16,370 --> 00:49:22,385
I mean, We started the year with
zero verified functions, and
714
00:49:22,385 --> 00:49:28,195
we ended the year with 255 or a
few more now verified functions,
715
00:49:28,705 --> 00:49:32,245
basically one a day, uh, if you will.
716
00:49:32,635 --> 00:49:35,335
Uh, that's really cool.
717
00:49:35,335 --> 00:49:38,815
And, and next year, you know, we
wanna increase the order of magnitude.
718
00:49:38,815 --> 00:49:41,955
We want to get into the thousands,
and we want to get this into
719
00:49:41,955 --> 00:49:44,405
the mainline, uh, the contracts.
720
00:49:45,445 --> 00:49:50,415
Rust is going to have contracts soon, and
we've been a part of those discussions.
721
00:49:51,615 --> 00:49:56,195
It is a great thing to have
contracts at the end of the day.
722
00:49:57,105 --> 00:50:03,075
a great thing to have formal
verification come into this light,
723
00:50:03,175 --> 00:50:08,865
because I do believe those are the
only guardrails has eventually.
724
00:50:09,655 --> 00:50:10,225
Um,
725
00:50:10,571 --> 00:50:18,111
Yeah, look, I mean, you can't ask the AI
to just write a test that will, it would
726
00:50:18,121 --> 00:50:24,331
be nice to make sure that, that the thing
is doing what it says that it's doing.
727
00:50:24,491 --> 00:50:27,951
And that it's essentially not spiraling.
728
00:50:29,161 --> 00:50:30,731
Out into mayhem.
729
00:50:30,991 --> 00:50:35,831
Uh, and yes, the Rust compiler, you know,
once it compiles, it runs and you kind of,
730
00:50:36,201 --> 00:50:42,141
you have some degree of assurance that you
at least have a working program, but it
731
00:50:42,141 --> 00:50:46,341
would be nice to go that next extra step
to say that you have a correct program.
732
00:50:46,841 --> 00:50:48,836
Um, No.
733
00:50:48,836 --> 00:50:49,526
Amazing.
734
00:50:49,706 --> 00:50:50,636
And thank you all.
735
00:50:50,715 --> 00:50:52,565
only nice, but required
736
00:50:53,215 --> 00:50:53,715
opinion.
737
00:50:54,915 --> 00:50:58,545
Yeah, but see this is the, this is
the whole frame of reference in which
738
00:50:59,055 --> 00:51:06,915
I'm currently operating in that at
the moment we don't have the idea
739
00:51:06,975 --> 00:51:12,565
that it's possible to formally verify,
kind of baked into the process.
740
00:51:12,805 --> 00:51:17,965
And so it's seen by, at least,
you know, you can tell that my.
741
00:51:18,480 --> 00:51:22,080
Our own preconceptions are kind of
like pushing against the idea that
742
00:51:22,080 --> 00:51:26,260
this could become a part of every day.
743
00:51:26,260 --> 00:51:30,590
In fact, it will become central to
it because it will be the foundation
744
00:51:30,860 --> 00:51:35,680
that the rest of the program sits
on, especially if this future comes
745
00:51:35,680 --> 00:51:41,210
true where the computer is doing a
lot of the writing of the software.
746
00:51:41,660 --> 00:51:48,220
And, uh, yeah, no, so thank you very much
for sharing with, uh, with everybody,
747
00:51:48,430 --> 00:51:53,590
uh, the story of, um, of verifying the
Rust standard library, as well as, uh,
748
00:51:53,590 --> 00:51:57,170
something which I was very unexpected
to me, this idea of essentially, um,
749
00:51:57,360 --> 00:52:01,780
creating this secure foundation for a
new paradigm of software development.
750
00:52:01,890 --> 00:52:05,510
And, um, in 20 years, we might
have another conversation and
751
00:52:05,510 --> 00:52:07,450
find out, um, whether or not.
752
00:52:07,950 --> 00:52:10,030
It happened or like what
it actually looks like.
753
00:52:10,030 --> 00:52:12,890
So I, uh, I wish you all the best.
754
00:52:14,284 --> 00:52:14,574
Thank you.
755
00:52:14,824 --> 00:52:15,754
Thank you very much.
756
00:52:15,814 --> 00:52:18,514
And, uh, I hope it's sooner than 20 years.
757
00:52:18,790 --> 00:52:19,140
Yeah.
758
00:52:19,190 --> 00:52:19,460
Yeah.
759
00:52:20,770 --> 00:52:21,060
Right.
760
00:52:21,290 --> 00:52:21,500
Right.
761
00:52:21,530 --> 00:52:21,960
Okay.
762
00:52:23,580 --> 00:52:24,590
People can take their bets.
763
00:52:27,026 --> 00:52:31,356
You've been listening to Compose, a
podcast for software developers interested
764
00:52:31,356 --> 00:52:32,736
in the Rust programming language.
765
00:52:33,766 --> 00:52:37,826
My name is Tim McNamara, also known
as timclicks, and you can find
766
00:52:37,836 --> 00:52:40,726
further resources at timclicks.
767
00:52:40,726 --> 00:52:40,896
dev.
768
00:52:42,016 --> 00:52:42,906
At timclicks.
769
00:52:42,946 --> 00:52:48,666
dev you'll find tutorials, videos and
articles all geared around helping you
770
00:52:48,666 --> 00:52:52,236
to get better at the Rust programming
language to build a better planet.
771
00:52:53,876 --> 00:52:57,746
If you've enjoyed this episode,
then here's a suggestion.
772
00:52:58,766 --> 00:53:03,036
Try to apply formal verification
to one of your projects today.
773
00:53:03,866 --> 00:53:05,386
Check the show notes for resources
774
00:53:06,536 --> 00:53:11,436
Check the show notes for links to
resources for you to get started.
775
00:53:13,386 --> 00:53:14,026
Take care.
776
00:53:14,136 --> 00:53:14,726
Have fun.
777
00:53:14,726 --> 00:53:16,206
I'll see you on the next episode.
