1
00:00:00,180 --> 00:00:04,500
And the output I want from this, the output I want from this is the ability to write,

2
00:00:04,620 --> 00:00:11,400
in some cases, formal proofs that a program I have written in this language has

3
00:00:11,400 --> 00:00:16,780
certain properties. I'm going to write a formal proof that this million lines of policy

4
00:00:16,780 --> 00:00:22,720
code will never allow me to spend over $1 ,000 on my credit card.

5
00:00:23,400 --> 00:00:29,340
It's a hard thing to do for languages in general, but if you design a language for analyzability,

6
00:00:29,600 --> 00:00:30,180
it's easier.