WEBVTT Kind: captions Language: en 00:00:15.529 --> 00:00:18.439 align:start position:0% well<00:00:16.529> thank<00:00:16.740> you<00:00:16.830> very<00:00:17.039> much<00:00:17.250> it's<00:00:18.060> a<00:00:18.180> pleasure 00:00:18.439 --> 00:00:18.449 align:start position:0% well thank you very much it's a pleasure 00:00:18.449 --> 00:00:20.990 align:start position:0% well thank you very much it's a pleasure to<00:00:18.600> be<00:00:18.690> here<00:00:18.990> and<00:00:19.529> grant<00:00:19.800> passmore<00:00:20.310> in<00:00:20.490> my 00:00:20.990 --> 00:00:21.000 align:start position:0% to be here and grant passmore in my 00:00:21.000 --> 00:00:23.269 align:start position:0% to be here and grant passmore in my co-founder<00:00:21.449> dennis<00:00:21.689> ignite<00:00:21.930> ovitch<00:00:22.189> here<00:00:23.189> in 00:00:23.269 --> 00:00:23.279 align:start position:0% co-founder dennis ignite ovitch here in 00:00:23.279 --> 00:00:25.670 align:start position:0% co-founder dennis ignite ovitch here in the<00:00:23.340> audience<00:00:23.460> thank<00:00:24.390> you<00:00:24.480> to<00:00:24.630> a<00:00:24.660> italic<00:00:25.500> for 00:00:25.670 --> 00:00:25.680 align:start position:0% the audience thank you to a italic for 00:00:25.680 --> 00:00:27.890 align:start position:0% the audience thank you to a italic for the<00:00:25.800> invitation<00:00:26.160> so<00:00:27.060> we're<00:00:27.210> going<00:00:27.390> to<00:00:27.539> talk<00:00:27.750> to 00:00:27.890 --> 00:00:27.900 align:start position:0% the invitation so we're going to talk to 00:00:27.900 --> 00:00:29.830 align:start position:0% the invitation so we're going to talk to you<00:00:27.990> today<00:00:28.199> about<00:00:28.349> our<00:00:28.830> formal<00:00:29.640> verification 00:00:29.830 --> 00:00:29.840 align:start position:0% you today about our formal verification 00:00:29.840 --> 00:00:32.150 align:start position:0% you today about our formal verification platform<00:00:30.840> and<00:00:31.019> mandra<00:00:31.439> and<00:00:31.619> a<00:00:32.009> particular 00:00:32.150 --> 00:00:32.160 align:start position:0% platform and mandra and a particular 00:00:32.160 --> 00:00:33.680 align:start position:0% platform and mandra and a particular something<00:00:32.880> we're<00:00:33.000> calling<00:00:33.030> a<00:00:33.360> mantra 00:00:33.680 --> 00:00:33.690 align:start position:0% something we're calling a mantra 00:00:33.690 --> 00:00:35.660 align:start position:0% something we're calling a mantra contracts<00:00:34.200> which<00:00:34.559> is<00:00:34.739> the<00:00:34.890> application<00:00:35.010> of<00:00:35.579> a 00:00:35.660 --> 00:00:35.670 align:start position:0% contracts which is the application of a 00:00:35.670 --> 00:00:39.139 align:start position:0% contracts which is the application of a mantra<00:00:36.090> to<00:00:36.840> etherium<00:00:37.739> smart<00:00:38.040> contracts<00:00:38.489> both 00:00:39.139 --> 00:00:39.149 align:start position:0% mantra to etherium smart contracts both 00:00:39.149 --> 00:00:41.990 align:start position:0% mantra to etherium smart contracts both to<00:00:39.360> analyze<00:00:39.809> smart<00:00:40.140> contracts<00:00:40.790> reason<00:00:41.790> about 00:00:41.990 --> 00:00:42.000 align:start position:0% to analyze smart contracts reason about 00:00:42.000 --> 00:00:44.000 align:start position:0% to analyze smart contracts reason about them<00:00:42.239> be<00:00:42.660> able<00:00:42.870> to<00:00:42.960> prove<00:00:43.140> properties<00:00:43.680> of<00:00:43.829> them 00:00:44.000 --> 00:00:44.010 align:start position:0% them be able to prove properties of them 00:00:44.010 --> 00:00:46.970 align:start position:0% them be able to prove properties of them compute<00:00:44.910> proofs<00:00:45.149> and<00:00:45.360> counter<00:00:45.600> examples<00:00:46.020> and 00:00:46.970 --> 00:00:46.980 align:start position:0% compute proofs and counter examples and 00:00:46.980 --> 00:00:48.770 align:start position:0% compute proofs and counter examples and then<00:00:47.100> on<00:00:47.309> top<00:00:47.520> of<00:00:47.579> that<00:00:47.730> to<00:00:48.090> actually<00:00:48.239> do<00:00:48.570> risk 00:00:48.770 --> 00:00:48.780 align:start position:0% then on top of that to actually do risk 00:00:48.780 --> 00:00:50.389 align:start position:0% then on top of that to actually do risk management<00:00:49.320> so<00:00:49.590> I'll<00:00:49.710> tell<00:00:49.920> you<00:00:50.010> what<00:00:50.129> I<00:00:50.160> mean 00:00:50.389 --> 00:00:50.399 align:start position:0% management so I'll tell you what I mean 00:00:50.399 --> 00:00:52.400 align:start position:0% management so I'll tell you what I mean but<00:00:50.910> for<00:00:51.090> those<00:00:51.210> and<00:00:51.480> investment<00:00:51.899> banking<00:00:52.140> we 00:00:52.400 --> 00:00:52.410 align:start position:0% but for those and investment banking we 00:00:52.410 --> 00:00:55.189 align:start position:0% but for those and investment banking we mean<00:00:52.590> you<00:00:52.770> no<00:00:52.860> compute<00:00:53.789> Greeks<00:00:54.030> and<00:00:54.270> so<00:00:54.390> on<00:00:54.510> so 00:00:55.189 --> 00:00:55.199 align:start position:0% mean you no compute Greeks and so on so 00:00:55.199 --> 00:00:57.500 align:start position:0% mean you no compute Greeks and so on so let<00:00:55.949> me<00:00:56.129> start<00:00:56.190> with<00:00:56.460> a<00:00:56.610> video<00:00:56.940> that<00:00:57.000> gives<00:00:57.329> you 00:00:57.500 --> 00:00:57.510 align:start position:0% let me start with a video that gives you 00:00:57.510 --> 00:00:59.119 align:start position:0% let me start with a video that gives you a<00:00:57.539> background<00:00:58.050> on<00:00:58.350> what<00:00:58.530> we're<00:00:58.680> doing<00:00:58.710> at 00:00:59.119 --> 00:00:59.129 align:start position:0% a background on what we're doing at 00:00:59.129 --> 00:01:02.950 align:start position:0% a background on what we're doing at aesthetic<00:00:59.730> integration<00:01:00.440> see<00:01:01.440> if<00:01:01.500> the<00:01:01.649> sound 00:01:02.950 --> 00:01:02.960 align:start position:0% aesthetic integration see if the sound 00:01:02.960 --> 00:01:21.630 align:start position:0% aesthetic integration see if the sound I'll<00:01:03.960> start<00:01:04.260> it<00:01:04.320> over<00:01:04.379> here<00:01:04.619> we<00:01:04.710> go 00:01:21.630 --> 00:01:21.640 align:start position:0% 00:01:21.640 --> 00:01:29.880 align:start position:0% yes<00:01:23.320> thought<00:01:24.320> was<00:01:24.619> the<00:01:24.799> best<00:01:26.350> of<00:01:28.420> an<00:01:29.420> issue 00:01:29.880 --> 00:01:29.890 align:start position:0% yes thought was the best of an issue 00:01:29.890 --> 00:01:32.300 align:start position:0% yes thought was the best of an issue Paris 00:01:32.300 --> 00:01:32.310 align:start position:0% Paris 00:01:32.310 --> 00:03:04.430 align:start position:0% Paris I<00:02:00.259> made<00:02:01.310> it 00:03:04.430 --> 00:03:04.440 align:start position:0% 00:03:04.440 --> 00:03:09.150 align:start position:0% alright<00:03:05.670> so<00:03:06.670> that<00:03:07.210> gave<00:03:07.420> you<00:03:07.630> a<00:03:08.010> bit<00:03:09.010> of<00:03:09.040> an 00:03:09.150 --> 00:03:09.160 align:start position:0% alright so that gave you a bit of an 00:03:09.160 --> 00:03:11.910 align:start position:0% alright so that gave you a bit of an overview<00:03:09.490> of<00:03:09.700> what<00:03:10.600> we're<00:03:10.750> doing<00:03:11.050> at 00:03:11.910 --> 00:03:11.920 align:start position:0% overview of what we're doing at 00:03:11.920 --> 00:03:13.500 align:start position:0% overview of what we're doing at aesthetic<00:03:12.310> integration<00:03:12.760> the<00:03:12.880> big<00:03:13.060> idea<00:03:13.240> is 00:03:13.500 --> 00:03:13.510 align:start position:0% aesthetic integration the big idea is 00:03:13.510 --> 00:03:15.360 align:start position:0% aesthetic integration the big idea is we're<00:03:13.900> bringing<00:03:14.200> the<00:03:14.440> hard<00:03:14.650> science<00:03:15.130> of 00:03:15.360 --> 00:03:15.370 align:start position:0% we're bringing the hard science of 00:03:15.370 --> 00:03:17.850 align:start position:0% we're bringing the hard science of formal<00:03:15.940> verification<00:03:16.710> techniques<00:03:17.710> that<00:03:17.800> are 00:03:17.850 --> 00:03:17.860 align:start position:0% formal verification techniques that are 00:03:17.860 --> 00:03:19.680 align:start position:0% formal verification techniques that are relied<00:03:18.160> upon<00:03:18.340> already<00:03:18.910> in<00:03:19.150> safety-critical 00:03:19.680 --> 00:03:19.690 align:start position:0% relied upon already in safety-critical 00:03:19.690 --> 00:03:22.260 align:start position:0% relied upon already in safety-critical industries<00:03:20.470> like<00:03:20.770> avionics<00:03:21.430> and<00:03:21.610> hardware 00:03:22.260 --> 00:03:22.270 align:start position:0% industries like avionics and hardware 00:03:22.270 --> 00:03:25.860 align:start position:0% industries like avionics and hardware design<00:03:23.070> finally<00:03:24.070> to<00:03:24.400> finance<00:03:24.910> so<00:03:25.660> that 00:03:25.860 --> 00:03:25.870 align:start position:0% design finally to finance so that 00:03:25.870 --> 00:03:28.140 align:start position:0% design finally to finance so that financial<00:03:26.380> algorithms<00:03:26.860> things<00:03:27.580> like<00:03:27.820> dark 00:03:28.140 --> 00:03:28.150 align:start position:0% financial algorithms things like dark 00:03:28.150 --> 00:03:30.810 align:start position:0% financial algorithms things like dark pool<00:03:28.360> matching<00:03:28.750> logics<00:03:29.310> exchange<00:03:30.310> matching 00:03:30.810 --> 00:03:30.820 align:start position:0% pool matching logics exchange matching 00:03:30.820 --> 00:03:33.360 align:start position:0% pool matching logics exchange matching logics<00:03:31.230> market<00:03:32.230> making<00:03:32.410> algorithm<00:03:33.010> smart 00:03:33.360 --> 00:03:33.370 align:start position:0% logics market making algorithm smart 00:03:33.370 --> 00:03:36.090 align:start position:0% logics market making algorithm smart order<00:03:33.610> routers<00:03:33.970> the<00:03:34.360> type<00:03:34.600> of<00:03:34.770> algorithm<00:03:35.770> that 00:03:36.090 --> 00:03:36.100 align:start position:0% order routers the type of algorithm that 00:03:36.100 --> 00:03:37.230 align:start position:0% order routers the type of algorithm that is<00:03:36.250> really<00:03:36.460> at<00:03:36.550> the<00:03:36.640> heart<00:03:36.670> of<00:03:36.880> our<00:03:37.000> global 00:03:37.230 --> 00:03:37.240 align:start position:0% is really at the heart of our global 00:03:37.240 --> 00:03:38.940 align:start position:0% is really at the heart of our global financial<00:03:37.630> infrastructure<00:03:37.900> so<00:03:38.740> that<00:03:38.770> they 00:03:38.940 --> 00:03:38.950 align:start position:0% financial infrastructure so that they 00:03:38.950 --> 00:03:40.920 align:start position:0% financial infrastructure so that they can<00:03:39.100> actually<00:03:39.250> be<00:03:39.550> analyzed<00:03:40.030> rigorously<00:03:40.660> and 00:03:40.920 --> 00:03:40.930 align:start position:0% can actually be analyzed rigorously and 00:03:40.930 --> 00:03:43.140 align:start position:0% can actually be analyzed rigorously and reasoned<00:03:41.770> about<00:03:41.950> so<00:03:42.790> a<00:03:42.820> bit<00:03:43.000> of<00:03:43.030> our 00:03:43.140 --> 00:03:43.150 align:start position:0% reasoned about so a bit of our 00:03:43.150 --> 00:03:46.170 align:start position:0% reasoned about so a bit of our background<00:03:43.630> so<00:03:43.900> Dennis<00:03:44.850> formerly<00:03:45.850> was<00:03:46.030> the 00:03:46.170 --> 00:03:46.180 align:start position:0% background so Dennis formerly was the 00:03:46.180 --> 00:03:47.760 align:start position:0% background so Dennis formerly was the head<00:03:46.330> of<00:03:46.420> the<00:03:46.540> central<00:03:46.780> risk<00:03:47.050> trading<00:03:47.410> desk<00:03:47.620> at 00:03:47.760 --> 00:03:47.770 align:start position:0% head of the central risk trading desk at 00:03:47.770 --> 00:03:51.120 align:start position:0% head of the central risk trading desk at Deutsche<00:03:48.390> roughly<00:03:49.390> I<00:03:49.630> believe<00:03:50.290> nine<00:03:50.530> years<00:03:50.860> at 00:03:51.120 --> 00:03:51.130 align:start position:0% Deutsche roughly I believe nine years at 00:03:51.130 --> 00:03:53.010 align:start position:0% Deutsche roughly I believe nine years at Deutsche<00:03:51.459> by<00:03:52.000> the<00:03:52.060> way<00:03:52.180> we<00:03:52.330> were<00:03:52.450> undergrad 00:03:53.010 --> 00:03:53.020 align:start position:0% Deutsche by the way we were undergrad 00:03:53.020 --> 00:03:56.340 align:start position:0% Deutsche by the way we were undergrad roommates<00:03:53.380> in<00:03:53.620> Texas<00:03:54.250> and<00:03:54.600> then<00:03:55.600> as<00:03:55.810> Dennis 00:03:56.340 --> 00:03:56.350 align:start position:0% roommates in Texas and then as Dennis 00:03:56.350 --> 00:03:58.280 align:start position:0% roommates in Texas and then as Dennis went<00:03:56.560> to<00:03:56.620> Wall<00:03:56.770> Street<00:03:56.800> I<00:03:57.190> went<00:03:57.490> to<00:03:57.550> academia 00:03:58.280 --> 00:03:58.290 align:start position:0% went to Wall Street I went to academia 00:03:58.290 --> 00:04:01.410 align:start position:0% went to Wall Street I went to academia did<00:03:59.290> my<00:03:59.410> PhD<00:03:59.470> in<00:04:00.070> formal<00:04:00.580> verification<00:04:00.700> in 00:04:01.410 --> 00:04:01.420 align:start position:0% did my PhD in formal verification in 00:04:01.420 --> 00:04:04.260 align:start position:0% did my PhD in formal verification in particular<00:04:02.220> the<00:04:03.220> real<00:04:03.850> loud<00:04:04.000> to<00:04:04.120> break 00:04:04.260 --> 00:04:04.270 align:start position:0% particular the real loud to break 00:04:04.270 --> 00:04:06.000 align:start position:0% particular the real loud to break geometry<00:04:04.870> for<00:04:05.080> reasoning<00:04:05.440> about<00:04:05.590> autopilot 00:04:06.000 --> 00:04:06.010 align:start position:0% geometry for reasoning about autopilot 00:04:06.010 --> 00:04:07.590 align:start position:0% geometry for reasoning about autopilot algorithms<00:04:06.610> and<00:04:06.850> being<00:04:07.090> able<00:04:07.270> to<00:04:07.360> prove 00:04:07.590 --> 00:04:07.600 align:start position:0% algorithms and being able to prove 00:04:07.600 --> 00:04:09.600 align:start position:0% algorithms and being able to prove safety<00:04:08.200> properties<00:04:08.650> of<00:04:09.190> autopilot 00:04:09.600 --> 00:04:09.610 align:start position:0% safety properties of autopilot 00:04:09.610 --> 00:04:11.820 align:start position:0% safety properties of autopilot algorithms<00:04:10.330> in<00:04:10.630> avionics<00:04:11.080> in<00:04:11.560> now<00:04:11.709> and 00:04:11.820 --> 00:04:11.830 align:start position:0% algorithms in avionics in now and 00:04:11.830 --> 00:04:15.360 align:start position:0% algorithms in avionics in now and self-driving<00:04:12.280> cars<00:04:12.959> and<00:04:13.959> ended<00:04:14.500> up<00:04:14.560> as<00:04:15.340> a 00:04:15.360 --> 00:04:15.370 align:start position:0% self-driving cars and ended up as a 00:04:15.370 --> 00:04:16.949 align:start position:0% self-driving cars and ended up as a postdoc<00:04:15.730> at<00:04:15.880> Cambridge<00:04:16.239> well<00:04:16.570> Dennis<00:04:16.780> was 00:04:16.949 --> 00:04:16.959 align:start position:0% postdoc at Cambridge well Dennis was 00:04:16.959 --> 00:04:19.650 align:start position:0% postdoc at Cambridge well Dennis was working<00:04:17.260> at<00:04:17.350> Deutsche<00:04:17.709> and<00:04:18.209> we<00:04:19.209> realized<00:04:19.510> we 00:04:19.650 --> 00:04:19.660 align:start position:0% working at Deutsche and we realized we 00:04:19.660 --> 00:04:21.449 align:start position:0% working at Deutsche and we realized we were<00:04:19.750> working<00:04:19.930> in<00:04:20.200> many<00:04:20.350> ways<00:04:20.530> on<00:04:20.799> some<00:04:21.280> of<00:04:21.370> the 00:04:21.449 --> 00:04:21.459 align:start position:0% were working in many ways on some of the 00:04:21.459 --> 00:04:23.040 align:start position:0% were working in many ways on some of the same<00:04:21.640> problems<00:04:22.090> he<00:04:22.270> had<00:04:22.360> very<00:04:22.570> complex 00:04:23.040 --> 00:04:23.050 align:start position:0% same problems he had very complex 00:04:23.050 --> 00:04:26.130 align:start position:0% same problems he had very complex trading<00:04:23.500> algorithms<00:04:23.620> that<00:04:25.140> constantly 00:04:26.130 --> 00:04:26.140 align:start position:0% trading algorithms that constantly 00:04:26.140 --> 00:04:27.990 align:start position:0% trading algorithms that constantly everyone<00:04:26.890> was<00:04:27.040> worried<00:04:27.370> you<00:04:27.669> know<00:04:27.700> if<00:04:27.880> we 00:04:27.990 --> 00:04:28.000 align:start position:0% everyone was worried you know if we 00:04:28.000 --> 00:04:30.330 align:start position:0% everyone was worried you know if we commit<00:04:28.240> a<00:04:28.300> line<00:04:28.480> of<00:04:28.600> code<00:04:28.870> is<00:04:29.110> this<00:04:29.710> change<00:04:30.040> all 00:04:30.330 --> 00:04:30.340 align:start position:0% commit a line of code is this change all 00:04:30.340 --> 00:04:31.920 align:start position:0% commit a line of code is this change all of<00:04:30.370> a<00:04:30.460> sudden<00:04:30.669> going<00:04:30.880> to<00:04:30.940> cause<00:04:31.150> us<00:04:31.390> to<00:04:31.570> violate 00:04:31.920 --> 00:04:31.930 align:start position:0% of a sudden going to cause us to violate 00:04:31.930 --> 00:04:34.050 align:start position:0% of a sudden going to cause us to violate a<00:04:31.960> regulation<00:04:32.560> and<00:04:32.710> it's<00:04:33.430> very<00:04:33.640> hard<00:04:33.850> to<00:04:33.910> get 00:04:34.050 --> 00:04:34.060 align:start position:0% a regulation and it's very hard to get 00:04:34.060 --> 00:04:35.760 align:start position:0% a regulation and it's very hard to get right<00:04:34.210> if<00:04:34.419> you<00:04:34.510> think<00:04:34.720> of<00:04:34.900> modern<00:04:35.440> market 00:04:35.760 --> 00:04:35.770 align:start position:0% right if you think of modern market 00:04:35.770 --> 00:04:37.380 align:start position:0% right if you think of modern market microstructure<00:04:36.120> something<00:04:37.120> like<00:04:37.240> in 00:04:37.380 --> 00:04:37.390 align:start position:0% microstructure something like in 00:04:37.390 --> 00:04:39.210 align:start position:0% microstructure something like in exchange<00:04:37.840> trading<00:04:38.470> than<00:04:38.620> you<00:04:38.740> in<00:04:38.860> the<00:04:38.950> US<00:04:39.190> for 00:04:39.210 --> 00:04:39.220 align:start position:0% exchange trading than you in the US for 00:04:39.220 --> 00:04:42.240 align:start position:0% exchange trading than you in the US for instance<00:04:39.730> it<00:04:40.240> may<00:04:40.390> have<00:04:40.540> upwards<00:04:40.720> of<00:04:41.050> 20<00:04:41.410> 30<00:04:41.860> 40 00:04:42.240 --> 00:04:42.250 align:start position:0% instance it may have upwards of 20 30 40 00:04:42.250 --> 00:04:44.040 align:start position:0% instance it may have upwards of 20 30 40 different<00:04:42.460> order<00:04:42.820> types<00:04:43.030> in<00:04:43.660> each<00:04:43.810> of<00:04:43.930> those 00:04:44.040 --> 00:04:44.050 align:start position:0% different order types in each of those 00:04:44.050 --> 00:04:46.350 align:start position:0% different order types in each of those order<00:04:44.320> types<00:04:44.700> effectively<00:04:45.700> it's<00:04:45.880> a<00:04:45.970> way<00:04:46.330> of 00:04:46.350 --> 00:04:46.360 align:start position:0% order types effectively it's a way of 00:04:46.360 --> 00:04:48.120 align:start position:0% order types effectively it's a way of packaging<00:04:46.750> risk<00:04:47.110> it's<00:04:47.710> a<00:04:47.800> programming 00:04:48.120 --> 00:04:48.130 align:start position:0% packaging risk it's a programming 00:04:48.130 --> 00:04:50.159 align:start position:0% packaging risk it's a programming language<00:04:48.250> and<00:04:48.730> as<00:04:49.270> you<00:04:49.390> introduce<00:04:49.570> new<00:04:49.900> order 00:04:50.159 --> 00:04:50.169 align:start position:0% language and as you introduce new order 00:04:50.169 --> 00:04:52.170 align:start position:0% language and as you introduce new order types<00:04:50.380> it's<00:04:50.740> very<00:04:51.100> difficult<00:04:51.310> by<00:04:51.669> hand<00:04:52.000> to 00:04:52.170 --> 00:04:52.180 align:start position:0% types it's very difficult by hand to 00:04:52.180 --> 00:04:54.170 align:start position:0% types it's very difficult by hand to understand<00:04:52.630> what<00:04:52.810> can<00:04:52.930> possibly<00:04:53.110> go<00:04:53.410> wrong 00:04:54.170 --> 00:04:54.180 align:start position:0% understand what can possibly go wrong 00:04:54.180 --> 00:04:57.380 align:start position:0% understand what can possibly go wrong so<00:04:55.180> when<00:04:55.360> it<00:04:55.450> comes<00:04:55.600> to<00:04:55.930> smart<00:04:56.740> contracts 00:04:57.380 --> 00:04:57.390 align:start position:0% so when it comes to smart contracts 00:04:57.390 --> 00:05:00.780 align:start position:0% so when it comes to smart contracts really<00:04:58.390> we<00:04:58.870> have<00:04:59.020> the<00:04:59.170> same<00:04:59.200> issues<00:04:59.650> so<00:05:00.520> if<00:05:00.700> i 00:05:00.780 --> 00:05:00.790 align:start position:0% really we have the same issues so if i 00:05:00.790 --> 00:05:02.640 align:start position:0% really we have the same issues so if i come<00:05:01.030> to<00:05:01.060> you<00:05:01.240> and<00:05:01.330> say<00:05:01.390> look<00:05:01.690> I<00:05:01.840> promise<00:05:02.350> you 00:05:02.640 --> 00:05:02.650 align:start position:0% come to you and say look I promise you 00:05:02.650 --> 00:05:04.500 align:start position:0% come to you and say look I promise you know<00:05:02.770> this<00:05:02.920> piece<00:05:03.130> of<00:05:03.280> bytecode<00:05:03.730> really 00:05:04.500 --> 00:05:04.510 align:start position:0% know this piece of bytecode really 00:05:04.510 --> 00:05:06.480 align:start position:0% know this piece of bytecode really implements<00:05:05.080> fair<00:05:05.260> escrow<00:05:05.680> please<00:05:06.130> send<00:05:06.430> me 00:05:06.480 --> 00:05:06.490 align:start position:0% implements fair escrow please send me 00:05:06.490 --> 00:05:09.450 align:start position:0% implements fair escrow please send me your<00:05:06.520> assets<00:05:06.970> how<00:05:07.750> do<00:05:07.810> you<00:05:07.960> know<00:05:08.280> likewise<00:05:09.280> if 00:05:09.450 --> 00:05:09.460 align:start position:0% your assets how do you know likewise if 00:05:09.460 --> 00:05:11.610 align:start position:0% your assets how do you know likewise if I<00:05:09.550> say<00:05:09.760> I<00:05:10.030> promise<00:05:10.540> this<00:05:10.720> implements<00:05:11.230> a<00:05:11.320> swap 00:05:11.610 --> 00:05:11.620 align:start position:0% I say I promise this implements a swap 00:05:11.620 --> 00:05:14.550 align:start position:0% I say I promise this implements a swap that<00:05:11.920> we've<00:05:12.340> agreed<00:05:12.550> upon<00:05:13.230> how<00:05:14.230> do<00:05:14.290> you<00:05:14.410> know 00:05:14.550 --> 00:05:14.560 align:start position:0% that we've agreed upon how do you know 00:05:14.560 --> 00:05:20.780 align:start position:0% that we've agreed upon how do you know you<00:05:15.250> can't<00:05:15.610> ultimately<00:05:17.250> trust<00:05:18.250> the<00:05:19.210> result<00:05:19.660> or 00:05:20.780 --> 00:05:20.790 align:start position:0% you can't ultimately trust the result or 00:05:20.790 --> 00:05:24.240 align:start position:0% you can't ultimately trust the result or the<00:05:21.790> design<00:05:22.240> of<00:05:22.690> a<00:05:23.350> given<00:05:23.620> smart<00:05:23.830> contract 00:05:24.240 --> 00:05:24.250 align:start position:0% the design of a given smart contract 00:05:24.250 --> 00:05:26.220 align:start position:0% the design of a given smart contract without<00:05:24.480> reasoning<00:05:25.480> about<00:05:25.660> it<00:05:25.840> without 00:05:26.220 --> 00:05:26.230 align:start position:0% without reasoning about it without 00:05:26.230 --> 00:05:28.080 align:start position:0% without reasoning about it without proving<00:05:26.650> theorems<00:05:27.070> about<00:05:27.430> it's<00:05:27.670> possible 00:05:28.080 --> 00:05:28.090 align:start position:0% proving theorems about it's possible 00:05:28.090 --> 00:05:30.360 align:start position:0% proving theorems about it's possible behavior<00:05:28.510> so<00:05:29.440> what<00:05:29.650> we've<00:05:29.770> done<00:05:29.800> is<00:05:30.160> we've 00:05:30.360 --> 00:05:30.370 align:start position:0% behavior so what we've done is we've 00:05:30.370 --> 00:05:32.220 align:start position:0% behavior so what we've done is we've taken<00:05:30.400> our<00:05:30.850> mantra<00:05:31.360> engine<00:05:31.780> which<00:05:31.930> I'll<00:05:32.080> tell 00:05:32.220 --> 00:05:32.230 align:start position:0% taken our mantra engine which I'll tell 00:05:32.230 --> 00:05:34.320 align:start position:0% taken our mantra engine which I'll tell you<00:05:32.290> about<00:05:32.380> for<00:05:33.190> reasoning<00:05:33.640> about<00:05:33.820> financial 00:05:34.320 --> 00:05:34.330 align:start position:0% you about for reasoning about financial 00:05:34.330 --> 00:05:36.260 align:start position:0% you about for reasoning about financial algorithms<00:05:34.750> and<00:05:34.960> now<00:05:35.050> we've<00:05:35.200> adapted<00:05:35.470> it<00:05:35.830> in 00:05:36.260 --> 00:05:36.270 align:start position:0% algorithms and now we've adapted it in 00:05:36.270 --> 00:05:38.490 align:start position:0% algorithms and now we've adapted it in effectively<00:05:37.270> two<00:05:37.450> different<00:05:37.780> ways<00:05:37.960> i'll<00:05:38.320> tell 00:05:38.490 --> 00:05:38.500 align:start position:0% effectively two different ways i'll tell 00:05:38.500 --> 00:05:40.020 align:start position:0% effectively two different ways i'll tell you<00:05:38.590> about<00:05:38.620> one<00:05:39.220> that's<00:05:39.430> reasoning<00:05:39.820> about<00:05:39.970> a 00:05:40.020 --> 00:05:40.030 align:start position:0% you about one that's reasoning about a 00:05:40.030 --> 00:05:42.060 align:start position:0% you about one that's reasoning about a high-level<00:05:40.420> language<00:05:40.810> that<00:05:41.500> can<00:05:41.590> be<00:05:41.650> compiled 00:05:42.060 --> 00:05:42.070 align:start position:0% high-level language that can be compiled 00:05:42.070 --> 00:05:44.670 align:start position:0% high-level language that can be compiled down<00:05:42.400> to<00:05:42.850> a<00:05:42.880> theorem<00:05:43.390> bytecode<00:05:43.780> and<00:05:44.020> the<00:05:44.530> other 00:05:44.670 --> 00:05:44.680 align:start position:0% down to a theorem bytecode and the other 00:05:44.680 --> 00:05:46.080 align:start position:0% down to a theorem bytecode and the other that<00:05:45.040> effectively<00:05:45.460> is<00:05:45.670> doing<00:05:45.880> something 00:05:46.080 --> 00:05:46.090 align:start position:0% that effectively is doing something 00:05:46.090 --> 00:05:48.450 align:start position:0% that effectively is doing something called<00:05:46.360> verified<00:05:46.990> d<00:05:47.170> compilation<00:05:47.770> that<00:05:47.950> takes 00:05:48.450 --> 00:05:48.460 align:start position:0% called verified d compilation that takes 00:05:48.460 --> 00:05:51.390 align:start position:0% called verified d compilation that takes etherium<00:05:48.850> bytecode<00:05:49.270> d<00:05:49.840> compiles<00:05:50.410> it<00:05:50.590> to<00:05:50.770> IML 00:05:51.390 --> 00:05:51.400 align:start position:0% etherium bytecode d compiles it to IML 00:05:51.400 --> 00:05:53.520 align:start position:0% etherium bytecode d compiles it to IML or<00:05:51.580> high-level<00:05:52.000> functional<00:05:52.720> language<00:05:53.020> that's 00:05:53.520 --> 00:05:53.530 align:start position:0% or high-level functional language that's 00:05:53.530 --> 00:05:55.350 align:start position:0% or high-level functional language that's actually<00:05:53.830> a<00:05:53.860> formalized<00:05:54.400> subset<00:05:54.790> of<00:05:54.820> o<00:05:54.970> camel 00:05:55.350 --> 00:05:55.360 align:start position:0% actually a formalized subset of o camel 00:05:55.360 --> 00:05:57.480 align:start position:0% actually a formalized subset of o camel if<00:05:55.510> you<00:05:55.750> know<00:05:55.870> camel<00:05:56.290> allows<00:05:56.950> you<00:05:57.100> to<00:05:57.190> reason 00:05:57.480 --> 00:05:57.490 align:start position:0% if you know camel allows you to reason 00:05:57.490 --> 00:05:59.010 align:start position:0% if you know camel allows you to reason about<00:05:57.550> it<00:05:57.850> and<00:05:57.970> push<00:05:58.120> the<00:05:58.300> proofs<00:05:58.540> back<00:05:58.780> down 00:05:59.010 --> 00:05:59.020 align:start position:0% about it and push the proofs back down 00:05:59.020 --> 00:06:01.800 align:start position:0% about it and push the proofs back down to<00:05:59.260> be<00:05:59.380> proofs<00:05:59.620> about<00:05:59.860> bytecode<00:06:00.390> so<00:06:01.390> okay 00:06:01.800 --> 00:06:01.810 align:start position:0% to be proofs about bytecode so okay 00:06:01.810 --> 00:06:03.900 align:start position:0% to be proofs about bytecode so okay that's<00:06:02.020> reasoning<00:06:02.830> about<00:06:03.010> individual 00:06:03.900 --> 00:06:03.910 align:start position:0% that's reasoning about individual 00:06:03.910 --> 00:06:07.140 align:start position:0% that's reasoning about individual contracts<00:06:04.330> but<00:06:05.170> as<00:06:05.290> I<00:06:05.380> mentioned<00:06:06.150> fundamental 00:06:07.140 --> 00:06:07.150 align:start position:0% contracts but as I mentioned fundamental 00:06:07.150 --> 00:06:10.760 align:start position:0% contracts but as I mentioned fundamental importance<00:06:07.630> as<00:06:07.960> you<00:06:08.410> know<00:06:08.500> a<00:06:08.530> bank<00:06:08.830> who's<00:06:09.790> a 00:06:10.760 --> 00:06:10.770 align:start position:0% importance as you know a bank who's a 00:06:10.770 --> 00:06:13.260 align:start position:0% importance as you know a bank who's a pioneer<00:06:11.770> right<00:06:12.160> now<00:06:12.340> with<00:06:12.640> let's<00:06:13.150> say 00:06:13.260 --> 00:06:13.270 align:start position:0% pioneer right now with let's say 00:06:13.270 --> 00:06:14.700 align:start position:0% pioneer right now with let's say athyrium<00:06:13.780> is<00:06:13.960> there<00:06:14.140> looking<00:06:14.380> down<00:06:14.410> the<00:06:14.680> road 00:06:14.700 --> 00:06:14.710 align:start position:0% athyrium is there looking down the road 00:06:14.710 --> 00:06:17.100 align:start position:0% athyrium is there looking down the road three<00:06:15.220> years<00:06:15.400> from<00:06:15.550> now<00:06:15.730> what<00:06:16.600> happens<00:06:16.930> when 00:06:17.100 --> 00:06:17.110 align:start position:0% three years from now what happens when 00:06:17.110 --> 00:06:19.590 align:start position:0% three years from now what happens when they<00:06:17.200> have<00:06:17.320> a<00:06:17.350> portfolio<00:06:17.710> of<00:06:18.070> 100,000<00:06:19.030> smart 00:06:19.590 --> 00:06:19.600 align:start position:0% they have a portfolio of 100,000 smart 00:06:19.600 --> 00:06:21.870 align:start position:0% they have a portfolio of 100,000 smart contracts<00:06:19.990> right<00:06:20.890> you<00:06:21.100> have<00:06:21.310> to<00:06:21.340> do<00:06:21.640> risk 00:06:21.870 --> 00:06:21.880 align:start position:0% contracts right you have to do risk 00:06:21.880 --> 00:06:23.460 align:start position:0% contracts right you have to do risk management<00:06:22.390> in<00:06:22.450> the<00:06:22.540> large<00:06:22.750> you<00:06:23.140> have<00:06:23.320> to 00:06:23.460 --> 00:06:23.470 align:start position:0% management in the large you have to 00:06:23.470 --> 00:06:25.830 align:start position:0% management in the large you have to compute<00:06:23.770> Greeks<00:06:24.100> and<00:06:24.430> to<00:06:25.060> do<00:06:25.240> that<00:06:25.420> you<00:06:25.750> have 00:06:25.830 --> 00:06:25.840 align:start position:0% compute Greeks and to do that you have 00:06:25.840 --> 00:06:28.350 align:start position:0% compute Greeks and to do that you have to<00:06:26.050> reason<00:06:26.650> about<00:06:26.710> the<00:06:27.010> code<00:06:27.190> so<00:06:27.910> you<00:06:27.970> must 00:06:28.350 --> 00:06:28.360 align:start position:0% to reason about the code so you must 00:06:28.360 --> 00:06:31.640 align:start position:0% to reason about the code so you must have<00:06:28.860> effectively<00:06:29.860> formal<00:06:30.400> semantics<00:06:30.970> that 00:06:31.640 --> 00:06:31.650 align:start position:0% have effectively formal semantics that 00:06:31.650 --> 00:06:34.500 align:start position:0% have effectively formal semantics that ultimately<00:06:32.650> is<00:06:32.800> mechanized<00:06:33.250> for<00:06:33.970> reasoning 00:06:34.500 --> 00:06:34.510 align:start position:0% ultimately is mechanized for reasoning 00:06:34.510 --> 00:06:37.920 align:start position:0% ultimately is mechanized for reasoning about<00:06:34.720> your<00:06:35.140> smart<00:06:35.410> contracts<00:06:36.420> so<00:06:37.420> let<00:06:37.900> me 00:06:37.920 --> 00:06:37.930 align:start position:0% about your smart contracts so let me 00:06:37.930 --> 00:06:39.300 align:start position:0% about your smart contracts so let me tell<00:06:38.080> you<00:06:38.200> a<00:06:38.230> bit<00:06:38.440> about<00:06:38.470> how<00:06:38.770> a<00:06:38.800> mantra<00:06:39.190> is 00:06:39.300 --> 00:06:39.310 align:start position:0% tell you a bit about how a mantra is 00:06:39.310 --> 00:06:43.620 align:start position:0% tell you a bit about how a mantra is used<00:06:39.490> currently<00:06:39.900> so<00:06:41.010> our<00:06:42.010> biggest<00:06:42.970> focus<00:06:43.210> has 00:06:43.620 --> 00:06:43.630 align:start position:0% used currently so our biggest focus has 00:06:43.630 --> 00:06:45.180 align:start position:0% used currently so our biggest focus has been<00:06:43.660> something<00:06:44.050> we<00:06:44.230> call<00:06:44.410> a<00:06:44.440> mantra<00:06:44.860> venues 00:06:45.180 --> 00:06:45.190 align:start position:0% been something we call a mantra venues 00:06:45.190 --> 00:06:47.730 align:start position:0% been something we call a mantra venues and<00:06:45.460> this<00:06:46.030> is<00:06:46.180> using<00:06:46.540> a<00:06:46.750> mantra<00:06:47.080> to<00:06:47.260> formally 00:06:47.730 --> 00:06:47.740 align:start position:0% and this is using a mantra to formally 00:06:47.740 --> 00:06:49.740 align:start position:0% and this is using a mantra to formally analyze<00:06:48.220> the<00:06:48.580> matching<00:06:48.970> logics<00:06:49.390> behind 00:06:49.740 --> 00:06:49.750 align:start position:0% analyze the matching logics behind 00:06:49.750 --> 00:06:51.090 align:start position:0% analyze the matching logics behind trading<00:06:50.110> venues<00:06:50.260> things<00:06:50.650> like<00:06:50.830> stock 00:06:51.090 --> 00:06:51.100 align:start position:0% trading venues things like stock 00:06:51.100 --> 00:06:53.400 align:start position:0% trading venues things like stock exchanges<00:06:51.670> and<00:06:51.790> dark<00:06:52.000> pools<00:06:52.270> so<00:06:53.110> you<00:06:53.170> may<00:06:53.380> have 00:06:53.400 --> 00:06:53.410 align:start position:0% exchanges and dark pools so you may have 00:06:53.410 --> 00:06:56.250 align:start position:0% exchanges and dark pools so you may have heard<00:06:54.280> about<00:06:54.460> many<00:06:54.820> glitches<00:06:55.090> in<00:06:55.570> the<00:06:56.020> past 00:06:56.250 --> 00:06:56.260 align:start position:0% heard about many glitches in the past 00:06:56.260 --> 00:06:59.250 align:start position:0% heard about many glitches in the past few<00:06:56.440> years<00:06:56.820> for<00:06:57.820> instance<00:06:58.000> bats<00:06:58.330> failed 00:06:59.250 --> 00:06:59.260 align:start position:0% few years for instance bats failed 00:06:59.260 --> 00:07:01.440 align:start position:0% few years for instance bats failed trading<00:06:59.710> its<00:06:59.830> own<00:06:59.980> IPO<00:07:00.370> of<00:07:00.880> course<00:07:01.090> famous 00:07:01.440 --> 00:07:01.450 align:start position:0% trading its own IPO of course famous 00:07:01.450 --> 00:07:04.260 align:start position:0% trading its own IPO of course famous Nasdaq<00:07:01.900> Nasdaq<00:07:02.710> glitch<00:07:03.070> with<00:07:03.250> Facebook<00:07:03.700> night 00:07:04.260 --> 00:07:04.270 align:start position:0% Nasdaq Nasdaq glitch with Facebook night 00:07:04.270 --> 00:07:06.330 align:start position:0% Nasdaq Nasdaq glitch with Facebook night capital<00:07:04.810> goldman<00:07:05.350> sachs<00:07:05.560> alphabet<00:07:06.010> trading 00:07:06.330 --> 00:07:06.340 align:start position:0% capital goldman sachs alphabet trading 00:07:06.340 --> 00:07:07.260 align:start position:0% capital goldman sachs alphabet trading glitch<00:07:06.520> these 00:07:07.260 --> 00:07:07.270 align:start position:0% glitch these 00:07:07.270 --> 00:07:08.670 align:start position:0% glitch these happen<00:07:07.480> all<00:07:07.600> the<00:07:07.630> time<00:07:07.750> and<00:07:08.140> finance<00:07:08.530> and 00:07:08.670 --> 00:07:08.680 align:start position:0% happen all the time and finance and 00:07:08.680 --> 00:07:10.530 align:start position:0% happen all the time and finance and fundamentally<00:07:09.370> what's<00:07:09.520> been<00:07:09.730> missing<00:07:09.910> is<00:07:10.210> a 00:07:10.530 --> 00:07:10.540 align:start position:0% fundamentally what's been missing is a 00:07:10.540 --> 00:07:12.300 align:start position:0% fundamentally what's been missing is a way<00:07:10.750> to<00:07:10.780> reason<00:07:11.290> about<00:07:11.380> the<00:07:11.680> algorithms<00:07:12.160> in 00:07:12.300 --> 00:07:12.310 align:start position:0% way to reason about the algorithms in 00:07:12.310 --> 00:07:15.810 align:start position:0% way to reason about the algorithms in advance<00:07:12.610> of<00:07:12.820> their<00:07:12.940> deployment<00:07:13.650> so<00:07:14.650> a<00:07:14.980> mantra 00:07:15.810 --> 00:07:15.820 align:start position:0% advance of their deployment so a mantra 00:07:15.820 --> 00:07:18.270 align:start position:0% advance of their deployment so a mantra venues<00:07:16.420> is<00:07:16.720> now<00:07:16.870> currently<00:07:17.140> get<00:07:17.380> use<00:07:17.620> at<00:07:17.920> top 00:07:18.270 --> 00:07:18.280 align:start position:0% venues is now currently get use at top 00:07:18.280 --> 00:07:20.880 align:start position:0% venues is now currently get use at top five<00:07:18.520> global<00:07:19.120> investment<00:07:19.540> banks<00:07:19.890> effectively 00:07:20.880 --> 00:07:20.890 align:start position:0% five global investment banks effectively 00:07:20.890 --> 00:07:25.580 align:start position:0% five global investment banks effectively to<00:07:21.190> take<00:07:21.750> what<00:07:22.750> is<00:07:23.070> classically<00:07:24.150> an 00:07:25.580 --> 00:07:25.590 align:start position:0% to take what is classically an 00:07:25.590 --> 00:07:28.980 align:start position:0% to take what is classically an imprecisely<00:07:26.590> described<00:07:27.430> algorithm<00:07:28.420> their 00:07:28.980 --> 00:07:28.990 align:start position:0% imprecisely described algorithm their 00:07:28.990 --> 00:07:30.600 align:start position:0% imprecisely described algorithm their collection<00:07:29.470> of<00:07:29.560> matching<00:07:29.920> logic<00:07:30.280> that<00:07:30.460> is 00:07:30.600 --> 00:07:30.610 align:start position:0% collection of matching logic that is 00:07:30.610 --> 00:07:32.790 align:start position:0% collection of matching logic that is usually<00:07:30.970> described<00:07:31.390> say<00:07:31.720> in<00:07:31.900> some<00:07:32.410> collection 00:07:32.790 --> 00:07:32.800 align:start position:0% usually described say in some collection 00:07:32.800 --> 00:07:35.460 align:start position:0% usually described say in some collection of<00:07:32.920> PDFs<00:07:33.810> you<00:07:34.810> know<00:07:34.900> there<00:07:35.080> there<00:07:35.320> is 00:07:35.460 --> 00:07:35.470 align:start position:0% of PDFs you know there there is 00:07:35.470 --> 00:07:38.160 align:start position:0% of PDFs you know there there is classically<00:07:36.190> no<00:07:36.340> formal<00:07:36.910> spec<00:07:37.450> of<00:07:37.630> how<00:07:37.990> these 00:07:38.160 --> 00:07:38.170 align:start position:0% classically no formal spec of how these 00:07:38.170 --> 00:07:40.560 align:start position:0% classically no formal spec of how these things<00:07:38.200> are<00:07:38.470> supposed<00:07:38.830> to<00:07:38.890> work<00:07:39.130> but<00:07:39.940> it's 00:07:40.560 --> 00:07:40.570 align:start position:0% things are supposed to work but it's 00:07:40.570 --> 00:07:45.180 align:start position:0% things are supposed to work but it's actually<00:07:41.010> taking<00:07:42.010> those<00:07:43.860> ambiguous<00:07:44.860> sort<00:07:45.130> of 00:07:45.180 --> 00:07:45.190 align:start position:0% actually taking those ambiguous sort of 00:07:45.190 --> 00:07:47.790 align:start position:0% actually taking those ambiguous sort of in<00:07:45.310> precise<00:07:45.670> specs<00:07:46.030> making<00:07:46.780> them<00:07:46.930> precise<00:07:47.410> in 00:07:47.790 --> 00:07:47.800 align:start position:0% in precise specs making them precise in 00:07:47.800 --> 00:07:50.100 align:start position:0% in precise specs making them precise in a<00:07:47.980> mantra<00:07:48.400> reasoning<00:07:49.360> about<00:07:49.540> fairness<00:07:49.870> and 00:07:50.100 --> 00:07:50.110 align:start position:0% a mantra reasoning about fairness and 00:07:50.110 --> 00:07:52.110 align:start position:0% a mantra reasoning about fairness and safety<00:07:50.470> properties<00:07:50.950> and<00:07:51.190> then<00:07:51.610> using<00:07:51.910> a 00:07:52.110 --> 00:07:52.120 align:start position:0% safety properties and then using a 00:07:52.120 --> 00:07:54.480 align:start position:0% safety properties and then using a mantra<00:07:52.570> to<00:07:52.990> vet<00:07:53.320> their<00:07:53.680> high-performance 00:07:54.480 --> 00:07:54.490 align:start position:0% mantra to vet their high-performance 00:07:54.490 --> 00:07:56.130 align:start position:0% mantra to vet their high-performance production<00:07:54.910> systems<00:07:55.330> to<00:07:55.540> ensure<00:07:55.660> that<00:07:55.840> the 00:07:56.130 --> 00:07:56.140 align:start position:0% production systems to ensure that the 00:07:56.140 --> 00:07:59.150 align:start position:0% production systems to ensure that the production<00:07:56.560> systems<00:07:56.980> really<00:07:57.520> correspond<00:07:58.240> to 00:07:59.150 --> 00:07:59.160 align:start position:0% production systems really correspond to 00:07:59.160 --> 00:08:03.180 align:start position:0% production systems really correspond to verified<00:08:00.160> specifications<00:08:01.110> so<00:08:02.110> there's<00:08:03.040> also 00:08:03.180 --> 00:08:03.190 align:start position:0% verified specifications so there's also 00:08:03.190 --> 00:08:04.740 align:start position:0% verified specifications so there's also some<00:08:03.460> exciting<00:08:03.790> developments<00:08:04.360> we<00:08:04.480> have<00:08:04.630> in 00:08:04.740 --> 00:08:04.750 align:start position:0% some exciting developments we have in 00:08:04.750 --> 00:08:06.600 align:start position:0% some exciting developments we have in the<00:08:04.840> regulatory<00:08:05.140> space<00:08:05.650> so<00:08:05.860> just<00:08:06.070> to<00:08:06.190> say<00:08:06.370> we 00:08:06.600 --> 00:08:06.610 align:start position:0% the regulatory space so just to say we 00:08:06.610 --> 00:08:08.460 align:start position:0% the regulatory space so just to say we came<00:08:07.150> out<00:08:07.270> of<00:08:07.390> stealth<00:08:07.600> mode<00:08:07.840> with<00:08:08.050> this<00:08:08.260> an 00:08:08.460 --> 00:08:08.470 align:start position:0% came out of stealth mode with this an 00:08:08.470 --> 00:08:11.010 align:start position:0% came out of stealth mode with this an april<00:08:08.650> and<00:08:09.070> the<00:08:09.370> sec<00:08:09.910> brought<00:08:10.690> us<00:08:10.810> to 00:08:11.010 --> 00:08:11.020 align:start position:0% april and the sec brought us to 00:08:11.020 --> 00:08:14.220 align:start position:0% april and the sec brought us to washington<00:08:11.710> DC<00:08:11.980> to<00:08:12.310> the<00:08:12.400> sec<00:08:12.790> headquarters<00:08:13.300> to 00:08:14.220 --> 00:08:14.230 align:start position:0% washington DC to the sec headquarters to 00:08:14.230 --> 00:08:15.810 align:start position:0% washington DC to the sec headquarters to teach<00:08:14.650> them<00:08:14.830> about<00:08:15.040> a<00:08:15.070> mantra<00:08:15.400> for<00:08:15.550> two<00:08:15.670> days 00:08:15.810 --> 00:08:15.820 align:start position:0% teach them about a mantra for two days 00:08:15.820 --> 00:08:18.480 align:start position:0% teach them about a mantra for two days and<00:08:16.090> some<00:08:16.870> exciting<00:08:17.320> developments<00:08:18.280> will<00:08:18.400> be 00:08:18.480 --> 00:08:18.490 align:start position:0% and some exciting developments will be 00:08:18.490 --> 00:08:21.300 align:start position:0% and some exciting developments will be announced<00:08:19.330> soon<00:08:19.450> on<00:08:20.020> a<00:08:20.080> mantra<00:08:20.770> in<00:08:20.980> the 00:08:21.300 --> 00:08:21.310 align:start position:0% announced soon on a mantra in the 00:08:21.310 --> 00:08:22.890 align:start position:0% announced soon on a mantra in the regulatory<00:08:21.610> space<00:08:22.090> but<00:08:22.330> fundamentally 00:08:22.890 --> 00:08:22.900 align:start position:0% regulatory space but fundamentally 00:08:22.900 --> 00:08:25.710 align:start position:0% regulatory space but fundamentally regulators<00:08:23.500> face<00:08:24.310> the<00:08:24.490> same<00:08:24.670> issues<00:08:24.970> someone 00:08:25.710 --> 00:08:25.720 align:start position:0% regulators face the same issues someone 00:08:25.720 --> 00:08:27.240 align:start position:0% regulators face the same issues someone comes<00:08:25.960> to<00:08:26.050> them<00:08:26.260> and<00:08:26.410> says<00:08:26.590> I'd<00:08:26.830> like<00:08:26.980> to<00:08:27.100> add 00:08:27.240 --> 00:08:27.250 align:start position:0% comes to them and says I'd like to add 00:08:27.250 --> 00:08:29.780 align:start position:0% comes to them and says I'd like to add this<00:08:27.430> new<00:08:27.610> order<00:08:27.880> type<00:08:28.090> to<00:08:28.330> my<00:08:28.420> trading<00:08:28.690> venue 00:08:29.780 --> 00:08:29.790 align:start position:0% this new order type to my trading venue 00:08:29.790 --> 00:08:32.130 align:start position:0% this new order type to my trading venue ensure<00:08:30.790> for<00:08:31.150> me<00:08:31.270> that<00:08:31.510> you<00:08:31.720> know<00:08:31.840> this<00:08:32.110> is 00:08:32.130 --> 00:08:32.140 align:start position:0% ensure for me that you know this is 00:08:32.140 --> 00:08:34.200 align:start position:0% ensure for me that you know this is allowed<00:08:32.560> and<00:08:32.830> the<00:08:33.070> SEC<00:08:33.490> then<00:08:33.670> has<00:08:33.820> to<00:08:34.000> process 00:08:34.200 --> 00:08:34.210 align:start position:0% allowed and the SEC then has to process 00:08:34.210 --> 00:08:36.540 align:start position:0% allowed and the SEC then has to process these<00:08:34.570> things<00:08:34.870> and<00:08:35.110> you<00:08:35.410> know<00:08:35.530> so<00:08:36.040> so<00:08:36.310> does<00:08:36.430> the 00:08:36.540 --> 00:08:36.550 align:start position:0% these things and you know so so does the 00:08:36.550 --> 00:08:38.730 align:start position:0% these things and you know so so does the FCA<00:08:36.820> and<00:08:37.090> other<00:08:37.180> global<00:08:37.330> regulators<00:08:37.720> and<00:08:38.140> it's 00:08:38.730 --> 00:08:38.740 align:start position:0% FCA and other global regulators and it's 00:08:38.740 --> 00:08:40.650 align:start position:0% FCA and other global regulators and it's virtually<00:08:39.490> impossible<00:08:39.580> to<00:08:40.090> do<00:08:40.300> by<00:08:40.450> hand 00:08:40.650 --> 00:08:40.660 align:start position:0% virtually impossible to do by hand 00:08:40.660 --> 00:08:44.190 align:start position:0% virtually impossible to do by hand without<00:08:40.870> formal<00:08:41.410> verification<00:08:42.270> so<00:08:43.270> what<00:08:44.020> is<00:08:44.170> a 00:08:44.190 --> 00:08:44.200 align:start position:0% without formal verification so what is a 00:08:44.200 --> 00:08:46.020 align:start position:0% without formal verification so what is a mantra<00:08:44.710> I'm<00:08:45.220> going<00:08:45.370> to<00:08:45.460> give<00:08:45.640> you<00:08:45.760> very 00:08:46.020 --> 00:08:46.030 align:start position:0% mantra I'm going to give you very 00:08:46.030 --> 00:08:48.180 align:start position:0% mantra I'm going to give you very low-level<00:08:46.480> demos<00:08:47.020> of<00:08:47.230> a<00:08:47.290> mantra<00:08:47.710> this<00:08:48.010> is<00:08:48.160> a 00:08:48.180 --> 00:08:48.190 align:start position:0% low-level demos of a mantra this is a 00:08:48.190 --> 00:08:50.550 align:start position:0% low-level demos of a mantra this is a very<00:08:48.370> technical<00:08:48.820> audience<00:08:49.180> so<00:08:50.170> i<00:08:50.200> want<00:08:50.350> you<00:08:50.410> to 00:08:50.550 --> 00:08:50.560 align:start position:0% very technical audience so i want you to 00:08:50.560 --> 00:08:52.530 align:start position:0% very technical audience so i want you to see<00:08:50.740> really<00:08:51.100> in<00:08:51.310> action<00:08:52.030> and<00:08:52.150> i<00:08:52.210> want<00:08:52.390> to<00:08:52.420> talk 00:08:52.530 --> 00:08:52.540 align:start position:0% see really in action and i want to talk 00:08:52.540 --> 00:08:53.820 align:start position:0% see really in action and i want to talk to<00:08:52.600> you<00:08:52.780> a<00:08:52.840> bit<00:08:52.960> about<00:08:53.020> the<00:08:53.380> automated 00:08:53.820 --> 00:08:53.830 align:start position:0% to you a bit about the automated 00:08:53.830 --> 00:08:55.800 align:start position:0% to you a bit about the automated reasoning<00:08:54.010> and<00:08:54.430> mathematical<00:08:54.940> logic<00:08:55.030> that's 00:08:55.800 --> 00:08:55.810 align:start position:0% reasoning and mathematical logic that's 00:08:55.810 --> 00:08:57.540 align:start position:0% reasoning and mathematical logic that's under<00:08:56.050> the<00:08:56.140> hood<00:08:56.290> but<00:08:56.920> fundamentally<00:08:57.550> it's 00:08:57.540 --> 00:08:57.550 align:start position:0% under the hood but fundamentally it's 00:08:57.550 --> 00:08:59.550 align:start position:0% under the hood but fundamentally it's three<00:08:57.940> things<00:08:58.210> in<00:08:58.390> one<00:08:58.630> it's<00:08:59.020> a<00:08:59.140> programming 00:08:59.550 --> 00:08:59.560 align:start position:0% three things in one it's a programming 00:08:59.560 --> 00:09:02.250 align:start position:0% three things in one it's a programming language<00:08:59.680> so<00:09:00.520> it's<00:09:01.150> a<00:09:01.270> formalized<00:09:01.750> subset<00:09:02.230> of 00:09:02.250 --> 00:09:02.260 align:start position:0% language so it's a formalized subset of 00:09:02.260 --> 00:09:04.170 align:start position:0% language so it's a formalized subset of o<00:09:02.410> camel<00:09:02.830> if<00:09:02.980> you're<00:09:03.190> familiar<00:09:03.310> with<00:09:03.550> o<00:09:03.790> camel 00:09:04.170 --> 00:09:04.180 align:start position:0% o camel if you're familiar with o camel 00:09:04.180 --> 00:09:07.950 align:start position:0% o camel if you're familiar with o camel in<00:09:04.360> the<00:09:04.630> ml<00:09:05.440> family<00:09:05.860> of<00:09:05.950> languages<00:09:06.960> functional 00:09:07.950 --> 00:09:07.960 align:start position:0% in the ml family of languages functional 00:09:07.960 --> 00:09:11.780 align:start position:0% in the ml family of languages functional language<00:09:08.290> it's<00:09:09.070> a<00:09:09.190> mathematical<00:09:09.340> logic<00:09:09.850> so 00:09:11.780 --> 00:09:11.790 align:start position:0% language it's a mathematical logic so 00:09:11.790 --> 00:09:14.520 align:start position:0% language it's a mathematical logic so fundamentally<00:09:12.790> every<00:09:13.090> data<00:09:13.570> type<00:09:13.870> definition 00:09:14.520 --> 00:09:14.530 align:start position:0% fundamentally every data type definition 00:09:14.530 --> 00:09:15.890 align:start position:0% fundamentally every data type definition or<00:09:14.620> every<00:09:14.890> program<00:09:15.340> they 00:09:15.890 --> 00:09:15.900 align:start position:0% or every program they 00:09:15.900 --> 00:09:17.690 align:start position:0% or every program they to<00:09:16.020> find<00:09:16.260> every<00:09:16.560> function<00:09:16.950> you<00:09:17.070> define<00:09:17.370> in<00:09:17.610> a 00:09:17.690 --> 00:09:17.700 align:start position:0% to find every function you define in a 00:09:17.700 --> 00:09:20.720 align:start position:0% to find every function you define in a mantra<00:09:18.090> is<00:09:18.470> automatically<00:09:19.470> transformed<00:09:20.430> into 00:09:20.720 --> 00:09:20.730 align:start position:0% mantra is automatically transformed into 00:09:20.730 --> 00:09:23.750 align:start position:0% mantra is automatically transformed into an<00:09:21.000> axiomatic<00:09:21.450> representation<00:09:22.550> that<00:09:23.550> then<00:09:23.730> a 00:09:23.750 --> 00:09:23.760 align:start position:0% an axiomatic representation that then a 00:09:23.760 --> 00:09:26.180 align:start position:0% an axiomatic representation that then a mantras<00:09:24.270> reasoning<00:09:24.720> engine<00:09:25.020> reasons<00:09:25.950> about 00:09:26.180 --> 00:09:26.190 align:start position:0% mantras reasoning engine reasons about 00:09:26.190 --> 00:09:30.350 align:start position:0% mantras reasoning engine reasons about so<00:09:26.730> you<00:09:26.790> write<00:09:27.060> code<00:09:27.390> and<00:09:28.640> questions<00:09:29.640> that<00:09:30.240> you 00:09:30.350 --> 00:09:30.360 align:start position:0% so you write code and questions that you 00:09:30.360 --> 00:09:32.360 align:start position:0% so you write code and questions that you would<00:09:30.450> like<00:09:30.510> to<00:09:30.870> ask<00:09:31.020> a<00:09:31.380> mantra<00:09:31.800> about<00:09:32.130> your 00:09:32.360 --> 00:09:32.370 align:start position:0% would like to ask a mantra about your 00:09:32.370 --> 00:09:34.820 align:start position:0% would like to ask a mantra about your code<00:09:32.610> in<00:09:32.880> a<00:09:33.300> mantra<00:09:33.630> works<00:09:33.870> to<00:09:34.110> produce<00:09:34.290> proofs 00:09:34.820 --> 00:09:34.830 align:start position:0% code in a mantra works to produce proofs 00:09:34.830 --> 00:09:37.400 align:start position:0% code in a mantra works to produce proofs or<00:09:35.160> counter<00:09:35.730> examples<00:09:36.180> using<00:09:37.020> many<00:09:37.320> different 00:09:37.400 --> 00:09:37.410 align:start position:0% or counter examples using many different 00:09:37.410 --> 00:09:39.800 align:start position:0% or counter examples using many different types<00:09:38.160> of<00:09:38.400> decision<00:09:38.760> procedures<00:09:39.210> and<00:09:39.540> I'll 00:09:39.800 --> 00:09:39.810 align:start position:0% types of decision procedures and I'll 00:09:39.810 --> 00:09:42.920 align:start position:0% types of decision procedures and I'll talk<00:09:40.020> to<00:09:40.050> you<00:09:40.200> more<00:09:40.290> about<00:09:40.350> them<00:09:41.480> so<00:09:42.480> that's 00:09:42.920 --> 00:09:42.930 align:start position:0% talk to you more about them so that's 00:09:42.930 --> 00:09:44.270 align:start position:0% talk to you more about them so that's the<00:09:43.080> big<00:09:43.200> idea<00:09:43.350> what<00:09:43.830> I<00:09:43.860> just<00:09:43.920> outlined 00:09:44.270 --> 00:09:44.280 align:start position:0% the big idea what I just outlined 00:09:44.280 --> 00:09:46.160 align:start position:0% the big idea what I just outlined effectively<00:09:45.270> you<00:09:45.390> give<00:09:45.540> a<00:09:45.570> mantra<00:09:45.960> your 00:09:46.160 --> 00:09:46.170 align:start position:0% effectively you give a mantra your 00:09:46.170 --> 00:09:47.990 align:start position:0% effectively you give a mantra your financial<00:09:46.980> algorithm<00:09:47.430> or<00:09:47.580> your<00:09:47.700> smart 00:09:47.990 --> 00:09:48.000 align:start position:0% financial algorithm or your smart 00:09:48.000 --> 00:09:50.960 align:start position:0% financial algorithm or your smart contract<00:09:48.650> and<00:09:49.650> ask<00:09:50.130> them<00:09:50.340> onto<00:09:50.550> a<00:09:50.580> question 00:09:50.960 --> 00:09:50.970 align:start position:0% contract and ask them onto a question 00:09:50.970 --> 00:09:52.850 align:start position:0% contract and ask them onto a question you<00:09:51.270> know<00:09:51.360> is<00:09:51.480> there<00:09:51.660> a<00:09:51.690> potential<00:09:52.320> glitch<00:09:52.650> of 00:09:52.850 --> 00:09:52.860 align:start position:0% you know is there a potential glitch of 00:09:52.860 --> 00:09:56.480 align:start position:0% you know is there a potential glitch of this<00:09:53.010> class<00:09:53.310> or<00:09:53.840> does<00:09:54.840> this<00:09:55.080> do<00:09:55.290> some<00:09:55.530> concrete 00:09:56.480 --> 00:09:56.490 align:start position:0% this class or does this do some concrete 00:09:56.490 --> 00:09:58.550 align:start position:0% this class or does this do some concrete form<00:09:56.880> of<00:09:57.030> unfair<00:09:57.390> trading<00:09:57.720> for<00:09:58.080> instance<00:09:58.380> is 00:09:58.550 --> 00:09:58.560 align:start position:0% form of unfair trading for instance is 00:09:58.560 --> 00:10:00.740 align:start position:0% form of unfair trading for instance is there<00:09:59.040> some<00:09:59.220> sequence<00:09:59.610> of<00:09:59.760> messages<00:09:59.940> that 00:10:00.740 --> 00:10:00.750 align:start position:0% there some sequence of messages that 00:10:00.750 --> 00:10:02.330 align:start position:0% there some sequence of messages that could<00:10:00.900> be<00:10:00.990> sent<00:10:01.260> to<00:10:01.380> this<00:10:01.500> trading<00:10:01.800> venue<00:10:02.160> that 00:10:02.330 --> 00:10:02.340 align:start position:0% could be sent to this trading venue that 00:10:02.340 --> 00:10:04.190 align:start position:0% could be sent to this trading venue that could<00:10:02.730> allow<00:10:02.940> someone<00:10:03.330> to<00:10:03.570> jump<00:10:03.780> the<00:10:03.930> queue 00:10:04.190 --> 00:10:04.200 align:start position:0% could allow someone to jump the queue 00:10:04.200 --> 00:10:07.370 align:start position:0% could allow someone to jump the queue right<00:10:04.940> and<00:10:05.940> ultimately<00:10:06.540> you<00:10:06.780> get<00:10:06.930> out<00:10:07.050> either 00:10:07.370 --> 00:10:07.380 align:start position:0% right and ultimately you get out either 00:10:07.380 --> 00:10:09.470 align:start position:0% right and ultimately you get out either that<00:10:07.500> the<00:10:07.650> algorithm<00:10:07.980> is<00:10:08.280> verified<00:10:08.760> with<00:10:09.420> a 00:10:09.470 --> 00:10:09.480 align:start position:0% that the algorithm is verified with a 00:10:09.480 --> 00:10:10.640 align:start position:0% that the algorithm is verified with a mathematical<00:10:10.050> proof<00:10:10.260> that<00:10:10.470> can<00:10:10.560> be 00:10:10.640 --> 00:10:10.650 align:start position:0% mathematical proof that can be 00:10:10.650 --> 00:10:13.010 align:start position:0% mathematical proof that can be independently<00:10:11.220> vetted<00:10:11.670> or<00:10:11.880> you<00:10:12.840> get<00:10:12.990> a 00:10:13.010 --> 00:10:13.020 align:start position:0% independently vetted or you get a 00:10:13.020 --> 00:10:14.780 align:start position:0% independently vetted or you get a counter<00:10:13.290> example<00:10:13.410> so<00:10:13.980> that's<00:10:14.160> that's<00:10:14.400> the<00:10:14.640> big 00:10:14.780 --> 00:10:14.790 align:start position:0% counter example so that's that's the big 00:10:14.790 --> 00:10:17.480 align:start position:0% counter example so that's that's the big idea<00:10:15.290> pushing<00:10:16.290> pushing<00:10:16.830> these<00:10:17.010> questions 00:10:17.480 --> 00:10:17.490 align:start position:0% idea pushing pushing these questions 00:10:17.490 --> 00:10:19.130 align:start position:0% idea pushing pushing these questions into<00:10:17.700> what<00:10:17.880> are<00:10:17.910> called<00:10:18.000> decidable<00:10:18.630> fragments 00:10:19.130 --> 00:10:19.140 align:start position:0% into what are called decidable fragments 00:10:19.140 --> 00:10:21.620 align:start position:0% into what are called decidable fragments so<00:10:19.620> that<00:10:19.770> this<00:10:19.890> is<00:10:20.040> automatic<00:10:20.490> so<00:10:21.240> let<00:10:21.390> me<00:10:21.480> show 00:10:21.620 --> 00:10:21.630 align:start position:0% so that this is automatic so let me show 00:10:21.630 --> 00:10:25.160 align:start position:0% so that this is automatic so let me show you<00:10:21.690> a<00:10:21.780> very<00:10:22.140> simple<00:10:22.380> example<00:10:23.540> here<00:10:24.540> we<00:10:25.020> have 00:10:25.160 --> 00:10:25.170 align:start position:0% you a very simple example here we have 00:10:25.170 --> 00:10:27.140 align:start position:0% you a very simple example here we have on<00:10:25.380> the<00:10:25.500> left<00:10:25.710> if<00:10:26.040> you<00:10:26.190> can<00:10:26.370> read<00:10:26.520> it<00:10:26.640> a 00:10:27.140 --> 00:10:27.150 align:start position:0% on the left if you can read it a 00:10:27.150 --> 00:10:29.900 align:start position:0% on the left if you can read it a summation<00:10:27.720> function<00:10:28.440> just<00:10:28.950> in<00:10:29.070> a<00:10:29.130> mantra<00:10:29.460> so 00:10:29.900 --> 00:10:29.910 align:start position:0% summation function just in a mantra so 00:10:29.910 --> 00:10:31.370 align:start position:0% summation function just in a mantra so you<00:10:29.970> may<00:10:30.180> this<00:10:30.570> is<00:10:30.720> just<00:10:30.930> summing<00:10:31.230> up<00:10:31.320> the 00:10:31.370 --> 00:10:31.380 align:start position:0% you may this is just summing up the 00:10:31.380 --> 00:10:34.490 align:start position:0% you may this is just summing up the numbers<00:10:31.860> from<00:10:32.100> 0<00:10:32.430> to<00:10:32.520> n<00:10:32.730> the<00:10:33.200> natural<00:10:34.200> numbers 00:10:34.490 --> 00:10:34.500 align:start position:0% numbers from 0 to n the natural numbers 00:10:34.500 --> 00:10:36.800 align:start position:0% numbers from 0 to n the natural numbers and<00:10:34.770> it's<00:10:35.280> a<00:10:35.340> program<00:10:35.730> so<00:10:36.060> on<00:10:36.210> the<00:10:36.300> right<00:10:36.480> we're 00:10:36.800 --> 00:10:36.810 align:start position:0% and it's a program so on the right we're 00:10:36.810 --> 00:10:38.840 align:start position:0% and it's a program so on the right we're just<00:10:37.020> computing<00:10:37.620> with<00:10:37.740> it<00:10:37.920> right<00:10:38.580> we<00:10:38.730> can 00:10:38.840 --> 00:10:38.850 align:start position:0% just computing with it right we can 00:10:38.850 --> 00:10:42.080 align:start position:0% just computing with it right we can compute<00:10:39.210> some<00:10:39.450> 5<00:10:39.780> some<00:10:40.620> of<00:10:40.740> 100<00:10:41.160> but<00:10:41.820> you<00:10:41.970> may 00:10:42.080 --> 00:10:42.090 align:start position:0% compute some 5 some of 100 but you may 00:10:42.090 --> 00:10:44.720 align:start position:0% compute some 5 some of 100 but you may remember<00:10:42.390> this<00:10:42.720> possibly<00:10:43.620> apocryphal<00:10:43.860> story 00:10:44.720 --> 00:10:44.730 align:start position:0% remember this possibly apocryphal story 00:10:44.730 --> 00:10:47.120 align:start position:0% remember this possibly apocryphal story of<00:10:44.880> Gauss's<00:10:45.120> a<00:10:45.450> six-year-old<00:10:46.130> proving 00:10:47.120 --> 00:10:47.130 align:start position:0% of Gauss's a six-year-old proving 00:10:47.130 --> 00:10:50.090 align:start position:0% of Gauss's a six-year-old proving actually<00:10:47.550> that<00:10:47.760> the<00:10:48.270> sum<00:10:48.540> of<00:10:48.690> in<00:10:49.010> you<00:10:50.010> know 00:10:50.090 --> 00:10:50.100 align:start position:0% actually that the sum of in you know 00:10:50.100 --> 00:10:52.730 align:start position:0% actually that the sum of in you know some<00:10:50.280> of<00:10:50.310> 0<00:10:50.640> up<00:10:50.850> to<00:10:51.000> n<00:10:51.150> is<00:10:51.510> equal<00:10:51.810> to<00:10:51.930> n<00:10:52.200> times<00:10:52.530> n 00:10:52.730 --> 00:10:52.740 align:start position:0% some of 0 up to n is equal to n times n 00:10:52.740 --> 00:10:55.970 align:start position:0% some of 0 up to n is equal to n times n plus<00:10:52.770> 1<00:10:53.160> over<00:10:53.190> 2<00:10:53.660> so<00:10:54.660> we<00:10:54.870> can<00:10:55.020> not<00:10:55.470> only<00:10:55.590> define 00:10:55.970 --> 00:10:55.980 align:start position:0% plus 1 over 2 so we can not only define 00:10:55.980 --> 00:10:58.070 align:start position:0% plus 1 over 2 so we can not only define programs<00:10:56.430> but<00:10:56.730> we<00:10:56.880> can<00:10:57.030> write<00:10:57.420> verification 00:10:58.070 --> 00:10:58.080 align:start position:0% programs but we can write verification 00:10:58.080 --> 00:11:00.230 align:start position:0% programs but we can write verification goals<00:10:58.290> and<00:10:58.560> what<00:10:58.890> we've<00:10:59.040> done<00:10:59.190> here<00:10:59.250> is<00:10:59.490> we've 00:11:00.230 --> 00:11:00.240 align:start position:0% goals and what we've done here is we've 00:11:00.240 --> 00:11:02.660 align:start position:0% goals and what we've done here is we've asked<00:11:00.450> Timandra<00:11:00.930> tactical<00:11:01.590> part<00:11:01.950> of<00:11:02.040> me<00:11:02.130> to 00:11:02.660 --> 00:11:02.670 align:start position:0% asked Timandra tactical part of me to 00:11:02.670 --> 00:11:04.250 align:start position:0% asked Timandra tactical part of me to actually<00:11:02.760> verify<00:11:03.120> this<00:11:03.480> statement<00:11:04.110> on<00:11:04.170> the 00:11:04.250 --> 00:11:04.260 align:start position:0% actually verify this statement on the 00:11:04.260 --> 00:11:06.590 align:start position:0% actually verify this statement on the left<00:11:04.470> to<00:11:04.620> verify<00:11:05.100> we<00:11:05.310> named<00:11:05.550> it<00:11:05.640> Gauss<00:11:05.850> we 00:11:06.590 --> 00:11:06.600 align:start position:0% left to verify we named it Gauss we 00:11:06.600 --> 00:11:08.420 align:start position:0% left to verify we named it Gauss we asked<00:11:06.780> amarjit<00:11:07.110> to<00:11:07.230> prove<00:11:07.530> for<00:11:08.040> every 00:11:08.420 --> 00:11:08.430 align:start position:0% asked amarjit to prove for every 00:11:08.430 --> 00:11:10.820 align:start position:0% asked amarjit to prove for every possible<00:11:08.880> input<00:11:09.060> in<00:11:09.510> if<00:11:09.720> n<00:11:10.350> is<00:11:10.380> greater<00:11:10.620> than 00:11:10.820 --> 00:11:10.830 align:start position:0% possible input in if n is greater than 00:11:10.830 --> 00:11:12.860 align:start position:0% possible input in if n is greater than or<00:11:10.920> equal<00:11:11.100> to<00:11:11.130> 0<00:11:11.430> then<00:11:11.790> the<00:11:11.910> sum<00:11:12.120> of<00:11:12.270> n<00:11:12.420> is<00:11:12.570> n 00:11:12.860 --> 00:11:12.870 align:start position:0% or equal to 0 then the sum of n is n 00:11:12.870 --> 00:11:16.070 align:start position:0% or equal to 0 then the sum of n is n times<00:11:13.050> n<00:11:13.230> plus<00:11:13.260> 1<00:11:13.620> over<00:11:13.650> 2<00:11:13.980> so<00:11:14.970> Ahmad<00:11:15.780> rhythm 00:11:16.070 --> 00:11:16.080 align:start position:0% times n plus 1 over 2 so Ahmad rhythm 00:11:16.080 --> 00:11:17.780 align:start position:0% times n plus 1 over 2 so Ahmad rhythm goes<00:11:16.230> and<00:11:16.440> does<00:11:16.500> a<00:11:16.560> proof<00:11:16.800> by<00:11:16.830> induction<00:11:17.010> and 00:11:17.780 --> 00:11:17.790 align:start position:0% goes and does a proof by induction and 00:11:17.790 --> 00:11:20.720 align:start position:0% goes and does a proof by induction and etc<00:11:18.750> we<00:11:19.320> can<00:11:19.470> see<00:11:19.620> a<00:11:19.650> trace<00:11:19.950> of<00:11:20.130> that<00:11:20.310> proof 00:11:20.720 --> 00:11:20.730 align:start position:0% etc we can see a trace of that proof 00:11:20.730 --> 00:11:23.450 align:start position:0% etc we can see a trace of that proof great<00:11:21.630> proof<00:11:22.380> by<00:11:22.530> induction<00:11:22.560> as<00:11:23.070> you<00:11:23.160> might<00:11:23.310> do 00:11:23.450 --> 00:11:23.460 align:start position:0% great proof by induction as you might do 00:11:23.460 --> 00:11:25.100 align:start position:0% great proof by induction as you might do by<00:11:23.610> hand<00:11:23.820> and<00:11:24.090> ultimately<00:11:24.420> has<00:11:24.600> to<00:11:24.630> do<00:11:24.840> some 00:11:25.100 --> 00:11:25.110 align:start position:0% by hand and ultimately has to do some 00:11:25.110 --> 00:11:27.450 align:start position:0% by hand and ultimately has to do some symbolic<00:11:25.740> rewriting 00:11:27.450 --> 00:11:27.460 align:start position:0% symbolic rewriting 00:11:27.460 --> 00:11:30.100 align:start position:0% symbolic rewriting that<00:11:28.460> proof<00:11:28.730> can<00:11:28.880> be<00:11:28.910> exported<00:11:29.360> can<00:11:29.990> be 00:11:30.100 --> 00:11:30.110 align:start position:0% that proof can be exported can be 00:11:30.110 --> 00:11:31.660 align:start position:0% that proof can be exported can be verified<00:11:30.380> by<00:11:30.560> an<00:11:30.800> open<00:11:31.010> source<00:11:31.190> proof<00:11:31.460> checker 00:11:31.660 --> 00:11:31.670 align:start position:0% verified by an open source proof checker 00:11:31.670 --> 00:11:34.210 align:start position:0% verified by an open source proof checker so<00:11:31.910> you<00:11:32.000> don't<00:11:32.149> have<00:11:32.270> to<00:11:32.390> trust<00:11:32.600> it<00:11:32.920> but<00:11:33.920> now 00:11:34.210 --> 00:11:34.220 align:start position:0% so you don't have to trust it but now 00:11:34.220 --> 00:11:36.160 align:start position:0% so you don't have to trust it but now what<00:11:34.850> happens<00:11:35.149> more<00:11:35.270> often<00:11:35.480> of<00:11:35.720> course<00:11:35.930> is<00:11:36.080> we 00:11:36.160 --> 00:11:36.170 align:start position:0% what happens more often of course is we 00:11:36.170 --> 00:11:38.740 align:start position:0% what happens more often of course is we have<00:11:36.260> bugs<00:11:36.470> in<00:11:36.589> our<00:11:36.680> code<00:11:36.950> so<00:11:37.760> instead<00:11:38.480> here 00:11:38.740 --> 00:11:38.750 align:start position:0% have bugs in our code so instead here 00:11:38.750 --> 00:11:40.990 align:start position:0% have bugs in our code so instead here I've<00:11:38.870> swapped<00:11:39.200> a<00:11:39.440> plus<00:11:39.649> for<00:11:39.890> a<00:11:39.950> minus<00:11:40.339> right 00:11:40.990 --> 00:11:41.000 align:start position:0% I've swapped a plus for a minus right 00:11:41.000 --> 00:11:43.510 align:start position:0% I've swapped a plus for a minus right and<00:11:41.240> I'm<00:11:41.570> asking<00:11:41.810> a<00:11:42.080> mantra<00:11:42.410> instead<00:11:42.800> to<00:11:43.310> prove 00:11:43.510 --> 00:11:43.520 align:start position:0% and I'm asking a mantra instead to prove 00:11:43.520 --> 00:11:44.829 align:start position:0% and I'm asking a mantra instead to prove that<00:11:43.550> some<00:11:43.940> event<00:11:44.209> is<00:11:44.330> equal<00:11:44.570> to<00:11:44.630> something 00:11:44.829 --> 00:11:44.839 align:start position:0% that some event is equal to something 00:11:44.839 --> 00:11:46.449 align:start position:0% that some event is equal to something really<00:11:45.320> that<00:11:45.440> it's<00:11:45.560> not<00:11:45.649> equal<00:11:45.920> to<00:11:46.040> and<00:11:46.250> a 00:11:46.449 --> 00:11:46.459 align:start position:0% really that it's not equal to and a 00:11:46.459 --> 00:11:47.829 align:start position:0% really that it's not equal to and a mantra<00:11:46.700> comes<00:11:46.880> back<00:11:47.060> and<00:11:47.209> gives<00:11:47.300> me<00:11:47.510> a<00:11:47.540> counter 00:11:47.829 --> 00:11:47.839 align:start position:0% mantra comes back and gives me a counter 00:11:47.839 --> 00:11:50.949 align:start position:0% mantra comes back and gives me a counter example<00:11:48.010> so<00:11:49.010> that's<00:11:49.250> a<00:11:49.430> super<00:11:50.240> simple<00:11:50.480> example 00:11:50.949 --> 00:11:50.959 align:start position:0% example so that's a super simple example 00:11:50.959 --> 00:11:53.019 align:start position:0% example so that's a super simple example but<00:11:51.529> let<00:11:52.100> me<00:11:52.130> show<00:11:52.399> you<00:11:52.459> something<00:11:52.820> more 00:11:53.019 --> 00:11:53.029 align:start position:0% but let me show you something more 00:11:53.029 --> 00:11:56.590 align:start position:0% but let me show you something more complex<00:11:53.510> so<00:11:54.380> I<00:11:55.000> believe<00:11:56.000> I<00:11:56.089> don't<00:11:56.300> have<00:11:56.420> too 00:11:56.590 --> 00:11:56.600 align:start position:0% complex so I believe I don't have too 00:11:56.600 --> 00:11:58.420 align:start position:0% complex so I believe I don't have too much<00:11:56.750> time<00:11:56.810> but<00:11:57.680> for<00:11:57.800> instance<00:11:58.070> here's<00:11:58.250> an 00:11:58.420 --> 00:11:58.430 align:start position:0% much time but for instance here's an 00:11:58.430 --> 00:12:00.490 align:start position:0% much time but for instance here's an example<00:11:58.700> where<00:11:59.029> I'm<00:11:59.209> effectively<00:11:59.630> defining 00:12:00.490 --> 00:12:00.500 align:start position:0% example where I'm effectively defining 00:12:00.500 --> 00:12:02.740 align:start position:0% example where I'm effectively defining algebraic<00:12:00.920> data<00:12:01.130> types<00:12:01.490> and<00:12:01.790> I'm<00:12:02.330> asking<00:12:02.480> a 00:12:02.740 --> 00:12:02.750 align:start position:0% algebraic data types and I'm asking a 00:12:02.750 --> 00:12:04.600 align:start position:0% algebraic data types and I'm asking a moderate<00:12:03.080> to<00:12:03.170> compute<00:12:03.529> some<00:12:03.770> complex<00:12:04.250> counter 00:12:04.600 --> 00:12:04.610 align:start position:0% moderate to compute some complex counter 00:12:04.610 --> 00:12:06.970 align:start position:0% moderate to compute some complex counter examples<00:12:05.029> for<00:12:05.209> me<00:12:05.330> and<00:12:05.510> again<00:12:06.470> you<00:12:06.830> know<00:12:06.920> it 00:12:06.970 --> 00:12:06.980 align:start position:0% examples for me and again you know it 00:12:06.980 --> 00:12:08.410 align:start position:0% examples for me and again you know it comes<00:12:07.130> back<00:12:07.370> and<00:12:07.610> always<00:12:07.790> the<00:12:08.149> counter 00:12:08.410 --> 00:12:08.420 align:start position:0% comes back and always the counter 00:12:08.420 --> 00:12:10.930 align:start position:0% comes back and always the counter examples<00:12:08.839> it<00:12:08.990> gives<00:12:09.200> me<00:12:09.380> those<00:12:09.830> are<00:12:10.010> valid<00:12:10.250> IML 00:12:10.930 --> 00:12:10.940 align:start position:0% examples it gives me those are valid IML 00:12:10.940 --> 00:12:12.910 align:start position:0% examples it gives me those are valid IML they're<00:12:11.240> valid<00:12:11.480> o<00:12:11.720> camel<00:12:12.110> objects<00:12:12.649> they<00:12:12.800> can 00:12:12.910 --> 00:12:12.920 align:start position:0% they're valid o camel objects they can 00:12:12.920 --> 00:12:14.260 align:start position:0% they're valid o camel objects they can be<00:12:13.010> reflected<00:12:13.490> into<00:12:13.610> the<00:12:13.760> language<00:12:13.910> and 00:12:14.260 --> 00:12:14.270 align:start position:0% be reflected into the language and 00:12:14.270 --> 00:12:18.550 align:start position:0% be reflected into the language and computed<00:12:14.959> with<00:12:15.100> so<00:12:16.100> the<00:12:16.250> same<00:12:16.550> idea<00:12:17.390> now<00:12:18.020> can 00:12:18.550 --> 00:12:18.560 align:start position:0% computed with so the same idea now can 00:12:18.560 --> 00:12:20.110 align:start position:0% computed with so the same idea now can actually<00:12:18.890> be<00:12:19.040> scaled<00:12:19.399> to<00:12:19.580> reason<00:12:20.060> about 00:12:20.110 --> 00:12:20.120 align:start position:0% actually be scaled to reason about 00:12:20.120 --> 00:12:22.960 align:start position:0% actually be scaled to reason about financial<00:12:20.810> algorithms<00:12:21.399> so<00:12:22.399> for<00:12:22.580> instance<00:12:22.640> we 00:12:22.960 --> 00:12:22.970 align:start position:0% financial algorithms so for instance we 00:12:22.970 --> 00:12:25.269 align:start position:0% financial algorithms so for instance we can<00:12:23.120> take<00:12:23.300> the<00:12:23.480> design<00:12:23.750> of<00:12:23.779> a<00:12:23.990> dark<00:12:24.200> pool<00:12:24.440> which 00:12:25.269 --> 00:12:25.279 align:start position:0% can take the design of a dark pool which 00:12:25.279 --> 00:12:28.300 align:start position:0% can take the design of a dark pool which I<00:12:25.399> have<00:12:25.580> on<00:12:25.790> the<00:12:25.880> left<00:12:26.089> here<00:12:26.830> fairly<00:12:27.830> complex 00:12:28.300 --> 00:12:28.310 align:start position:0% I have on the left here fairly complex 00:12:28.310 --> 00:12:30.550 align:start position:0% I have on the left here fairly complex matching<00:12:28.820> logic<00:12:29.149> this<00:12:29.810> is<00:12:29.959> of<00:12:30.110> a<00:12:30.200> global 00:12:30.550 --> 00:12:30.560 align:start position:0% matching logic this is of a global 00:12:30.560 --> 00:12:32.320 align:start position:0% matching logic this is of a global investment<00:12:31.160> bank<00:12:31.339> top<00:12:31.700> five<00:12:31.880> investment 00:12:32.320 --> 00:12:32.330 align:start position:0% investment bank top five investment 00:12:32.330 --> 00:12:35.980 align:start position:0% investment bank top five investment banks<00:12:32.540> dark<00:12:32.720> pool<00:12:33.040> and<00:12:34.040> now<00:12:34.850> we<00:12:35.600> can<00:12:35.720> reason 00:12:35.980 --> 00:12:35.990 align:start position:0% banks dark pool and now we can reason 00:12:35.990 --> 00:12:37.329 align:start position:0% banks dark pool and now we can reason about<00:12:36.050> it<00:12:36.320> so<00:12:36.440> by<00:12:36.560> the<00:12:36.620> way<00:12:36.740> this<00:12:36.890> is<00:12:37.040> all<00:12:37.160> based 00:12:37.329 --> 00:12:37.339 align:start position:0% about it so by the way this is all based 00:12:37.339 --> 00:12:39.280 align:start position:0% about it so by the way this is all based on<00:12:37.550> publicly<00:12:38.089> available<00:12:38.390> information<00:12:38.630> don't 00:12:39.280 --> 00:12:39.290 align:start position:0% on publicly available information don't 00:12:39.290 --> 00:12:41.949 align:start position:0% on publicly available information don't worry<00:12:39.850> so<00:12:40.850> now<00:12:40.970> for<00:12:41.000> a<00:12:41.240> sense<00:12:41.420> i<00:12:41.510> can<00:12:41.690> ask<00:12:41.779> a 00:12:41.949 --> 00:12:41.959 align:start position:0% worry so now for a sense i can ask a 00:12:41.959 --> 00:12:44.560 align:start position:0% worry so now for a sense i can ask a mantra<00:12:42.320> yeah<00:12:42.950> is<00:12:43.220> the<00:12:43.910> order<00:12:44.209> ranking 00:12:44.560 --> 00:12:44.570 align:start position:0% mantra yeah is the order ranking 00:12:44.570 --> 00:12:47.079 align:start position:0% mantra yeah is the order ranking function<00:12:44.990> transitive<00:12:45.650> right<00:12:46.310> so<00:12:46.550> that's 00:12:47.079 --> 00:12:47.089 align:start position:0% function transitive right so that's 00:12:47.089 --> 00:12:48.510 align:start position:0% function transitive right so that's something<00:12:47.300> we<00:12:47.510> really<00:12:47.660> care<00:12:47.930> about<00:12:47.990> a 00:12:48.510 --> 00:12:48.520 align:start position:0% something we really care about a 00:12:48.520 --> 00:12:51.100 align:start position:0% something we really care about a fairness<00:12:49.520> property<00:12:50.089> so<00:12:50.540> i<00:12:50.570> can<00:12:50.750> ask<00:12:50.839> them<00:12:51.020> on 00:12:51.100 --> 00:12:51.110 align:start position:0% fairness property so i can ask them on 00:12:51.110 --> 00:12:54.220 align:start position:0% fairness property so i can ask them on through<00:12:51.290> this<00:12:51.380> question<00:12:51.830> it<00:12:52.570> has<00:12:53.570> a<00:12:53.600> model<00:12:54.110> of 00:12:54.220 --> 00:12:54.230 align:start position:0% through this question it has a model of 00:12:54.230 --> 00:12:55.810 align:start position:0% through this question it has a model of the<00:12:54.290> matching<00:12:54.680> logic<00:12:54.950> on<00:12:55.070> the<00:12:55.160> right<00:12:55.339> that's 00:12:55.810 --> 00:12:55.820 align:start position:0% the matching logic on the right that's 00:12:55.820 --> 00:12:58.360 align:start position:0% the matching logic on the right that's also<00:12:55.970> a<00:12:56.120> high-performance<00:12:57.080> simulator<00:12:57.500> and<00:12:57.740> a 00:12:58.360 --> 00:12:58.370 align:start position:0% also a high-performance simulator and a 00:12:58.370 --> 00:13:00.370 align:start position:0% also a high-performance simulator and a mantra<00:12:58.640> comes<00:12:58.850> back<00:12:59.060> and<00:12:59.300> synthesizes<00:13:00.110> for<00:13:00.290> me 00:13:00.370 --> 00:13:00.380 align:start position:0% mantra comes back and synthesizes for me 00:13:00.380 --> 00:13:02.769 align:start position:0% mantra comes back and synthesizes for me a<00:13:00.410> counter<00:13:00.740> example<00:13:00.860> so<00:13:01.490> now<00:13:01.670> i<00:13:01.700> have<00:13:01.820> concrete 00:13:02.769 --> 00:13:02.779 align:start position:0% a counter example so now i have concrete 00:13:02.779 --> 00:13:06.160 align:start position:0% a counter example so now i have concrete values<00:13:03.230> of<00:13:04.180> different<00:13:05.180> orders<00:13:05.540> effectively 00:13:06.160 --> 00:13:06.170 align:start position:0% values of different orders effectively 00:13:06.170 --> 00:13:07.480 align:start position:0% values of different orders effectively that<00:13:06.260> could<00:13:06.529> exist<00:13:06.650> in<00:13:06.920> the<00:13:07.010> book<00:13:07.220> of<00:13:07.370> this 00:13:07.480 --> 00:13:07.490 align:start position:0% that could exist in the book of this 00:13:07.490 --> 00:13:09.310 align:start position:0% that could exist in the book of this dark<00:13:07.760> pool<00:13:08.000> where<00:13:08.540> the<00:13:08.720> ranking<00:13:09.020> function 00:13:09.310 --> 00:13:09.320 align:start position:0% dark pool where the ranking function 00:13:09.320 --> 00:13:11.680 align:start position:0% dark pool where the ranking function violates<00:13:09.740> transitivity<00:13:10.250> so<00:13:11.180> that's<00:13:11.360> the<00:13:11.540> main 00:13:11.680 --> 00:13:11.690 align:start position:0% violates transitivity so that's the main 00:13:11.690 --> 00:13:14.500 align:start position:0% violates transitivity so that's the main idea<00:13:11.839> proofs<00:13:12.500> and<00:13:12.680> counter<00:13:12.920> examples<00:13:13.370> so<00:13:14.329> let 00:13:14.500 --> 00:13:14.510 align:start position:0% idea proofs and counter examples so let 00:13:14.510 --> 00:13:18.069 align:start position:0% idea proofs and counter examples so let me<00:13:14.709> quickly<00:13:15.709> cut<00:13:16.459> to<00:13:16.610> the<00:13:16.700> chase<00:13:16.730> for<00:13:17.079> athyrium 00:13:18.069 --> 00:13:18.079 align:start position:0% me quickly cut to the chase for athyrium 00:13:18.079 --> 00:13:22.769 align:start position:0% me quickly cut to the chase for athyrium so<00:13:18.920> what<00:13:19.880> we've<00:13:20.029> done<00:13:20.209> here<00:13:20.270> is<00:13:20.600> we've<00:13:21.290> taken<00:13:21.620> a 00:13:22.769 --> 00:13:22.779 align:start position:0% so what we've done here is we've taken a 00:13:22.779 --> 00:13:25.630 align:start position:0% so what we've done here is we've taken a mantra<00:13:23.779> and<00:13:23.930> we've<00:13:24.350> adapted<00:13:24.620> it<00:13:24.980> so<00:13:25.220> that<00:13:25.399> in 00:13:25.630 --> 00:13:25.640 align:start position:0% mantra and we've adapted it so that in 00:13:25.640 --> 00:13:28.150 align:start position:0% mantra and we've adapted it so that in IML<00:13:26.209> in<00:13:26.420> this<00:13:26.720> fragment<00:13:27.140> of<00:13:27.200> o<00:13:27.320> campbell<00:13:27.680> you 00:13:28.150 --> 00:13:28.160 align:start position:0% IML in this fragment of o campbell you 00:13:28.160 --> 00:13:30.970 align:start position:0% IML in this fragment of o campbell you can<00:13:28.339> directly<00:13:28.700> write<00:13:28.940> smart<00:13:29.329> contracts<00:13:29.980> so 00:13:30.970 --> 00:13:30.980 align:start position:0% can directly write smart contracts so 00:13:30.980 --> 00:13:32.949 align:start position:0% can directly write smart contracts so there's<00:13:31.850> many<00:13:32.060> things<00:13:32.149> to<00:13:32.480> talk<00:13:32.660> to<00:13:32.779> you<00:13:32.870> about 00:13:32.949 --> 00:13:32.959 align:start position:0% there's many things to talk to you about 00:13:32.959 --> 00:13:34.750 align:start position:0% there's many things to talk to you about how<00:13:33.260> we<00:13:33.320> actually<00:13:33.560> do<00:13:33.860> the<00:13:34.010> compilation<00:13:34.550> so 00:13:34.750 --> 00:13:34.760 align:start position:0% how we actually do the compilation so 00:13:34.760 --> 00:13:37.630 align:start position:0% how we actually do the compilation so right<00:13:34.940> now<00:13:34.970> we<00:13:35.750> actually<00:13:35.900> compile 00:13:37.630 --> 00:13:37.640 align:start position:0% right now we actually compile 00:13:37.640 --> 00:13:40.040 align:start position:0% right now we actually compile effectively<00:13:38.640> your<00:13:39.030> customized<00:13:39.750> smart 00:13:40.040 --> 00:13:40.050 align:start position:0% effectively your customized smart 00:13:40.050 --> 00:13:42.500 align:start position:0% effectively your customized smart contract<00:13:40.470> code<00:13:40.740> via<00:13:41.340> serpent<00:13:41.880> we<00:13:42.060> compile<00:13:42.360> it 00:13:42.500 --> 00:13:42.510 align:start position:0% contract code via serpent we compile it 00:13:42.510 --> 00:13:44.390 align:start position:0% contract code via serpent we compile it first<00:13:42.750> to<00:13:42.900> serpent<00:13:43.290> and<00:13:43.380> we<00:13:43.890> have<00:13:44.040> different 00:13:44.390 --> 00:13:44.400 align:start position:0% first to serpent and we have different 00:13:44.400 --> 00:13:45.950 align:start position:0% first to serpent and we have different encoding<00:13:44.610> mechanisms<00:13:45.270> for<00:13:45.480> how<00:13:45.570> we<00:13:45.630> encode 00:13:45.950 --> 00:13:45.960 align:start position:0% encoding mechanisms for how we encode 00:13:45.960 --> 00:13:50.060 align:start position:0% encoding mechanisms for how we encode algebraic<00:13:46.440> data<00:13:46.620> types<00:13:46.950> recursively<00:13:48.680> but<00:13:49.680> now 00:13:50.060 --> 00:13:50.070 align:start position:0% algebraic data types recursively but now 00:13:50.070 --> 00:13:51.950 align:start position:0% algebraic data types recursively but now we<00:13:50.640> have<00:13:50.790> this<00:13:50.910> smart<00:13:51.180> contract<00:13:51.600> let's<00:13:51.810> say 00:13:51.950 --> 00:13:51.960 align:start position:0% we have this smart contract let's say 00:13:51.960 --> 00:13:56.300 align:start position:0% we have this smart contract let's say for<00:13:52.290> a<00:13:53.240> crowdfunding<00:13:54.770> example<00:13:55.770> and<00:13:55.980> now<00:13:56.250> we 00:13:56.300 --> 00:13:56.310 align:start position:0% for a crowdfunding example and now we 00:13:56.310 --> 00:13:57.950 align:start position:0% for a crowdfunding example and now we can<00:13:56.520> ask<00:13:56.670> a<00:13:56.790> monitor<00:13:57.090> to<00:13:57.120> reason<00:13:57.450> about<00:13:57.510> it<00:13:57.750> so 00:13:57.950 --> 00:13:57.960 align:start position:0% can ask a monitor to reason about it so 00:13:57.960 --> 00:13:59.930 align:start position:0% can ask a monitor to reason about it so for<00:13:58.560> instance<00:13:58.620> we<00:13:58.950> just<00:13:59.130> had<00:13:59.250> a<00:13:59.280> mantra<00:13:59.640> prove 00:13:59.930 --> 00:13:59.940 align:start position:0% for instance we just had a mantra prove 00:13:59.940 --> 00:14:02.000 align:start position:0% for instance we just had a mantra prove that<00:14:00.600> in<00:14:00.870> this<00:14:01.080> smart<00:14:01.380> contract<00:14:01.830> you 00:14:02.000 --> 00:14:02.010 align:start position:0% that in this smart contract you 00:14:02.010 --> 00:14:03.740 align:start position:0% that in this smart contract you effectively<00:14:02.400> can't<00:14:02.730> jump<00:14:02.970> the<00:14:03.090> queue<00:14:03.360> in<00:14:03.630> a 00:14:03.740 --> 00:14:03.750 align:start position:0% effectively can't jump the queue in a 00:14:03.750 --> 00:14:06.350 align:start position:0% effectively can't jump the queue in a certain<00:14:03.930> sense<00:14:04.230> and<00:14:04.500> then<00:14:05.310> we<00:14:05.940> ask<00:14:06.090> another 00:14:06.350 --> 00:14:06.360 align:start position:0% certain sense and then we ask another 00:14:06.360 --> 00:14:09.200 align:start position:0% certain sense and then we ask another question<00:14:06.590> effectively<00:14:07.590> that<00:14:08.310> we<00:14:08.910> will<00:14:09.060> always 00:14:09.200 --> 00:14:09.210 align:start position:0% question effectively that we will always 00:14:09.210 --> 00:14:11.510 align:start position:0% question effectively that we will always get<00:14:09.480> our<00:14:09.630> money<00:14:09.870> back<00:14:09.960> if<00:14:10.380> we<00:14:10.440> come<00:14:11.040> in<00:14:11.190> after<00:14:11.490> a 00:14:11.510 --> 00:14:11.520 align:start position:0% get our money back if we come in after a 00:14:11.520 --> 00:14:13.190 align:start position:0% get our money back if we come in after a certain<00:14:11.760> time<00:14:11.910> out<00:14:12.240> and<00:14:12.450> a<00:14:12.570> modular<00:14:12.840> computes 00:14:13.190 --> 00:14:13.200 align:start position:0% certain time out and a modular computes 00:14:13.200 --> 00:14:14.690 align:start position:0% certain time out and a modular computes for<00:14:13.380> us<00:14:13.440> a<00:14:13.560> counter<00:14:13.800> example<00:14:13.920> where<00:14:14.520> that 00:14:14.690 --> 00:14:14.700 align:start position:0% for us a counter example where that 00:14:14.700 --> 00:14:18.860 align:start position:0% for us a counter example where that fails<00:14:14.960> so<00:14:15.960> that's<00:14:16.890> the<00:14:17.100> big<00:14:17.220> idea<00:14:17.370> I<00:14:18.060> think<00:14:18.810> I 00:14:18.860 --> 00:14:18.870 align:start position:0% fails so that's the big idea I think I 00:14:18.870 --> 00:14:20.660 align:start position:0% fails so that's the big idea I think I need<00:14:19.050> to<00:14:19.080> end<00:14:19.320> here<00:14:19.710> but<00:14:20.310> we<00:14:20.400> have<00:14:20.550> these 00:14:20.660 --> 00:14:20.670 align:start position:0% need to end here but we have these 00:14:20.670 --> 00:14:22.490 align:start position:0% need to end here but we have these different<00:14:21.030> modes<00:14:21.330> effectively<00:14:21.990> you<00:14:22.200> can<00:14:22.230> go 00:14:22.490 --> 00:14:22.500 align:start position:0% different modes effectively you can go 00:14:22.500 --> 00:14:25.370 align:start position:0% different modes effectively you can go IML<00:14:23.250> directly<00:14:23.910> to<00:14:24.000> bytecode<00:14:24.210> by<00:14:24.810> a<00:14:24.840> serpent 00:14:25.370 --> 00:14:25.380 align:start position:0% IML directly to bytecode by a serpent 00:14:25.380 --> 00:14:28.790 align:start position:0% IML directly to bytecode by a serpent reason<00:14:26.010> about<00:14:26.220> your<00:14:26.400> IML<00:14:26.790> or<00:14:27.000> we<00:14:27.990> can<00:14:28.170> use<00:14:28.230> our 00:14:28.790 --> 00:14:28.800 align:start position:0% reason about your IML or we can use our 00:14:28.800 --> 00:14:32.810 align:start position:0% reason about your IML or we can use our etherium<00:14:29.580> to<00:14:29.700> IML<00:14:30.150> verified<00:14:30.840> decompiler<00:14:31.820> so 00:14:32.810 --> 00:14:32.820 align:start position:0% etherium to IML verified decompiler so 00:14:32.820 --> 00:14:35.720 align:start position:0% etherium to IML verified decompiler so sign<00:14:33.450> up<00:14:33.480> please<00:14:33.930> if<00:14:34.110> you'd<00:14:34.230> like<00:14:34.350> to<00:14:34.590> join<00:14:35.070> the 00:14:35.720 --> 00:14:35.730 align:start position:0% sign up please if you'd like to join the 00:14:35.730 --> 00:14:46.430 align:start position:0% sign up please if you'd like to join the private<00:14:36.060> alpha<00:14:36.360> and<00:14:36.800> thank<00:14:37.800> you<00:14:37.860> very<00:14:38.010> much 00:14:46.430 --> 00:14:46.440 align:start position:0% 00:14:46.440 --> 00:14:53.370 align:start position:0% okay<00:14:47.760> okay<00:14:48.760> oh<00:14:51.209> ok<00:14:52.209> well<00:14:52.570> that's<00:14:52.660> okay<00:14:52.930> I<00:14:53.110> mean 00:14:53.370 --> 00:14:53.380 align:start position:0% okay okay oh ok well that's okay I mean 00:14:53.380 --> 00:14:58.920 align:start position:0% okay okay oh ok well that's okay I mean if<00:14:53.709> there's<00:14:53.950> any<00:14:54.070> questions<00:14:54.480> okay<00:14:55.480> yes<00:14:57.720> so<00:14:58.720> are 00:14:58.920 --> 00:14:58.930 align:start position:0% if there's any questions okay yes so are 00:14:58.930 --> 00:15:00.930 align:start position:0% if there's any questions okay yes so are you<00:14:59.050> saying<00:14:59.230> we<00:14:59.380> can<00:14:59.529> write<00:14:59.709> smart<00:15:00.430> contracts 00:15:00.930 --> 00:15:00.940 align:start position:0% you saying we can write smart contracts 00:15:00.940 --> 00:15:04.590 align:start position:0% you saying we can write smart contracts in<00:15:01.060> oh<00:15:01.300> come<00:15:01.540> in<00:15:02.050> I<00:15:02.680> exactly<00:15:03.459> in<00:15:03.610> IML<00:15:04.000> so<00:15:04.180> I<00:15:04.209> ml 00:15:04.590 --> 00:15:04.600 align:start position:0% in oh come in I exactly in IML so I ml 00:15:04.600 --> 00:15:07.800 align:start position:0% in oh come in I exactly in IML so I ml it's<00:15:04.959> not<00:15:05.140> all<00:15:05.320> evoke<00:15:05.589> camel<00:15:06.000> but<00:15:07.000> it's<00:15:07.180> you 00:15:07.800 --> 00:15:07.810 align:start position:0% it's not all evoke camel but it's you 00:15:07.810 --> 00:15:10.650 align:start position:0% it's not all evoke camel but it's you know<00:15:07.860> polymorphic<00:15:08.860> hemming<00:15:09.370> milner<00:15:09.670> fragment 00:15:10.650 --> 00:15:10.660 align:start position:0% know polymorphic hemming milner fragment 00:15:10.660 --> 00:15:12.449 align:start position:0% know polymorphic hemming milner fragment of<00:15:10.779> o<00:15:10.899> camel<00:15:11.290> for<00:15:11.860> instance<00:15:12.010> it<00:15:12.190> doesn't 00:15:12.449 --> 00:15:12.459 align:start position:0% of o camel for instance it doesn't 00:15:12.459 --> 00:15:14.490 align:start position:0% of o camel for instance it doesn't support<00:15:12.670> exceptions<00:15:13.209> so<00:15:13.750> that's<00:15:13.930> a<00:15:14.110> that's<00:15:14.350> a 00:15:14.490 --> 00:15:14.500 align:start position:0% support exceptions so that's a that's a 00:15:14.500 --> 00:15:16.050 align:start position:0% support exceptions so that's a that's a fundamental<00:15:14.680> difference<00:15:15.040> but<00:15:15.700> instead<00:15:15.940> of 00:15:16.050 --> 00:15:16.060 align:start position:0% fundamental difference but instead of 00:15:16.060 --> 00:15:17.760 align:start position:0% fundamental difference but instead of exceptions<00:15:16.540> you<00:15:16.720> use<00:15:16.959> you<00:15:17.380> know<00:15:17.470> things<00:15:17.680> like 00:15:17.760 --> 00:15:17.770 align:start position:0% exceptions you use you know things like 00:15:17.770 --> 00:15:20.940 align:start position:0% exceptions you use you know things like option<00:15:18.130> types<00:15:18.390> yeah<00:15:19.390> but<00:15:19.690> yes<00:15:19.839> that<00:15:20.080> is<00:15:20.709> pretty 00:15:20.940 --> 00:15:20.950 align:start position:0% option types yeah but yes that is pretty 00:15:20.950 --> 00:15:26.810 align:start position:0% option types yeah but yes that is pretty awesome<00:15:21.130> oh<00:15:21.550> thank<00:15:22.149> you<00:15:25.110> but<00:15:26.110> part<00:15:26.440> of<00:15:26.500> me<00:15:26.560> it's 00:15:26.810 --> 00:15:26.820 align:start position:0% awesome oh thank you but part of me it's 00:15:26.820 --> 00:15:29.790 align:start position:0% awesome oh thank you but part of me it's not<00:15:27.820> it's<00:15:28.390> not<00:15:28.510> so<00:15:28.839> effectively<00:15:29.440> we<00:15:29.620> have<00:15:29.770> a 00:15:29.790 --> 00:15:29.800 align:start position:0% not it's not so effectively we have a 00:15:29.800 --> 00:15:33.240 align:start position:0% not it's not so effectively we have a reasoning<00:15:30.520> as<00:15:30.640> a<00:15:30.670> service<00:15:31.149> API<00:15:31.980> we<00:15:32.980> have<00:15:33.130> an 00:15:33.240 --> 00:15:33.250 align:start position:0% reasoning as a service API we have an 00:15:33.250 --> 00:15:35.220 align:start position:0% reasoning as a service API we have an online<00:15:33.370> web<00:15:33.730> interface<00:15:34.149> and<00:15:34.420> we<00:15:34.630> have<00:15:34.779> an<00:15:34.930> open 00:15:35.220 --> 00:15:35.230 align:start position:0% online web interface and we have an open 00:15:35.230 --> 00:15:37.139 align:start position:0% online web interface and we have an open source<00:15:35.500> proof<00:15:35.800> checker<00:15:36.070> so<00:15:36.730> you<00:15:36.790> can<00:15:37.000> always 00:15:37.139 --> 00:15:37.149 align:start position:0% source proof checker so you can always 00:15:37.149 --> 00:15:39.540 align:start position:0% source proof checker so you can always you<00:15:37.600> don't<00:15:37.779> have<00:15:37.930> to<00:15:38.050> trust<00:15:38.290> the<00:15:38.529> proofs<00:15:38.860> the 00:15:39.540 --> 00:15:39.550 align:start position:0% you don't have to trust the proofs the 00:15:39.550 --> 00:15:40.949 align:start position:0% you don't have to trust the proofs the hard<00:15:39.700> part<00:15:39.850> is<00:15:39.910> finding<00:15:40.089> the<00:15:40.300> proofs<00:15:40.600> you<00:15:40.870> know 00:15:40.949 --> 00:15:40.959 align:start position:0% hard part is finding the proofs you know 00:15:40.959 --> 00:15:43.769 align:start position:0% hard part is finding the proofs you know the<00:15:41.080> easy<00:15:41.230> part<00:15:41.529> is<00:15:41.620> checking<00:15:41.830> the<00:15:41.950> proofs<00:15:42.779> so 00:15:43.769 --> 00:15:43.779 align:start position:0% the easy part is checking the proofs so 00:15:43.779 --> 00:15:46.079 align:start position:0% the easy part is checking the proofs so currently<00:15:44.170> it's<00:15:44.500> not<00:15:44.709> open<00:15:45.610> source<00:15:45.850> though 00:15:46.079 --> 00:15:46.089 align:start position:0% currently it's not open source though 00:15:46.089 --> 00:15:47.790 align:start position:0% currently it's not open source though I'm<00:15:46.240> sure<00:15:46.600> we'll<00:15:46.750> open<00:15:46.870> source<00:15:47.200> pieces<00:15:47.589> of<00:15:47.709> it 00:15:47.790 --> 00:15:47.800 align:start position:0% I'm sure we'll open source pieces of it 00:15:47.800 --> 00:15:56.990 align:start position:0% I'm sure we'll open source pieces of it over<00:15:47.980> time 00:15:56.990 --> 00:15:57.000 align:start position:0% 00:15:57.000 --> 00:15:59.700 align:start position:0% do<00:15:58.000> you<00:15:58.240> mean<00:15:58.360> use<00:15:58.840> a<00:15:58.870> mantra<00:15:59.260> to<00:15:59.410> reason<00:15:59.650> about 00:15:59.700 --> 00:15:59.710 align:start position:0% do you mean use a mantra to reason about 00:15:59.710 --> 00:16:01.550 align:start position:0% do you mean use a mantra to reason about a<00:15:59.860> mantra<00:16:00.220> yeah<00:16:00.580> yeah<00:16:00.910> it's<00:16:01.090> a<00:16:01.180> great<00:16:01.360> question 00:16:01.550 --> 00:16:01.560 align:start position:0% a mantra yeah yeah it's a great question 00:16:01.560 --> 00:16:05.430 align:start position:0% a mantra yeah yeah it's a great question so<00:16:03.000> there's<00:16:04.000> there's<00:16:04.270> you<00:16:04.840> know<00:16:04.870> sort<00:16:05.410> of 00:16:05.430 --> 00:16:05.440 align:start position:0% so there's there's you know sort of 00:16:05.440 --> 00:16:06.960 align:start position:0% so there's there's you know sort of architecture<00:16:06.010> of<00:16:06.040> a<00:16:06.220> mantra<00:16:06.550> there's<00:16:06.760> some 00:16:06.960 --> 00:16:06.970 align:start position:0% architecture of a mantra there's some 00:16:06.970 --> 00:16:09.180 align:start position:0% architecture of a mantra there's some bootstrapping<00:16:07.480> in<00:16:08.230> a<00:16:08.350> mantra<00:16:08.680> that<00:16:08.830> is<00:16:09.010> not 00:16:09.180 --> 00:16:09.190 align:start position:0% bootstrapping in a mantra that is not 00:16:09.190 --> 00:16:10.650 align:start position:0% bootstrapping in a mantra that is not written<00:16:09.430> in<00:16:09.580> a<00:16:09.640> mantra<00:16:10.000> that's<00:16:10.270> written<00:16:10.480> in 00:16:10.650 --> 00:16:10.660 align:start position:0% written in a mantra that's written in 00:16:10.660 --> 00:16:13.860 align:start position:0% written in a mantra that's written in let's<00:16:10.960> say<00:16:11.080> raw<00:16:11.260> Oh<00:16:11.650> camel<00:16:12.010> see<00:16:12.640> but<00:16:13.540> then<00:16:13.660> most 00:16:13.860 --> 00:16:13.870 align:start position:0% let's say raw Oh camel see but then most 00:16:13.870 --> 00:16:15.330 align:start position:0% let's say raw Oh camel see but then most of<00:16:14.050> a<00:16:14.140> mantra<00:16:14.530> actually<00:16:14.920> is<00:16:15.010> written<00:16:15.220> in<00:16:15.310> a 00:16:15.330 --> 00:16:15.340 align:start position:0% of a mantra actually is written in a 00:16:15.340 --> 00:16:17.460 align:start position:0% of a mantra actually is written in a mantra<00:16:15.640> after<00:16:16.090> this<00:16:16.210> bootstrapping<00:16:16.690> so<00:16:17.350> we've 00:16:17.460 --> 00:16:17.470 align:start position:0% mantra after this bootstrapping so we've 00:16:17.470 --> 00:16:19.440 align:start position:0% mantra after this bootstrapping so we've actually<00:16:17.620> done<00:16:17.980> some<00:16:18.310> self<00:16:18.580> verifications<00:16:19.240> I 00:16:19.440 --> 00:16:19.450 align:start position:0% actually done some self verifications I 00:16:19.450 --> 00:16:21.210 align:start position:0% actually done some self verifications I mean<00:16:20.260> you<00:16:20.500> know<00:16:20.590> you<00:16:20.620> always<00:16:20.830> have<00:16:21.070> these 00:16:21.210 --> 00:16:21.220 align:start position:0% mean you know you always have these 00:16:21.220 --> 00:16:23.130 align:start position:0% mean you know you always have these fundamental<00:16:21.910> meta<00:16:22.120> mathematical<00:16:22.720> results 00:16:23.130 --> 00:16:23.140 align:start position:0% fundamental meta mathematical results 00:16:23.140 --> 00:16:25.170 align:start position:0% fundamental meta mathematical results that<00:16:23.710> if<00:16:23.800> you<00:16:23.890> want<00:16:24.070> to<00:16:24.130> prove<00:16:24.370> ultimately 00:16:25.170 --> 00:16:25.180 align:start position:0% that if you want to prove ultimately 00:16:25.180 --> 00:16:27.090 align:start position:0% that if you want to prove ultimately consistency<00:16:25.900> of<00:16:25.990> your<00:16:26.140> own<00:16:26.230> system<00:16:26.620> you 00:16:27.090 --> 00:16:27.100 align:start position:0% consistency of your own system you 00:16:27.100 --> 00:16:28.770 align:start position:0% consistency of your own system you effectively<00:16:27.490> need<00:16:27.730> to<00:16:27.850> add<00:16:27.970> you<00:16:28.660> know 00:16:28.770 --> 00:16:28.780 align:start position:0% effectively need to add you know 00:16:28.780 --> 00:16:30.630 align:start position:0% effectively need to add you know something<00:16:29.170> like<00:16:29.320> trans<00:16:29.620> finite<00:16:29.950> induction<00:16:30.280> up 00:16:30.630 --> 00:16:30.640 align:start position:0% something like trans finite induction up 00:16:30.640 --> 00:16:32.970 align:start position:0% something like trans finite induction up to<00:16:30.910> a<00:16:30.940> larger<00:16:31.270> ordinal<00:16:31.630> so<00:16:32.140> actually<00:16:32.230> a<00:16:32.530> mantra 00:16:32.970 --> 00:16:32.980 align:start position:0% to a larger ordinal so actually a mantra 00:16:32.980 --> 00:16:35.070 align:start position:0% to a larger ordinal so actually a mantra is<00:16:33.040> logic<00:16:33.490> it's<00:16:33.970> related<00:16:34.330> to<00:16:34.360> a<00:16:34.510> logic<00:16:34.900> called 00:16:35.070 --> 00:16:35.080 align:start position:0% is logic it's related to a logic called 00:16:35.080 --> 00:16:37.110 align:start position:0% is logic it's related to a logic called primitive<00:16:35.260> recursive<00:16:35.680> arithmetic<00:16:36.400> of<00:16:36.610> Scala 00:16:37.110 --> 00:16:37.120 align:start position:0% primitive recursive arithmetic of Scala 00:16:37.120 --> 00:16:39.300 align:start position:0% primitive recursive arithmetic of Scala but<00:16:37.420> it's<00:16:37.540> typed<00:16:37.870> and<00:16:38.230> but<00:16:38.890> then<00:16:39.010> we<00:16:39.130> have 00:16:39.300 --> 00:16:39.310 align:start position:0% but it's typed and but then we have 00:16:39.310 --> 00:16:40.650 align:start position:0% but it's typed and but then we have transplant<00:16:39.790> out<00:16:39.880> induction<00:16:40.180> up<00:16:40.480> to<00:16:40.570> an 00:16:40.650 --> 00:16:40.660 align:start position:0% transplant out induction up to an 00:16:40.660 --> 00:16:42.990 align:start position:0% transplant out induction up to an ordinal<00:16:41.020> called<00:16:41.200> epsilon<00:16:41.380> zero<00:16:41.860> so<00:16:42.580> basically 00:16:42.990 --> 00:16:43.000 align:start position:0% ordinal called epsilon zero so basically 00:16:43.000 --> 00:16:45.900 align:start position:0% ordinal called epsilon zero so basically that<00:16:43.030> means<00:16:43.180> we<00:16:43.660> can<00:16:43.840> you<00:16:44.320> know<00:16:44.910> synthesized 00:16:45.900 --> 00:16:45.910 align:start position:0% that means we can you know synthesized 00:16:45.910 --> 00:16:48.840 align:start position:0% that means we can you know synthesized in<00:16:46.390> do<00:16:47.020> termination<00:16:47.650> proofs<00:16:47.950> of<00:16:48.220> functions 00:16:48.840 --> 00:16:48.850 align:start position:0% in do termination proofs of functions 00:16:48.850 --> 00:16:50.880 align:start position:0% in do termination proofs of functions that<00:16:48.940> you<00:16:49.330> know<00:16:49.570> effectively<00:16:50.290> recurse<00:16:50.650> in 00:16:50.880 --> 00:16:50.890 align:start position:0% that you know effectively recurse in 00:16:50.890 --> 00:16:54.900 align:start position:0% that you know effectively recurse in some<00:16:51.070> complex<00:16:51.370> ways<00:16:53.040> but<00:16:54.040> so<00:16:54.550> what<00:16:54.700> you<00:16:54.790> would 00:16:54.900 --> 00:16:54.910 align:start position:0% some complex ways but so what you would 00:16:54.910 --> 00:16:56.070 align:start position:0% some complex ways but so what you would have<00:16:54.940> to<00:16:55.120> do<00:16:55.210> because<00:16:55.330> we<00:16:55.630> already<00:16:55.750> have<00:16:55.960> that 00:16:56.070 --> 00:16:56.080 align:start position:0% have to do because we already have that 00:16:56.080 --> 00:16:57.960 align:start position:0% have to do because we already have that strong<00:16:56.380> ordinal<00:16:56.860> in<00:16:56.980> the<00:16:57.070> logic<00:16:57.400> you'd<00:16:57.850> have 00:16:57.960 --> 00:16:57.970 align:start position:0% strong ordinal in the logic you'd have 00:16:57.970 --> 00:17:00.300 align:start position:0% strong ordinal in the logic you'd have to<00:16:58.030> add<00:16:58.270> a<00:16:58.590> transaction<00:16:59.590> principle<00:16:59.980> up<00:17:00.130> to<00:17:00.280> a 00:17:00.300 --> 00:17:00.310 align:start position:0% to add a transaction principle up to a 00:17:00.310 --> 00:17:03.510 align:start position:0% to add a transaction principle up to a bigger<00:17:00.820> ordinal<00:17:01.680> but<00:17:02.680> you<00:17:02.770> can<00:17:02.920> you<00:17:03.310> know<00:17:03.400> so 00:17:03.510 --> 00:17:03.520 align:start position:0% bigger ordinal but you can you know so 00:17:03.520 --> 00:17:05.070 align:start position:0% bigger ordinal but you can you know so proof<00:17:03.730> theorists<00:17:04.240> have<00:17:04.480> have<00:17:04.720> isolated 00:17:05.070 --> 00:17:05.080 align:start position:0% proof theorists have have isolated 00:17:05.080 --> 00:17:07.200 align:start position:0% proof theorists have have isolated effectively<00:17:06.010> the<00:17:06.220> ordinal<00:17:06.550> analysis<00:17:07.030> of 00:17:07.200 --> 00:17:07.210 align:start position:0% effectively the ordinal analysis of 00:17:07.210 --> 00:17:09.600 align:start position:0% effectively the ordinal analysis of theories<00:17:07.510> like<00:17:07.660> this<00:17:08.160> so<00:17:09.160> you<00:17:09.220> could<00:17:09.370> do<00:17:09.490> it 00:17:09.600 --> 00:17:09.610 align:start position:0% theories like this so you could do it 00:17:09.610 --> 00:17:10.950 align:start position:0% theories like this so you could do it and<00:17:09.730> actually<00:17:09.910> try<00:17:10.330> to<00:17:10.390> prove<00:17:10.630> soundness 00:17:10.950 --> 00:17:10.960 align:start position:0% and actually try to prove soundness 00:17:10.960 --> 00:17:13.130 align:start position:0% and actually try to prove soundness properties<00:17:11.470> of<00:17:11.620> a<00:17:11.680> mandra<00:17:11.980> as<00:17:12.100> a<00:17:12.190> whole<00:17:12.370> but 00:17:13.130 --> 00:17:13.140 align:start position:0% properties of a mandra as a whole but 00:17:13.140 --> 00:17:17.280 align:start position:0% properties of a mandra as a whole but one<00:17:14.140> of<00:17:14.230> our<00:17:14.350> really<00:17:14.620> driving<00:17:16.290> philosophies 00:17:17.280 --> 00:17:17.290 align:start position:0% one of our really driving philosophies 00:17:17.290 --> 00:17:20.070 align:start position:0% one of our really driving philosophies has<00:17:17.860> been<00:17:18.160> we<00:17:18.850> always<00:17:19.030> just<00:17:19.390> want<00:17:19.660> our<00:17:19.780> proofs 00:17:20.070 --> 00:17:20.080 align:start position:0% has been we always just want our proofs 00:17:20.080 --> 00:17:22.680 align:start position:0% has been we always just want our proofs to<00:17:20.380> be<00:17:20.710> independently<00:17:21.220> checkable<00:17:21.550> as<00:17:21.820> well<00:17:22.450> so 00:17:22.680 --> 00:17:22.690 align:start position:0% to be independently checkable as well so 00:17:22.690 --> 00:17:23.970 align:start position:0% to be independently checkable as well so when<00:17:22.870> we<00:17:22.960> produce<00:17:23.170> a<00:17:23.410> proof<00:17:23.560> object 00:17:23.970 --> 00:17:23.980 align:start position:0% when we produce a proof object 00:17:23.980 --> 00:17:26.010 align:start position:0% when we produce a proof object ultimately<00:17:24.760> you<00:17:25.000> can<00:17:25.180> use<00:17:25.360> a<00:17:25.390> simple<00:17:25.810> checker 00:17:26.010 --> 00:17:26.020 align:start position:0% ultimately you can use a simple checker 00:17:26.020 --> 00:17:28.200 align:start position:0% ultimately you can use a simple checker to<00:17:26.800> check<00:17:26.980> that<00:17:27.130> proof<00:17:27.340> object<00:17:27.730> or<00:17:27.850> if<00:17:28.060> we 00:17:28.200 --> 00:17:28.210 align:start position:0% to check that proof object or if we 00:17:28.210 --> 00:17:30.030 align:start position:0% to check that proof object or if we produce<00:17:28.630> a<00:17:28.870> counter<00:17:29.140> example<00:17:29.230> it's<00:17:29.890> an 00:17:30.030 --> 00:17:30.040 align:start position:0% produce a counter example it's an 00:17:30.040 --> 00:17:32.730 align:start position:0% produce a counter example it's an explicit<00:17:30.760> you<00:17:31.090> know<00:17:31.210> value<00:17:31.660> of<00:17:31.840> a<00:17:32.320> given<00:17:32.530> type 00:17:32.730 --> 00:17:32.740 align:start position:0% explicit you know value of a given type 00:17:32.740 --> 00:17:35.010 align:start position:0% explicit you know value of a given type that<00:17:33.130> you<00:17:33.160> can<00:17:33.370> run<00:17:33.550> your<00:17:33.760> system<00:17:34.120> on<00:17:34.270> so<00:17:34.870> in 00:17:35.010 --> 00:17:35.020 align:start position:0% that you can run your system on so in 00:17:35.020 --> 00:17:36.860 align:start position:0% that you can run your system on so in either<00:17:35.110> case<00:17:35.350> you<00:17:35.530> don't<00:17:35.680> have<00:17:35.740> to<00:17:35.950> trust<00:17:36.160> us 00:17:36.860 --> 00:17:36.870 align:start position:0% either case you don't have to trust us 00:17:36.870 --> 00:17:39.330 align:start position:0% either case you don't have to trust us but<00:17:37.870> we<00:17:37.960> have<00:17:38.050> a<00:17:38.080> lot<00:17:38.260> of<00:17:38.290> ideas<00:17:38.500> where<00:17:39.040> you 00:17:39.330 --> 00:17:39.340 align:start position:0% but we have a lot of ideas where you 00:17:39.340 --> 00:17:40.980 align:start position:0% but we have a lot of ideas where you know<00:17:39.430> we<00:17:39.550> would<00:17:39.670> love<00:17:39.820> to<00:17:39.970> talk<00:17:40.120> to<00:17:40.300> members<00:17:40.870> of 00:17:40.980 --> 00:17:40.990 align:start position:0% know we would love to talk to members of 00:17:40.990 --> 00:17:42.720 align:start position:0% know we would love to talk to members of the<00:17:41.140> community<00:17:41.500> who<00:17:41.620> are<00:17:41.710> interested<00:17:42.160> a<00:17:42.340> lot 00:17:42.720 --> 00:17:42.730 align:start position:0% the community who are interested a lot 00:17:42.730 --> 00:17:46.170 align:start position:0% the community who are interested a lot of<00:17:42.850> ideas<00:17:42.970> of<00:17:43.620> effectively<00:17:45.030> attaching<00:17:46.030> this 00:17:46.170 --> 00:17:46.180 align:start position:0% of ideas of effectively attaching this 00:17:46.180 --> 00:17:48.360 align:start position:0% of ideas of effectively attaching this type<00:17:46.420> of<00:17:46.450> evidence<00:17:46.720> directly<00:17:47.650> to<00:17:48.040> smart 00:17:48.360 --> 00:17:48.370 align:start position:0% type of evidence directly to smart 00:17:48.370 --> 00:17:50.880 align:start position:0% type of evidence directly to smart contracts<00:17:48.820> different<00:17:49.630> ways<00:17:49.810> that<00:17:49.840> we<00:17:50.380> can<00:17:50.590> you 00:17:50.880 --> 00:17:50.890 align:start position:0% contracts different ways that we can you 00:17:50.890 --> 00:17:52.470 align:start position:0% contracts different ways that we can you know<00:17:50.980> actually<00:17:51.160> have<00:17:51.430> an<00:17:51.520> API<00:17:51.850> where<00:17:52.210> you<00:17:52.330> can 00:17:52.470 --> 00:17:52.480 align:start position:0% know actually have an API where you can 00:17:52.480 --> 00:17:54.390 align:start position:0% know actually have an API where you can easily<00:17:52.630> query<00:17:53.110> what<00:17:53.650> is<00:17:53.740> known<00:17:53.980> about<00:17:54.160> this 00:17:54.390 --> 00:17:54.400 align:start position:0% easily query what is known about this 00:17:54.400 --> 00:17:55.950 align:start position:0% easily query what is known about this contract<00:17:54.880> what's<00:17:55.120> been<00:17:55.270> proved<00:17:55.540> about<00:17:55.780> it 00:17:55.950 --> 00:17:55.960 align:start position:0% contract what's been proved about it 00:17:55.960 --> 00:17:58.800 align:start position:0% contract what's been proved about it what's<00:17:56.380> been<00:17:56.560> disproved<00:17:57.450> also<00:17:58.450> you<00:17:58.720> know 00:17:58.800 --> 00:17:58.810 align:start position:0% what's been disproved also you know 00:17:58.810 --> 00:18:00.510 align:start position:0% what's been disproved also you know there<00:17:59.290> are<00:17:59.380> times<00:17:59.560> you<00:17:59.650> need<00:17:59.800> to<00:17:59.950> prove<00:18:00.160> limos 00:18:00.510 --> 00:18:00.520 align:start position:0% there are times you need to prove limos 00:18:00.520 --> 00:18:02.670 align:start position:0% there are times you need to prove limos before<00:18:01.360> a<00:18:01.630> mantra<00:18:01.990> will<00:18:02.170> you<00:18:02.440> know<00:18:02.530> actually 00:18:02.670 --> 00:18:02.680 align:start position:0% before a mantra will you know actually 00:18:02.680 --> 00:18:04.460 align:start position:0% before a mantra will you know actually prove<00:18:03.070> your<00:18:03.220> main<00:18:03.370> theorem 00:18:04.460 --> 00:18:04.470 align:start position:0% prove your main theorem 00:18:04.470 --> 00:18:06.649 align:start position:0% prove your main theorem you<00:18:05.130> know<00:18:05.190> happens<00:18:05.520> all<00:18:05.640> the<00:18:05.669> time<00:18:05.850> for<00:18:06.270> let's 00:18:06.649 --> 00:18:06.659 align:start position:0% you know happens all the time for let's 00:18:06.659 --> 00:18:08.360 align:start position:0% you know happens all the time for let's say<00:18:06.690> you<00:18:07.110> know<00:18:07.230> very<00:18:07.350> deep<00:18:07.650> properties<00:18:08.159> and 00:18:08.360 --> 00:18:08.370 align:start position:0% say you know very deep properties and 00:18:08.370 --> 00:18:10.039 align:start position:0% say you know very deep properties and there<00:18:08.850> we<00:18:09.000> imagined<00:18:09.390> you<00:18:09.510> could<00:18:09.659> have<00:18:09.840> you 00:18:10.039 --> 00:18:10.049 align:start position:0% there we imagined you could have you 00:18:10.049 --> 00:18:11.779 align:start position:0% there we imagined you could have you know<00:18:10.140> sort<00:18:10.350> of<00:18:10.409> bounties<00:18:10.860> where<00:18:11.370> you<00:18:11.549> want<00:18:11.700> to 00:18:11.779 --> 00:18:11.789 align:start position:0% know sort of bounties where you want to 00:18:11.789 --> 00:18:14.690 align:start position:0% know sort of bounties where you want to give<00:18:11.940> someone<00:18:12.500> you<00:18:13.500> know<00:18:13.620> some<00:18:14.100> some<00:18:14.429> number 00:18:14.690 --> 00:18:14.700 align:start position:0% give someone you know some some number 00:18:14.700 --> 00:18:16.580 align:start position:0% give someone you know some some number of<00:18:14.789> credits<00:18:15.150> if<00:18:15.360> they<00:18:15.630> prove<00:18:15.960> this<00:18:16.110> limo<00:18:16.380> for 00:18:16.580 --> 00:18:16.590 align:start position:0% of credits if they prove this limo for 00:18:16.590 --> 00:18:18.649 align:start position:0% of credits if they prove this limo for you<00:18:16.710> that<00:18:16.919> you<00:18:17.010> relied<00:18:17.280> upon<00:18:17.400> so<00:18:18.210> there's<00:18:18.570> lots 00:18:18.649 --> 00:18:18.659 align:start position:0% you that you relied upon so there's lots 00:18:18.659 --> 00:18:19.940 align:start position:0% you that you relied upon so there's lots of<00:18:18.840> cool<00:18:18.990> things<00:18:19.049> I<00:18:19.409> think<00:18:19.590> we<00:18:19.679> can<00:18:19.799> do 00:18:19.940 --> 00:18:19.950 align:start position:0% of cool things I think we can do 00:18:19.950 --> 00:18:30.590 align:start position:0% of cool things I think we can do community<00:18:20.520> wise<00:18:29.000> flash<00:18:30.000> crashes<00:18:30.240> are<00:18:30.510> either 00:18:30.590 --> 00:18:30.600 align:start position:0% community wise flash crashes are either 00:18:30.600 --> 00:18:32.450 align:start position:0% community wise flash crashes are either generated<00:18:31.200> by<00:18:31.320> fat<00:18:31.620> fingers<00:18:32.010> or<00:18:32.220> like 00:18:32.450 --> 00:18:32.460 align:start position:0% generated by fat fingers or like 00:18:32.460 --> 00:18:34.880 align:start position:0% generated by fat fingers or like downward<00:18:32.970> spirals<00:18:33.480> we're<00:18:33.750> algorithms<00:18:34.620> are 00:18:34.880 --> 00:18:34.890 align:start position:0% downward spirals we're algorithms are 00:18:34.890 --> 00:18:37.159 align:start position:0% downward spirals we're algorithms are forced<00:18:35.280> to<00:18:35.340> sell<00:18:35.700> because<00:18:36.150> other<00:18:36.510> algorithms 00:18:37.159 --> 00:18:37.169 align:start position:0% forced to sell because other algorithms 00:18:37.169 --> 00:18:39.169 align:start position:0% forced to sell because other algorithms are<00:18:37.350> selling<00:18:37.740> and<00:18:37.980> so<00:18:38.549> you<00:18:38.610> just<00:18:38.880> get<00:18:39.030> this 00:18:39.169 --> 00:18:39.179 align:start position:0% are selling and so you just get this 00:18:39.179 --> 00:18:41.600 align:start position:0% are selling and so you just get this very<00:18:39.570> very<00:18:39.870> quick<00:18:40.260> negative<00:18:40.890> spiral<00:18:41.159> down 00:18:41.600 --> 00:18:41.610 align:start position:0% very very quick negative spiral down 00:18:41.610 --> 00:18:43.850 align:start position:0% very very quick negative spiral down like<00:18:42.330> how<00:18:42.539> Adam<00:18:42.840> Andhra<00:18:43.140> help<00:18:43.350> in<00:18:43.559> either<00:18:43.679> of 00:18:43.850 --> 00:18:43.860 align:start position:0% like how Adam Andhra help in either of 00:18:43.860 --> 00:18:46.190 align:start position:0% like how Adam Andhra help in either of those<00:18:44.039> two<00:18:44.250> cases<00:18:44.429> oh<00:18:44.820> great<00:18:45.480> question<00:18:45.840> I<00:18:45.990> mean 00:18:46.190 --> 00:18:46.200 align:start position:0% those two cases oh great question I mean 00:18:46.200 --> 00:18:49.220 align:start position:0% those two cases oh great question I mean fundamentally<00:18:47.960> there's<00:18:48.960> a<00:18:49.020> number<00:18:49.140> of 00:18:49.220 --> 00:18:49.230 align:start position:0% fundamentally there's a number of 00:18:49.230 --> 00:18:51.649 align:start position:0% fundamentally there's a number of answers<00:18:49.470> so<00:18:49.919> if<00:18:50.820> you<00:18:51.000> look<00:18:51.210> at<00:18:51.360> what<00:18:51.539> has 00:18:51.649 --> 00:18:51.659 align:start position:0% answers so if you look at what has 00:18:51.659 --> 00:18:52.940 align:start position:0% answers so if you look at what has happened<00:18:51.690> so<00:18:52.140> first<00:18:52.350> of<00:18:52.409> all<00:18:52.440> flash<00:18:52.679> crashes 00:18:52.940 --> 00:18:52.950 align:start position:0% happened so first of all flash crashes 00:18:52.950 --> 00:18:55.039 align:start position:0% happened so first of all flash crashes happen<00:18:53.370> a<00:18:53.429> lot<00:18:53.549> more<00:18:53.700> often<00:18:53.970> than<00:18:54.150> you<00:18:54.659> know<00:18:54.809> we 00:18:55.039 --> 00:18:55.049 align:start position:0% happen a lot more often than you know we 00:18:55.049 --> 00:18:56.390 align:start position:0% happen a lot more often than you know we hear<00:18:55.200> about<00:18:55.409> in<00:18:55.500> the<00:18:55.590> press<00:18:55.799> right<00:18:56.220> these 00:18:56.390 --> 00:18:56.400 align:start position:0% hear about in the press right these 00:18:56.400 --> 00:18:58.130 align:start position:0% hear about in the press right these happened<00:18:56.700> at<00:18:56.789> a<00:18:56.820> micro<00:18:57.150> level<00:18:57.179> happened<00:18:58.020> at<00:18:58.080> a 00:18:58.130 --> 00:18:58.140 align:start position:0% happened at a micro level happened at a 00:18:58.140 --> 00:19:02.690 align:start position:0% happened at a micro level happened at a micro<00:18:58.409> level<00:18:59.059> it<00:19:00.059> is<00:19:00.210> not<00:19:00.360> uncommon<00:19:00.690> and<00:19:00.990> a<00:19:01.890> lot 00:19:02.690 --> 00:19:02.700 align:start position:0% micro level it is not uncommon and a lot 00:19:02.700 --> 00:19:04.490 align:start position:0% micro level it is not uncommon and a lot of<00:19:02.820> work<00:19:02.940> has<00:19:03.120> been<00:19:03.179> done<00:19:03.390> effectively<00:19:04.020> having 00:19:04.490 --> 00:19:04.500 align:start position:0% of work has been done effectively having 00:19:04.500 --> 00:19:07.120 align:start position:0% of work has been done effectively having things<00:19:04.710> like<00:19:05.010> risk<00:19:05.250> specialized<00:19:05.940> risk<00:19:06.179> gates 00:19:07.120 --> 00:19:07.130 align:start position:0% things like risk specialized risk gates 00:19:07.130 --> 00:19:09.710 align:start position:0% things like risk specialized risk gates specialized<00:19:08.130> circuit<00:19:08.429> breakers<00:19:08.760> that<00:19:09.000> are 00:19:09.710 --> 00:19:09.720 align:start position:0% specialized circuit breakers that are 00:19:09.720 --> 00:19:11.779 align:start position:0% specialized circuit breakers that are effectively<00:19:10.590> you<00:19:10.770> know<00:19:10.890> trying<00:19:11.190> to<00:19:11.250> act<00:19:11.490> as<00:19:11.669> an 00:19:11.779 --> 00:19:11.789 align:start position:0% effectively you know trying to act as an 00:19:11.789 --> 00:19:13.220 align:start position:0% effectively you know trying to act as an arbiter<00:19:12.120> to<00:19:12.480> make<00:19:12.630> sure<00:19:12.750> that<00:19:12.900> things<00:19:13.080> don't 00:19:13.220 --> 00:19:13.230 align:start position:0% arbiter to make sure that things don't 00:19:13.230 --> 00:19:15.799 align:start position:0% arbiter to make sure that things don't get<00:19:13.380> out<00:19:13.470> of<00:19:13.530> control<00:19:13.710> so<00:19:14.700> first<00:19:15.419> in<00:19:15.539> some<00:19:15.720> of 00:19:15.799 --> 00:19:15.809 align:start position:0% get out of control so first in some of 00:19:15.809 --> 00:19:17.390 align:start position:0% get out of control so first in some of our<00:19:15.900> clients<00:19:16.320> now<00:19:16.500> the<00:19:16.559> first<00:19:16.950> thing<00:19:17.100> they 00:19:17.390 --> 00:19:17.400 align:start position:0% our clients now the first thing they 00:19:17.400 --> 00:19:19.340 align:start position:0% our clients now the first thing they actually<00:19:17.820> do<00:19:17.970> is<00:19:18.179> they<00:19:18.510> use<00:19:18.690> a<00:19:18.720> mantra<00:19:19.169> to 00:19:19.340 --> 00:19:19.350 align:start position:0% actually do is they use a mantra to 00:19:19.350 --> 00:19:20.990 align:start position:0% actually do is they use a mantra to reason<00:19:19.710> about<00:19:19.799> their<00:19:20.100> risk<00:19:20.309> a<00:19:20.460> component 00:19:20.990 --> 00:19:21.000 align:start position:0% reason about their risk a component 00:19:21.000 --> 00:19:22.970 align:start position:0% reason about their risk a component before<00:19:21.750> they<00:19:21.870> go<00:19:22.020> in<00:19:22.169> reason<00:19:22.530> let's<00:19:22.770> say<00:19:22.860> they 00:19:22.970 --> 00:19:22.980 align:start position:0% before they go in reason let's say they 00:19:22.980 --> 00:19:24.919 align:start position:0% before they go in reason let's say they have<00:19:23.100> an<00:19:23.220> order<00:19:23.549> router<00:19:23.760> before<00:19:24.510> they<00:19:24.630> start 00:19:24.919 --> 00:19:24.929 align:start position:0% have an order router before they start 00:19:24.929 --> 00:19:26.720 align:start position:0% have an order router before they start to<00:19:25.049> reason<00:19:25.350> about<00:19:25.440> best<00:19:25.799> execution<00:19:26.309> of<00:19:26.580> their 00:19:26.720 --> 00:19:26.730 align:start position:0% to reason about best execution of their 00:19:26.730 --> 00:19:29.000 align:start position:0% to reason about best execution of their routing<00:19:27.000> they<00:19:27.690> may<00:19:27.840> use<00:19:28.020> a<00:19:28.049> mantra<00:19:28.500> first<00:19:28.799> to 00:19:29.000 --> 00:19:29.010 align:start position:0% routing they may use a mantra first to 00:19:29.010 --> 00:19:30.830 align:start position:0% routing they may use a mantra first to prove<00:19:29.309> that<00:19:29.610> their<00:19:29.880> risk<00:19:30.090> a<00:19:30.240> component<00:19:30.750> which 00:19:30.830 --> 00:19:30.840 align:start position:0% prove that their risk a component which 00:19:30.840 --> 00:19:34.490 align:start position:0% prove that their risk a component which is<00:19:30.870> just<00:19:31.230> this<00:19:31.530> last<00:19:31.799> piece<00:19:32.960> that<00:19:33.960> that<00:19:34.350> it 00:19:34.490 --> 00:19:34.500 align:start position:0% is just this last piece that that it 00:19:34.500 --> 00:19:36.049 align:start position:0% is just this last piece that that it effectively<00:19:34.919> won't<00:19:35.250> let<00:19:35.429> something<00:19:35.789> crazy 00:19:36.049 --> 00:19:36.059 align:start position:0% effectively won't let something crazy 00:19:36.059 --> 00:19:39.220 align:start position:0% effectively won't let something crazy out<00:19:36.330> the<00:19:36.450> door<00:19:36.770> so<00:19:37.770> you<00:19:37.830> can<00:19:37.950> effectively 00:19:39.220 --> 00:19:39.230 align:start position:0% out the door so you can effectively 00:19:39.230 --> 00:19:42.020 align:start position:0% out the door so you can effectively incrementally<00:19:40.230> verify<00:19:40.860> the<00:19:41.490> circuit 00:19:42.020 --> 00:19:42.030 align:start position:0% incrementally verify the circuit 00:19:42.030 --> 00:19:43.880 align:start position:0% incrementally verify the circuit breakers<00:19:42.390> these<00:19:42.690> risks<00:19:42.990> gates<00:19:43.169> get<00:19:43.679> those 00:19:43.880 --> 00:19:43.890 align:start position:0% breakers these risks gates get those 00:19:43.890 --> 00:19:46.640 align:start position:0% breakers these risks gates get those safe<00:19:44.130> first<00:19:44.490> and<00:19:44.880> then<00:19:45.510> start<00:19:45.900> to<00:19:45.990> verify<00:19:46.350> more 00:19:46.640 --> 00:19:46.650 align:start position:0% safe first and then start to verify more 00:19:46.650 --> 00:19:48.020 align:start position:0% safe first and then start to verify more pieces<00:19:46.980> that<00:19:47.220> are<00:19:47.370> you<00:19:47.820> know<00:19:47.909> more 00:19:48.020 --> 00:19:48.030 align:start position:0% pieces that are you know more 00:19:48.030 --> 00:19:50.750 align:start position:0% pieces that are you know more algorithmically<00:19:48.600> interesting<00:19:49.140> so<00:19:50.130> did<00:19:50.730> that 00:19:50.750 --> 00:19:50.760 align:start position:0% algorithmically interesting so did that 00:19:50.760 --> 00:19:55.039 align:start position:0% algorithmically interesting so did that answer<00:19:50.970> your<00:19:51.059> question<00:19:53.210> okay<00:19:54.210> thank<00:19:54.929> you<00:19:54.960> very 00:19:55.039 --> 00:19:55.049 align:start position:0% answer your question okay thank you very 00:19:55.049 --> 00:19:56.090 align:start position:0% answer your question okay thank you very much 00:19:56.090 --> 00:19:56.100 align:start position:0% much 00:19:56.100 --> 00:19:58.370 align:start position:0% much thank<00:19:56.250> you