WEBVTT

NOTE Sentence-level transcript of https://www.youtube.com/watch?v=-CnA2lGfymY

NOTE One cue per sentence. Cue ids are the line anchors on /transcripts/-CnA2lGfymY.html. A cue ends where the next begins, or 2 s after its last word.

s1
00:00:01.309 --> 00:00:03.309
[music]

s2
00:00:13.040 --> 00:00:20.200
Please welcome to the stage the research scholar at Live Nets Labs, Eric Meyer.

s3
00:00:37.760 --> 00:00:42.400
Well, um can you go back one slide?

s4
00:00:42.400 --> 00:00:43.680
Sorry.

s5
00:00:43.680 --> 00:00:44.880
All right.

s6
00:00:44.880 --> 00:00:46.600
Good afternoon, everybody.

s7
00:00:46.600 --> 00:00:52.200
Thanks for being here after a long day of talks, exhibits, side effects.

s8
00:00:52.200 --> 00:00:54.960
Oh, sorry, that was the side events.

s9
00:00:54.960 --> 00:01:03.400
Um I hope that um you have as much fun watching this talk as I had uh creating it.

s10
00:01:04.720 --> 00:01:07.680
Um let me first get this out of the way.

s11
00:01:07.680 --> 00:01:10.920
This is not a product pitch or announcement or anything.

s12
00:01:10.920 --> 00:01:22.320
It's a 20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe.

s13
00:01:22.320 --> 00:01:25.680
And I'm sharing all my secrets with you today.

s14
00:01:25.680 --> 00:01:37.800
Um hopefully to kind of inspire some of you that next year you will have a booth downstairs where you have kind of like, you know, created a provably safe agentic

s15
00:01:37.800 --> 00:01:39.000
harness.

s16
00:01:39.000 --> 00:01:43.120
Um or who knows, maybe some of you have already solved it.

s17
00:01:43.120 --> 00:01:48.640
Let me know, and then, you know, we can grab a coffee instead of doing this talk.

s18
00:01:48.640 --> 00:01:52.840
Um with that out of the way, let's get going.

s19
00:01:52.840 --> 00:02:02.920
Um while I was preparing these slides, and I'm sorry that I was multitasking, but I was site five coding on the side.

s20
00:02:02.920 --> 00:02:14.120
Um and then, when my attention waned for a second because I was trying to convince the model to draw some pictures that it didn't want to do, and you will see some of these pictures later.

s21
00:02:14.120 --> 00:02:17.680
You can guess which ones were rejected.

s22
00:02:17.680 --> 00:02:20.120
Suddenly, wham!

s23
00:02:20.120 --> 00:02:23.000
Claude code deleted one of my files.

s24
00:02:23.000 --> 00:02:27.360
And I'm sure this has happened to you before.

s25
00:02:27.360 --> 00:02:28.680
Um or maybe not.

s26
00:02:28.680 --> 00:02:34.920
Maybe you always kind of like, you know, run everything with no permissions, and then you say yes, yes, yes.

s27
00:02:34.920 --> 00:02:37.920
But I like to live dangerously.

s28
00:02:37.920 --> 00:02:51.760
Um but I'm convinced that if there's anything between the model's goal and where the model currently is, it will do everything that it can to reach that goal, including

s29
00:02:51.760 --> 00:02:56.080
killing us or deleting your files or deleting your database.

s30
00:02:56.080 --> 00:03:02.280
So, I think that these models are intrinsically very, very dangerous, and we have to tame them.

s31
00:03:02.280 --> 00:03:04.600
So, that's what my talk is about.

s32
00:03:04.600 --> 00:03:08.640
Um So, let's kind of like, you know, start this story.

s33
00:03:08.640 --> 00:03:23.280
Um and it's, I think, a very, very sad story, but also a scary story of how we as an industry got to this point where we are about to let normal people, the general public,

s34
00:03:23.280 --> 00:03:31.720
give control of their computers, their finances, their whole personal lives over to AI agents.

s35
00:03:31.720 --> 00:03:34.519
And we don't have any protection in place.

s36
00:03:34.519 --> 00:03:38.600
Um I think that's very sad and very scary.

s37
00:03:38.600 --> 00:03:47.959
Um so, let me tell you the story how we got there, and I will kind of like have some characters uh like Claude, and we will see Dario, Daniela,

s38
00:03:47.959 --> 00:03:49.680
Sam, Bernie.

s39
00:03:49.680 --> 00:03:57.160
Uh but um the main character is is our friendly pit cloud here.

s40
00:03:57.160 --> 00:04:04.000
Um I think you can all remember um November 30, 2022.

s41
00:04:04.000 --> 00:04:11.280
This was a kind of like a very special day in in history because this is the first time that you could speak to your computer.

s42
00:04:11.280 --> 00:04:14.160
You could say, "Hey, summarize my emails."

s43
00:04:14.160 --> 00:04:19.799
And it would you know, um answer you in perfect English.

s44
00:04:19.799 --> 00:04:33.600
Um I think for me at least that was magic, but I think most of us didn't realize that by introducing this innocent-looking function here, LLM, that takes a question and returns an answer,

s45
00:04:33.600 --> 00:04:39.480
that that would open Pandora's Box and that would change our history forever.

s46
00:04:39.480 --> 00:04:48.800
Um but before we go continue the story, this conference is called AI Engineer.

s47
00:04:48.800 --> 00:04:56.919
All right, so we are engineers and maybe we're the last generation of engineers that still understand what this is, what code is.

s48
00:04:56.919 --> 00:05:03.320
Um or maybe most of you have already forgotten what code is because all your code is written by agents.

s49
00:05:03.320 --> 00:05:09.800
But if we look at this signature here, it says it the LLM takes a question and returns an answer.

s50
00:05:09.800 --> 00:05:11.600
The question and answers are not strings.

s51
00:05:11.600 --> 00:05:19.320
They are very complicated JSON structures and they get more complicated every day, every time a new release of APIs comes out.

s52
00:05:19.320 --> 00:05:24.400
But for this talk, we can just assume that question and answer are just opaque types.

s53
00:05:24.400 --> 00:05:27.600
We we don't care about how they look like.

s54
00:05:27.600 --> 00:05:31.680
We do care about what they represent.

s55
00:05:31.680 --> 00:05:40.520
Um Now, anyway, the euphoria of like these LLMs as being great tools didn't last very long.

s56
00:05:40.520 --> 00:05:54.360
And just when we thought that we have eradicated the smallpox of computer science, SQL injection, it came back with a vengeance because the bad guys discovered that you can trick LLMs

s57
00:05:54.360 --> 00:06:09.640
using prompt injection and LLMs have no distinction make no distinction between code and and and text and so they're very very easy to trick and this I think is a bigger problem than SQL injection

s58
00:06:09.640 --> 00:06:11.600
ever was.

s59
00:06:11.600 --> 00:06:18.520
Um but it was not prompt injection only that made LLMs kind of like have a bad rap.

s60
00:06:18.520 --> 00:06:27.919
LLMs are trained on the whole internet and there's like a lot of good stuff on the internet but also a lot of bad stuff like how do you create a bomb?

s61
00:06:27.919 --> 00:06:29.520
How do you synthesize drugs?

s62
00:06:29.520 --> 00:06:32.080
How do you hack into people's systems?

s63
00:06:32.080 --> 00:06:43.960
And the leaders of the big foundation labs they got a little bit worried that the that the government would interfere and regulated the industry so they told their PhD researchers

s64
00:06:43.960 --> 00:06:48.160
go find a solution for this problem right now AND QUICK.

s65
00:06:48.160 --> 00:06:53.240
COME ON, SOLVE IT BEFORE YOU KNOW the the government steps in.

s66
00:06:53.240 --> 00:07:07.440
Um and here the PhD types since they're PhD types they thought long and hard about the safety problem and they came up with a new interface for LLMs.

s67
00:07:07.440 --> 00:07:10.440
That's this kind of scary on the right.

s68
00:07:10.440 --> 00:07:11.640
Look at that.

s69
00:07:11.640 --> 00:07:12.320
What does it say?

s70
00:07:12.320 --> 00:07:16.440
There's like some sigma Greek symbols, there's proofs, whatever.

s71
00:07:16.440 --> 00:07:18.480
Well, that is Lean.

s72
00:07:18.480 --> 00:07:20.160
Probably you have heard of Lean.

s73
00:07:20.160 --> 00:07:22.120
Anyone here heard of Lean?

s74
00:07:22.120 --> 00:07:24.880
Lean is now like the hot thing, right?

s75
00:07:24.880 --> 00:07:32.240
Like VCs are are writing like multi-billion dollar checks if you just say that you're doing something with Lean.

s76
00:07:32.240 --> 00:07:40.400
And of course these PhD types researchers are using Lean and you have to suffer because of that.

s77
00:07:40.400 --> 00:07:47.720
Um now let's first look at the signature in a slightly simpler language called um Daphne.

s78
00:07:47.720 --> 00:07:53.520
And what this thing says is that the LLM takes a question, returns an answer.

s79
00:07:53.520 --> 00:08:03.000
It requires this question to be proper, which means that it's not an offensive question, and then the model returns a safe uh answer.

s80
00:08:03.000 --> 00:08:05.840
And this thing is proved automatically.

s81
00:08:05.840 --> 00:08:09.800
So, if you give it a proper question, it gives you a safe answer.

s82
00:08:09.800 --> 00:08:15.160
Um Now, I think there's too much attention for Lean.

s83
00:08:15.160 --> 00:08:18.440
I'm a recovering type-a-holic and math addict.

s84
00:08:18.440 --> 00:08:30.520
Um I love Lean, but there's many, many other theorem provers and uh model checkers out there like Isabelle, Rock, PVS, TLAPlus.

s85
00:08:30.520 --> 00:08:36.120
Um but Lean is the grease that got like, keeps the VC money pumps going.

s86
00:08:36.120 --> 00:08:39.440
So, I will use Lean um today.

s87
00:08:39.440 --> 00:08:44.720
So, here here's the got like, you know, the the uh interface again in Lean.

s88
00:08:44.720 --> 00:08:49.000
And now in Lean, you don't do automatic theorem proving.

s89
00:08:49.000 --> 00:08:55.800
If you're like a Lean expert, you will say, "Eric, well, we have grind in Lean, but let's got like, you know, put that aside for a minute."

s90
00:08:55.800 --> 00:09:06.600
Um but in Lean, you have to both show that the how to compute the the result type, and you have to do the proof by hand.

s91
00:09:06.600 --> 00:09:12.360
Um so, it's it's slightly different than um the Daphne example.

s92
00:09:12.360 --> 00:09:25.440
But if you think about this thing for just a single nanosecond, you will realize that it's impossible to write a formal proof that an answer is safe or a question is proper.

s93
00:09:25.440 --> 00:09:35.800
Um and that is why there are at least a hundred startups down here in the exhibition hall that are using LLMs as a judge, because this is not something that you can formally specify.

s94
00:09:35.800 --> 00:09:38.360
What does it mean that an answer is safe?

s95
00:09:38.360 --> 00:09:40.720
That's not a mathematical property.

s96
00:09:40.720 --> 00:09:47.120
Um And of course, if you own a foundation model like these guys, you don't need external LLMs as a judge.

s97
00:09:47.120 --> 00:09:52.600
You just um bake it into the weights and you call it the model is aligned.

s98
00:09:52.600 --> 00:10:01.280
Um But unfortunately, trying to bake alignment into the model is not foolproof and models get routinely jailbroken.

s99
00:10:01.280 --> 00:10:08.680
So, they had to go to the Pope and ask it to get like, you know, um bless their model that it's safe.

s100
00:10:08.680 --> 00:10:16.680
Um Now, I think it's terrible if like a model says something offensive, but those are just words.

s101
00:10:16.680 --> 00:10:21.760
And ultimately, the words are are like they just like, you know, they drip off your body.

s102
00:10:21.760 --> 00:10:23.120
They don't do anything.

s103
00:10:23.120 --> 00:10:26.520
Some human has to act on words to make them dangerous.

s104
00:10:26.520 --> 00:10:38.400
Um and so, maybe that is what they mean by broadly safe um when Anthropic uh uh talks about safety um because it's still a human involved.

s105
00:10:38.400 --> 00:10:40.560
But then something terrible happened.

s106
00:10:40.560 --> 00:10:45.760
Something really terrible happened that changed the world forever.

s107
00:10:45.760 --> 00:10:53.120
And that is in June 2023, OpenAI announced tool call support in GPT-4.

s108
00:10:53.120 --> 00:10:58.080
And of course, all the other vendors rushed out to copy this.

s109
00:10:58.080 --> 00:11:05.160
This is called the principle of minimum differentiation and that is why all these APIs uh look the same.

s110
00:11:05.160 --> 00:11:15.360
Um Now, the act of adding tool calls changes AI safety from a philosophical debate to something that causes real danger.

s111
00:11:15.360 --> 00:11:19.920
You could say tool calls give the model claws in addition to a mouth.

s112
00:11:19.920 --> 00:11:25.640
Or you can say tool calls is like handing a gun a loaded gun to them.

s113
00:11:25.640 --> 00:11:29.839
But of course, nobody listens to me.

s114
00:11:29.839 --> 00:11:31.920
Everybody ignores what they say.

s115
00:11:31.920 --> 00:11:35.800
And these guys just went ahead and have shipped tool calls.

s116
00:11:35.800 --> 00:11:40.120
They just, yeah, just just do it.

s117
00:11:41.640 --> 00:11:45.680
Now, let's go back to like this is AI engineering conference.

s118
00:11:45.680 --> 00:11:50.840
So, let's look at what is the difference in the signature of LLMs when they add the tool calls.

s119
00:11:50.840 --> 00:12:00.880
And it's just that little IO there, and of course it messes up the the formatting of of the the um uh signature.

s120
00:12:00.880 --> 00:12:08.240
But, if you look at the picture, there what you show, now suddenly Claude goes from like a nice puppy to a dangerous thing.

s121
00:12:08.240 --> 00:12:10.600
Look, it has all these dangerous tools.

s122
00:12:10.600 --> 00:12:12.280
And now it becomes scary, right?

s123
00:12:12.280 --> 00:12:17.000
I've never seen anything scarier than an LLM with tool calls.

s124
00:12:17.000 --> 00:12:23.960
Um now, if you look at this, this is like a like a small step for a type, but a giant leap for chaos.

s125
00:12:23.960 --> 00:12:25.520
Why is that?

s126
00:12:25.520 --> 00:12:35.000
And that is because this IO says that in order to compute the answer, the agent has to go through the agentic loop, and it's doing side effects.

s127
00:12:35.000 --> 00:12:42.320
So, while it's producing the answer, it might empty your bank account, it might delete your files, and then it gives you a safe answer.

s128
00:12:42.320 --> 00:12:46.960
But, who cares about the safe answer when all my files are gone?

s129
00:12:46.960 --> 00:12:47.480
Right?

s130
00:12:47.480 --> 00:12:51.400
So, that's why I say it, it's a giant leap for for chaos.

s131
00:12:51.400 --> 00:12:55.280
Um again, sorry, this is an engineering conference.

s132
00:12:55.280 --> 00:12:57.480
Let's look at this type IO.

s133
00:12:57.480 --> 00:13:02.839
And you don't have to understand it, but just see that there's a type there called real world.

s134
00:13:02.839 --> 00:13:06.960
Yes, Lean, this is a direct thing, has a type called real world.

s135
00:13:06.960 --> 00:13:08.120
And why is that?

s136
00:13:08.120 --> 00:13:12.360
Because something of type IO will mutate the real world.

s137
00:13:12.360 --> 00:13:19.480
So, it warns you, don't use this because it can make irreversible side effects.

s138
00:13:19.480 --> 00:13:21.729
Um like deleting your files.

s139
00:13:21.729 --> 00:13:21.960
[snorts]

s140
00:13:21.960 --> 00:13:30.440
So, Solomon Heikes um last year this conference called an AI agent, an LLM that's wrecking its environment in a loop.

s141
00:13:30.440 --> 00:13:31.680
And I think he's a hero.

s142
00:13:31.680 --> 00:13:39.680
I don't know if Solomon is here this year, but I think he should he deserves uh deserves a round of applause.

s143
00:13:39.680 --> 00:13:45.840
Um because I think this is the right definition of an AI agent.

s144
00:13:45.840 --> 00:13:53.360
Um by the way, this was one of the pictures that I had trouble to generate because it it clearly depicts violence.

s145
00:13:53.360 --> 00:13:55.600
And so it's a kind of an unsafe thing, right?

s146
00:13:55.600 --> 00:13:58.520
I have a picture that depicts violence.

s147
00:13:58.520 --> 00:14:00.680
Um so are we doomed?

s148
00:14:00.680 --> 00:14:03.640
Well, our agents have access to private data.

s149
00:14:03.640 --> 00:14:07.160
They have untrusted content like the prompt injections.

s150
00:14:07.160 --> 00:14:08.800
And now we give them tools.

s151
00:14:08.800 --> 00:14:12.360
Simon Willison calls this the lethal trifecta.

s152
00:14:12.360 --> 00:14:14.160
Um what can we do about this?

s153
00:14:14.160 --> 00:14:24.520
Well, um I don't know if you've seen the Dutch soccer fans, they have the famous march where they say to the left left left or to the left left left to the right right right.

s154
00:14:24.520 --> 00:14:28.600
This is actually the secret to solving this problem.

s155
00:14:28.600 --> 00:14:34.320
The Dutch team got eliminated yesterday, so you have to see me do the dance.

s156
00:14:34.320 --> 00:14:40.839
Um but all that we're doing is we're pushing this IO to the right to the right.

s157
00:14:40.839 --> 00:14:46.000
And what you now see is that the tool belt of Claude goes to the left to the left.

s158
00:14:46.000 --> 00:14:49.080
And suddenly Claude is a nice puppy again.

s159
00:14:49.080 --> 00:14:56.920
Because instead of executing the agentic loop, it creates a plan and says here is a plan to do the agentic loop.

s160
00:14:56.920 --> 00:15:00.360
And now Bernie will take that plan and will execute it.

s161
00:15:00.360 --> 00:15:02.680
And we all trust Bernie, right?

s162
00:15:02.680 --> 00:15:04.760
Bernie is a good guy.

s163
00:15:04.760 --> 00:15:06.200
All right.

s164
00:15:06.200 --> 00:15:08.440
So just to kind of like show it here.

s165
00:15:08.440 --> 00:15:13.960
So in some sense what we're doing, we're air gapping the agentic loop from the agent.

s166
00:15:13.960 --> 00:15:17.200
So we don't let the agent run the agentic loop.

s167
00:15:17.200 --> 00:15:22.080
Before the agent run it, we want to be able to check it.

s168
00:15:22.080 --> 00:15:23.360
All right.

s169
00:15:23.360 --> 00:15:31.840
Now, the problem is that if you get the value of type IO of A, um that's a really a black box.

s170
00:15:31.840 --> 00:15:35.440
And the Lean manual says that if it's a black box, you cannot reason about it.

s171
00:15:35.440 --> 00:15:40.800
So, even though Claude now gives us this plan, there's we cannot look into this plan.

s172
00:15:40.800 --> 00:15:42.600
Lean doesn't allow us to do it.

s173
00:15:42.600 --> 00:15:44.280
By the way, this is another picture, right?

s174
00:15:44.280 --> 00:15:49.480
That's that's promotes drugs use and the model let me do it.

s175
00:15:49.480 --> 00:15:50.640
I'm a good hacker, yeah.

s176
00:15:50.640 --> 00:15:53.920
I can just make it do forbidden pictures.

s177
00:15:53.920 --> 00:16:03.040
Um So, if we look at the Lean again, what you see here is that the model now computes an answer, but it doesn't compute the answer, right?

s178
00:16:03.040 --> 00:16:05.840
It creates an an IO of answer.

s179
00:16:05.840 --> 00:16:14.480
So, this is a plan to generate the answer, and then it creates a proof that this um that that plan is safe.

s180
00:16:14.480 --> 00:16:21.280
And the the nice thing is here that you can get at that proof without having to run the agentic loop.

s181
00:16:21.280 --> 00:16:27.320
But, unfortunately, as I said, like this proof, if it's like something of type IO, it's useless.

s182
00:16:27.320 --> 00:16:29.560
Ah, What can we do about that?

s183
00:16:29.560 --> 00:16:35.880
So, I keep like moving you guys forward, and then we never get to the final answer.

s184
00:16:35.880 --> 00:16:45.720
But, there's one last trick, and you see the the researchers here are becoming more much more sophisticated instead of the flat 2D ones in the past.

s185
00:16:45.720 --> 00:16:48.000
Now, they're like real people.

s186
00:16:48.000 --> 00:17:01.000
Um And what is better than creating a plan of type IO of A is creating a program that represents an expression of type IO of A. Ooh, that sounds very meta,

s187
00:17:01.000 --> 00:17:01.680
right?

s188
00:17:01.680 --> 00:17:05.199
Um Not meta in terms of meta.

s189
00:17:05.199 --> 00:17:10.760
I don't think they're very meta, but um meta in the terms of like you know, like meta.

s190
00:17:10.760 --> 00:17:12.800
You You know, you know what I mean.

s191
00:17:12.800 --> 00:17:21.480
Um And again, it's a small step for a signature, but a giant leap for safety.

s192
00:17:21.480 --> 00:17:27.199
Because now the model returns an expression, a program that represents a computation.

s193
00:17:27.199 --> 00:17:32.960
If you know link or C#, you will recognize that this is one of the tricks that I always use.

s194
00:17:32.960 --> 00:17:36.760
If you know Lisp, this is of course second nature for you.

s195
00:17:36.760 --> 00:17:41.280
I cannot have like you know, have a talk without talking about monads.

s196
00:17:41.280 --> 00:17:44.440
So, if you ask yourself, what is this expression thing?

s197
00:17:44.440 --> 00:17:48.880
Well, that's just a monad, but it's not just a monad, it's a free monad.

s198
00:17:48.880 --> 00:17:50.280
What is a free monad?

s199
00:17:50.280 --> 00:17:53.320
It's a monad that loves tie dyes.

s200
00:17:53.320 --> 00:18:06.040
Um And now if you look at the the signature of the the property to prove that something is safe, you see that it takes an expression of a computation

s201
00:18:06.040 --> 00:18:07.680
that returns an answer.

s202
00:18:07.680 --> 00:18:17.040
Um and if you have taken any compiler course in college, you know that it's trivial to do data flow analysis, type checking, and so on on programs.

s203
00:18:17.040 --> 00:18:17.240
Right?

s204
00:18:17.240 --> 00:18:19.320
So, now we're safe, we're home safe.

s205
00:18:19.320 --> 00:18:30.240
And Jeff Huntley wanted to remind you that we can solve the drive factor problem just by doing taint analysis on these expression on these programs.

s206
00:18:30.240 --> 00:18:40.240
Okay, this is the last code I will show you because I'm running out of time, but just want to show you here that, you know, you now have a simple inductive recursive interpreter

s207
00:18:40.240 --> 00:18:43.760
for this language and you have a simple inductive proof.

s208
00:18:43.760 --> 00:18:47.040
And the models can generate these proofs.

s209
00:18:47.040 --> 00:19:00.040
So, to um recapitulate like the summarize, what we did is we went from unhinged LLMs that were like you know, could give bad answers to ones that were aligned,

s210
00:19:00.040 --> 00:19:17.000
then we saw how tools wrecked it, then we solved that by deferring execution, so by air gapping the LLM from the tools, and then the real solution was to rewrite the plan into a program and a program that we could prove to be safe.

s211
00:19:17.000 --> 00:19:19.840
Now, you would say, "Eric, oh, you're a genius."

s212
00:19:19.840 --> 00:19:22.880
No, I'm my brain is the size of a peanut.

s213
00:19:22.880 --> 00:19:30.120
This is something that's called proof-carrying code and it was invented by academics in the 1990s and I'm just stealing it.

s214
00:19:30.120 --> 00:19:31.800
Um, all right.

s215
00:19:31.800 --> 00:19:36.320
At the higher level, if you didn't understand the code, three points.

s216
00:19:36.320 --> 00:19:45.560
Agents are dangerous until proven safe, so you should never ever let your agents do something unless you can absolutely prove that it's safe.

s217
00:19:45.560 --> 00:19:53.000
And the language that this agents generated was not designed like normal users don't understand free monads.

s218
00:19:53.000 --> 00:19:54.000
Doesn't matter.

s219
00:19:54.000 --> 00:19:56.240
It's a machine that consumes it.

s220
00:19:56.240 --> 00:19:57.680
It's a machine that generates it.

s221
00:19:57.680 --> 00:19:58.680
It's a machine that proves it.

s222
00:19:58.680 --> 00:20:05.760
So, we should stop designing languages for humans and it's all basic, only requires programming 101.

s223
00:20:05.760 --> 00:20:07.560
Um, there we go.

s224
00:20:07.560 --> 00:20:08.720
All right.

s225
00:20:08.720 --> 00:20:10.000
That's it.

s226
00:20:10.000 --> 00:20:12.200
Um, the end of the story.

s227
00:20:12.200 --> 00:20:19.000
If you're curious to play with this, a bunch of academics, in particular Nada Amin from Harvard, have implemented this.

s228
00:20:19.000 --> 00:20:21.240
It's it's there on GitHub.

s229
00:20:21.240 --> 00:20:25.480
It uses a slightly different language than what I use.

s230
00:20:25.480 --> 00:20:30.240
It uses also a slightly different language than free monads, but the idea is the same.

s231
00:20:30.240 --> 00:20:31.360
The language doesn't matter.

s232
00:20:31.360 --> 00:20:34.760
It's it's the the principle that matters.

s233
00:20:34.760 --> 00:20:53.720
So, hopefully, you've learned tonight that it is actually possible to have mathematically proven safe agentic compute and it only requires very elementary type systems and programming language machinery.

s234
00:20:53.720 --> 00:20:56.120
Thank you so much.

s235
00:21:09.404 --> 00:21:11.404
[music]

s236
00:21:12.520 --> 00:21:14.520
Oh.