WEBVTT Kind: captions Language: en 00:00:17.359 --> 00:00:20.689 align:start position:0% Virgil<00:00:18.359> dr.<00:00:18.840> Virgil<00:00:19.170> Griffith<00:00:19.770> and<00:00:20.039> Vikram 00:00:20.689 --> 00:00:20.699 align:start position:0% Virgil dr. Virgil Griffith and Vikram 00:00:20.699 --> 00:00:23.450 align:start position:0% Virgil dr. Virgil Griffith and Vikram Verma<00:00:20.970> will<00:00:21.509> present<00:00:21.990> designs<00:00:22.529> for<00:00:22.829> the<00:00:22.950> L<00:00:23.130> for 00:00:23.450 --> 00:00:23.460 align:start position:0% Verma will present designs for the L for 00:00:23.460 --> 00:00:25.519 align:start position:0% Verma will present designs for the L for contract<00:00:24.060> Pro<00:00:24.300> make<00:00:24.509> programming<00:00:25.020> language 00:00:25.519 --> 00:00:25.529 align:start position:0% contract Pro make programming language 00:00:25.529 --> 00:00:32.179 align:start position:0% contract Pro make programming language based<00:00:26.310> on<00:00:26.550> deontic<00:00:27.060> modal<00:00:27.480> logic<00:00:31.189> hello 00:00:32.179 --> 00:00:32.189 align:start position:0% based on deontic modal logic hello 00:00:32.189 --> 00:00:36.619 align:start position:0% based on deontic modal logic hello everyone<00:00:34.519> so<00:00:35.519> we're<00:00:35.640> working<00:00:35.760> are<00:00:36.300> we<00:00:36.449> sitting 00:00:36.619 --> 00:00:36.629 align:start position:0% everyone so we're working are we sitting 00:00:36.629 --> 00:00:39.590 align:start position:0% everyone so we're working are we sitting down<00:00:37.550> you're<00:00:38.550> going<00:00:38.640> to<00:00:38.699> sit<00:00:38.820> down<00:00:38.850> okay<00:00:39.239> Suzy 00:00:39.590 --> 00:00:39.600 align:start position:0% down you're going to sit down okay Suzy 00:00:39.600 --> 00:00:41.900 align:start position:0% down you're going to sit down okay Suzy doesn't<00:00:39.839> sit<00:00:39.960> down<00:00:40.170> so<00:00:40.559> we're<00:00:41.339> gonna<00:00:41.460> ice<00:00:41.670> can 00:00:41.900 --> 00:00:41.910 align:start position:0% doesn't sit down so we're gonna ice can 00:00:41.910 --> 00:00:43.369 align:start position:0% doesn't sit down so we're gonna ice can go<00:00:42.000> to<00:00:42.059> our<00:00:42.150> first<00:00:42.360> slide<00:00:42.540> I<00:00:42.809> mean<00:00:43.140> this<00:00:43.260> is 00:00:43.369 --> 00:00:43.379 align:start position:0% go to our first slide I mean this is 00:00:43.379 --> 00:00:45.829 align:start position:0% go to our first slide I mean this is actually<00:00:43.470> so<00:00:44.280> there's<00:00:45.180> me<00:00:45.300> a<00:00:45.329> lot<00:00:45.420> of<00:00:45.540> math<00:00:45.659> in 00:00:45.829 --> 00:00:45.839 align:start position:0% actually so there's me a lot of math in 00:00:45.839 --> 00:00:48.529 align:start position:0% actually so there's me a lot of math in this<00:00:45.930> talk<00:00:46.170> just<00:00:46.470> like<00:00:46.680> accept<00:00:47.430> it 00:00:48.529 --> 00:00:48.539 align:start position:0% this talk just like accept it 00:00:48.539 --> 00:00:52.430 align:start position:0% this talk just like accept it where's<00:00:49.410> our<00:00:49.590> slide<00:00:50.780> well<00:00:51.780> okay<00:00:52.050> well<00:00:52.289> tell 00:00:52.430 --> 00:00:52.440 align:start position:0% where's our slide well okay well tell 00:00:52.440 --> 00:00:54.680 align:start position:0% where's our slide well okay well tell what<00:00:52.559> the<00:00:52.620> meantime<00:00:52.739> so<00:00:53.460> we're<00:00:54.090> here<00:00:54.270> to<00:00:54.420> tell 00:00:54.680 --> 00:00:54.690 align:start position:0% what the meantime so we're here to tell 00:00:54.690 --> 00:00:56.360 align:start position:0% what the meantime so we're here to tell you<00:00:54.719> about<00:00:54.899> we're<00:00:55.530> developing<00:00:55.770> a<00:00:55.890> brand<00:00:56.129> new 00:00:56.360 --> 00:00:56.370 align:start position:0% you about we're developing a brand new 00:00:56.370 --> 00:00:59.389 align:start position:0% you about we're developing a brand new language<00:00:56.579> for<00:00:57.239> contracts<00:00:57.750> and<00:00:58.079> so<00:00:58.710> so<00:00:59.129> from<00:00:59.309> a 00:00:59.389 --> 00:00:59.399 align:start position:0% language for contracts and so so from a 00:00:59.399 --> 00:01:02.060 align:start position:0% language for contracts and so so from a company<00:00:59.730> called<00:00:59.910> legalese<00:01:00.870> legalese<00:01:01.620> calm 00:01:02.060 --> 00:01:02.070 align:start position:0% company called legalese legalese calm 00:01:02.070 --> 00:01:04.609 align:start position:0% company called legalese legalese calm legalese<00:01:02.789> is<00:01:02.820> an<00:01:03.059> open<00:01:03.359> source<00:01:03.570> project<00:01:03.840> with 00:01:04.609 --> 00:01:04.619 align:start position:0% legalese is an open source project with 00:01:04.619 --> 00:01:07.490 align:start position:0% legalese is an open source project with with<00:01:05.220> delusions<00:01:05.910> of<00:01:06.030> one<00:01:06.330> day<00:01:06.539> being<00:01:07.410> a 00:01:07.490 --> 00:01:07.500 align:start position:0% with delusions of one day being a 00:01:07.500 --> 00:01:12.169 align:start position:0% with delusions of one day being a start-up<00:01:07.830> and<00:01:08.070> so<00:01:09.030> and<00:01:09.929> so<00:01:10.920> originally<00:01:11.399> so<00:01:12.090> you 00:01:12.169 --> 00:01:12.179 align:start position:0% start-up and so and so originally so you 00:01:12.179 --> 00:01:15.770 align:start position:0% start-up and so and so originally so you talk<00:01:12.810> to<00:01:12.929> us<00:01:13.050> all<00:01:13.170> there<00:01:13.580> so<00:01:14.580> I'm<00:01:15.240> kind<00:01:15.539> of<00:01:15.600> the 00:01:15.770 --> 00:01:15.780 align:start position:0% talk to us all there so I'm kind of the 00:01:15.780 --> 00:01:18.550 align:start position:0% talk to us all there so I'm kind of the face<00:01:15.960> and<00:01:16.259> the<00:01:16.830> Crim<00:01:17.070> here<00:01:17.250> is<00:01:17.490> is<00:01:17.850> the<00:01:18.149> brains 00:01:18.550 --> 00:01:18.560 align:start position:0% face and the Crim here is is the brains 00:01:18.560 --> 00:01:21.139 align:start position:0% face and the Crim here is is the brains so<00:01:19.560> we<00:01:19.830> can<00:01:20.039> we<00:01:20.190> can<00:01:20.340> just<00:01:20.369> go<00:01:20.550> ahead<00:01:20.610> and<00:01:20.910> going 00:01:21.139 --> 00:01:21.149 align:start position:0% so we can we can just go ahead and going 00:01:21.149 --> 00:01:22.880 align:start position:0% so we can we can just go ahead and going straight<00:01:21.420> and<00:01:21.690> we<00:01:21.780> can<00:01:21.899> go<00:01:22.289> to<00:01:22.349> the<00:01:22.440> next<00:01:22.590> slide 00:01:22.880 --> 00:01:22.890 align:start position:0% straight and we can go to the next slide 00:01:22.890 --> 00:01:28.180 align:start position:0% straight and we can go to the next slide and<00:01:23.190> we'll<00:01:24.000> tell<00:01:24.179> you<00:01:24.209> about<00:01:24.330> the<00:01:24.690> gist<00:01:24.929> is 00:01:28.180 --> 00:01:28.190 align:start position:0% 00:01:28.190 --> 00:01:35.109 align:start position:0% there<00:01:29.190> a<00:01:29.220> clicker<00:01:29.459> oh<00:01:32.660> okay<00:01:33.660> wait<00:01:34.229> buttons 00:01:35.109 --> 00:01:35.119 align:start position:0% there a clicker oh okay wait buttons 00:01:35.119 --> 00:01:38.749 align:start position:0% there a clicker oh okay wait buttons okay<00:01:36.119> great<00:01:36.330> all<00:01:36.899> right<00:01:37.050> so<00:01:37.380> yeah<00:01:37.619> so<00:01:37.920> so<00:01:38.489> we 00:01:38.749 --> 00:01:38.759 align:start position:0% okay great all right so yeah so so we 00:01:38.759 --> 00:01:41.389 align:start position:0% okay great all right so yeah so so we are<00:01:38.910> giving<00:01:39.270> you<00:01:39.300> a<00:01:39.440> lovely<00:01:40.440> start<00:01:40.770> up<00:01:40.860> here<00:01:40.979> um 00:01:41.389 --> 00:01:41.399 align:start position:0% are giving you a lovely start up here um 00:01:41.399 --> 00:01:44.839 align:start position:0% are giving you a lovely start up here um so<00:01:42.060> so<00:01:42.869> originally<00:01:43.590> our<00:01:43.800> goal<00:01:44.130> was<00:01:44.429> to<00:01:44.489> make<00:01:44.789> a 00:01:44.839 --> 00:01:44.849 align:start position:0% so so originally our goal was to make a 00:01:44.849 --> 00:01:47.389 align:start position:0% so so originally our goal was to make a little<00:01:45.149> programming<00:01:45.569> language<00:01:46.039> for<00:01:47.039> for 00:01:47.389 --> 00:01:47.399 align:start position:0% little programming language for for 00:01:47.399 --> 00:01:49.639 align:start position:0% little programming language for for lawyers<00:01:47.789> to<00:01:47.819> use<00:01:48.149> so<00:01:48.509> so<00:01:49.200> the<00:01:49.289> idea<00:01:49.349> is<00:01:49.619> that 00:01:49.639 --> 00:01:49.649 align:start position:0% lawyers to use so so the idea is that 00:01:49.649 --> 00:01:50.990 align:start position:0% lawyers to use so so the idea is that you<00:01:49.830> would<00:01:49.950> write<00:01:50.099> your<00:01:50.280> little<00:01:50.459> contract<00:01:50.849> in 00:01:50.990 --> 00:01:51.000 align:start position:0% you would write your little contract in 00:01:51.000 --> 00:01:52.490 align:start position:0% you would write your little contract in a<00:01:51.060> high-level<00:01:51.300> language<00:01:51.869> you'd<00:01:52.259> hit<00:01:52.380> the 00:01:52.490 --> 00:01:52.500 align:start position:0% a high-level language you'd hit the 00:01:52.500 --> 00:01:54.889 align:start position:0% a high-level language you'd hit the compile<00:01:53.009> button<00:01:53.130> and<00:01:53.550> you<00:01:53.970> would<00:01:54.060> get<00:01:54.239> English 00:01:54.889 --> 00:01:54.899 align:start position:0% compile button and you would get English 00:01:54.899 --> 00:01:56.779 align:start position:0% compile button and you would get English legalese<00:01:55.410> out<00:01:55.679> of<00:01:55.830> it<00:01:55.920> and<00:01:56.099> that<00:01:56.130> was<00:01:56.520> kind<00:01:56.759> of 00:01:56.779 --> 00:01:56.789 align:start position:0% legalese out of it and that was kind of 00:01:56.789 --> 00:01:59.869 align:start position:0% legalese out of it and that was kind of like<00:01:56.910> the<00:01:57.390> big<00:01:57.569> idea<00:01:57.899> and<00:01:58.170> so<00:01:58.979> so<00:01:59.670> I<00:01:59.729> was 00:01:59.869 --> 00:01:59.879 align:start position:0% like the big idea and so so I was 00:01:59.879 --> 00:02:02.029 align:start position:0% like the big idea and so so I was friends<00:02:00.179> with<00:02:00.209> italic<00:02:01.080> over<00:02:01.259> here<00:02:01.470> and<00:02:01.619> they 00:02:02.029 --> 00:02:02.039 align:start position:0% friends with italic over here and they 00:02:02.039 --> 00:02:05.210 align:start position:0% friends with italic over here and they were<00:02:02.099> and<00:02:02.520> and<00:02:03.440> and<00:02:04.440> they<00:02:04.679> were<00:02:04.770> doing<00:02:05.009> even 00:02:05.210 --> 00:02:05.220 align:start position:0% were and and and they were doing even 00:02:05.220 --> 00:02:06.529 align:start position:0% were and and and they were doing even more<00:02:05.369> sophisticated<00:02:05.520> things<00:02:06.090> with<00:02:06.270> formal 00:02:06.529 --> 00:02:06.539 align:start position:0% more sophisticated things with formal 00:02:06.539 --> 00:02:08.540 align:start position:0% more sophisticated things with formal verification<00:02:06.690> so<00:02:07.379> there's<00:02:07.560> a<00:02:07.619> nice<00:02:07.739> joke<00:02:08.009> the 00:02:08.540 --> 00:02:08.550 align:start position:0% verification so there's a nice joke the 00:02:08.550 --> 00:02:11.720 align:start position:0% verification so there's a nice joke the joke<00:02:08.580> is<00:02:09.179> what<00:02:09.899> do<00:02:10.080> you<00:02:10.140> call<00:02:10.730> runtime 00:02:11.720 --> 00:02:11.730 align:start position:0% joke is what do you call runtime 00:02:11.730 --> 00:02:14.630 align:start position:0% joke is what do you call runtime debugging<00:02:12.360> of<00:02:12.480> a<00:02:12.750> smart<00:02:13.020> contract<00:02:13.470> and<00:02:14.310> you 00:02:14.630 --> 00:02:14.640 align:start position:0% debugging of a smart contract and you 00:02:14.640 --> 00:02:16.130 align:start position:0% debugging of a smart contract and you think<00:02:14.849> about<00:02:14.970> it<00:02:15.120> and<00:02:15.390> the<00:02:15.780> answer<00:02:16.020> is 00:02:16.130 --> 00:02:16.140 align:start position:0% think about it and the answer is 00:02:16.140 --> 00:02:18.470 align:start position:0% think about it and the answer is litigation<00:02:16.650> and<00:02:17.430> you<00:02:17.550> know<00:02:17.640> yeah<00:02:18.120> I<00:02:18.150> know<00:02:18.330> I 00:02:18.470 --> 00:02:18.480 align:start position:0% litigation and you know yeah I know I 00:02:18.480 --> 00:02:19.880 align:start position:0% litigation and you know yeah I know I know<00:02:18.660> it's<00:02:18.930> funny<00:02:19.110> but<00:02:19.440> no<00:02:19.560> it's<00:02:19.770> actually 00:02:19.880 --> 00:02:19.890 align:start position:0% know it's funny but no it's actually 00:02:19.890 --> 00:02:23.839 align:start position:0% know it's funny but no it's actually totally<00:02:20.250> true<00:02:20.989> totally<00:02:21.989> true<00:02:22.200> so<00:02:22.760> amazing<00:02:23.760> it 00:02:23.839 --> 00:02:23.849 align:start position:0% totally true totally true so amazing it 00:02:23.849 --> 00:02:25.399 align:start position:0% totally true totally true so amazing it means<00:02:24.060> that<00:02:24.390> if<00:02:24.719> you're<00:02:24.930> have<00:02:25.079> your<00:02:25.200> smart 00:02:25.399 --> 00:02:25.409 align:start position:0% means that if you're have your smart 00:02:25.409 --> 00:02:26.650 align:start position:0% means that if you're have your smart contract 00:02:26.650 --> 00:02:26.660 align:start position:0% contract 00:02:26.660 --> 00:02:28.780 align:start position:0% contract having<00:02:26.870> runtime<00:02:27.350> errors<00:02:27.680> is<00:02:27.860> like<00:02:28.040> crazy 00:02:28.780 --> 00:02:28.790 align:start position:0% having runtime errors is like crazy 00:02:28.790 --> 00:02:29.680 align:start position:0% having runtime errors is like crazy expensive 00:02:29.680 --> 00:02:29.690 align:start position:0% expensive 00:02:29.690 --> 00:02:31.300 align:start position:0% expensive and<00:02:29.840> maybe<00:02:30.170> you<00:02:30.290> just<00:02:30.320> can't<00:02:30.500> have<00:02:30.740> them<00:02:30.890> so 00:02:31.300 --> 00:02:31.310 align:start position:0% and maybe you just can't have them so 00:02:31.310 --> 00:02:33.340 align:start position:0% and maybe you just can't have them so you're<00:02:31.610> like<00:02:31.790> okay<00:02:31.940> well<00:02:32.420> how<00:02:32.780> do<00:02:32.840> we<00:02:33.140> do<00:02:33.230> it<00:02:33.320> in 00:02:33.340 --> 00:02:33.350 align:start position:0% you're like okay well how do we do it in 00:02:33.350 --> 00:02:35.230 align:start position:0% you're like okay well how do we do it in other<00:02:33.470> industries<00:02:33.980> like<00:02:34.220> say<00:02:34.430> a<00:02:34.460> hardware<00:02:35.030> or 00:02:35.230 --> 00:02:35.240 align:start position:0% other industries like say a hardware or 00:02:35.240 --> 00:02:37.630 align:start position:0% other industries like say a hardware or space<00:02:35.600> shuttle's<00:02:35.900> where<00:02:36.770> your<00:02:37.250> runtime 00:02:37.630 --> 00:02:37.640 align:start position:0% space shuttle's where your runtime 00:02:37.640 --> 00:02:39.040 align:start position:0% space shuttle's where your runtime errors<00:02:37.910> are<00:02:38.000> like<00:02:38.120> just<00:02:38.390> not<00:02:38.540> okay<00:02:38.840> because 00:02:39.040 --> 00:02:39.050 align:start position:0% errors are like just not okay because 00:02:39.050 --> 00:02:41.530 align:start position:0% errors are like just not okay because you<00:02:39.260> lose<00:02:39.410> like<00:02:39.560> a<00:02:39.620> billion<00:02:39.980> dollars<00:02:40.300> so<00:02:41.300> yeah 00:02:41.530 --> 00:02:41.540 align:start position:0% you lose like a billion dollars so yeah 00:02:41.540 --> 00:02:43.480 align:start position:0% you lose like a billion dollars so yeah so<00:02:41.780> you<00:02:41.840> left<00:02:42.050> for<00:02:42.560> your<00:02:42.680> vacation<00:02:43.130> and<00:02:43.280> so 00:02:43.480 --> 00:02:43.490 align:start position:0% so you left for your vacation and so 00:02:43.490 --> 00:02:45.310 align:start position:0% so you left for your vacation and so we're<00:02:43.610> like<00:02:43.700> oh<00:02:43.820> well<00:02:44.300> let's<00:02:44.660> go<00:02:44.840> take<00:02:45.080> all<00:02:45.230> of 00:02:45.310 --> 00:02:45.320 align:start position:0% we're like oh well let's go take all of 00:02:45.320 --> 00:02:46.510 align:start position:0% we're like oh well let's go take all of our<00:02:45.380> stuff<00:02:45.560> for<00:02:45.710> lawyers<00:02:46.010> and<00:02:46.040> give<00:02:46.400> it<00:02:46.490> to 00:02:46.510 --> 00:02:46.520 align:start position:0% our stuff for lawyers and give it to 00:02:46.520 --> 00:02:48.070 align:start position:0% our stuff for lawyers and give it to your<00:02:46.850> to<00:02:47.240> give<00:02:47.360> it<00:02:47.450> to<00:02:47.540> you<00:02:47.630> etherion<00:02:48.050> x' 00:02:48.070 --> 00:02:48.080 align:start position:0% your to give it to you etherion x' 00:02:48.080 --> 00:02:49.210 align:start position:0% your to give it to you etherion x' because<00:02:48.410> you're<00:02:48.620> probably<00:02:48.800> gonna<00:02:48.980> be<00:02:49.130> our 00:02:49.210 --> 00:02:49.220 align:start position:0% because you're probably gonna be our 00:02:49.220 --> 00:02:51.310 align:start position:0% because you're probably gonna be our power<00:02:49.400> users<00:02:49.850> and<00:02:50.060> you<00:02:50.360> need<00:02:50.510> it<00:02:50.540> even<00:02:51.020> more 00:02:51.310 --> 00:02:51.320 align:start position:0% power users and you need it even more 00:02:51.320 --> 00:02:54.040 align:start position:0% power users and you need it even more than<00:02:51.500> the<00:02:51.560> lawyers<00:02:51.860> do<00:02:52.070> so<00:02:52.760> yeah<00:02:53.660> so<00:02:53.810> here<00:02:53.990> we 00:02:54.040 --> 00:02:54.050 align:start position:0% than the lawyers do so yeah so here we 00:02:54.050 --> 00:02:57.190 align:start position:0% than the lawyers do so yeah so here we are<00:02:54.280> the<00:02:55.280> so<00:02:55.760> we're<00:02:55.910> making<00:02:56.120> a<00:02:56.330> custom<00:02:56.780> DSL 00:02:57.190 --> 00:02:57.200 align:start position:0% are the so we're making a custom DSL 00:02:57.200 --> 00:02:59.430 align:start position:0% are the so we're making a custom DSL just<00:02:57.650> for<00:02:57.920> you<00:02:58.160> no<00:02:58.280> permissions<00:02:58.790> obligations 00:02:59.430 --> 00:02:59.440 align:start position:0% just for you no permissions obligations 00:02:59.440 --> 00:03:01.930 align:start position:0% just for you no permissions obligations surprisingly<00:03:00.440> enough<00:03:00.710> some<00:03:01.580> of<00:03:01.610> the<00:03:01.700> lawyers 00:03:01.930 --> 00:03:01.940 align:start position:0% surprisingly enough some of the lawyers 00:03:01.940 --> 00:03:03.430 align:start position:0% surprisingly enough some of the lawyers are<00:03:02.270> actually<00:03:02.570> they're<00:03:02.660> already<00:03:02.840> biting<00:03:03.320> into 00:03:03.430 --> 00:03:03.440 align:start position:0% are actually they're already biting into 00:03:03.440 --> 00:03:04.390 align:start position:0% are actually they're already biting into this<00:03:03.710> you<00:03:03.890> know<00:03:03.980> we<00:03:04.070> said<00:03:04.220> it'll<00:03:04.340> be 00:03:04.390 --> 00:03:04.400 align:start position:0% this you know we said it'll be 00:03:04.400 --> 00:03:06.340 align:start position:0% this you know we said it'll be technophobic<00:03:05.060> but<00:03:05.240> hey<00:03:05.390> someone<00:03:05.750> can<00:03:05.900> some<00:03:06.230> of 00:03:06.340 --> 00:03:06.350 align:start position:0% technophobic but hey someone can some of 00:03:06.350 --> 00:03:08.800 align:start position:0% technophobic but hey someone can some of them<00:03:06.440> actually<00:03:06.680> get<00:03:07.250> it<00:03:07.370> and<00:03:07.760> so<00:03:08.450> this<00:03:08.540> is<00:03:08.690> like 00:03:08.800 --> 00:03:08.810 align:start position:0% them actually get it and so this is like 00:03:08.810 --> 00:03:11.560 align:start position:0% them actually get it and so this is like you<00:03:08.930> know<00:03:09.080> a<00:03:09.260> real<00:03:09.680> law<00:03:09.950> firm<00:03:10.190> and<00:03:10.340> they<00:03:11.240> and 00:03:11.560 --> 00:03:11.570 align:start position:0% you know a real law firm and they and 00:03:11.570 --> 00:03:14.410 align:start position:0% you know a real law firm and they and they<00:03:11.780> use<00:03:12.140> some<00:03:12.170> of<00:03:12.410> our<00:03:12.560> code<00:03:12.770> so<00:03:13.670> Oh<00:03:13.940> wrong 00:03:14.410 --> 00:03:14.420 align:start position:0% they use some of our code so Oh wrong 00:03:14.420 --> 00:03:17.560 align:start position:0% they use some of our code so Oh wrong button<00:03:15.070> okay<00:03:16.070> so<00:03:16.490> this<00:03:16.970> is<00:03:17.120> just<00:03:17.210> kind<00:03:17.420> of<00:03:17.450> a 00:03:17.560 --> 00:03:17.570 align:start position:0% button okay so this is just kind of a 00:03:17.570 --> 00:03:18.220 align:start position:0% button okay so this is just kind of a b-t-dub 00:03:18.220 --> 00:03:18.230 align:start position:0% b-t-dub 00:03:18.230 --> 00:03:21.640 align:start position:0% b-t-dub so<00:03:19.130> the<00:03:19.910> red<00:03:20.090> is<00:03:20.330> what<00:03:20.780> we<00:03:20.930> are<00:03:21.020> modeling<00:03:21.380> here 00:03:21.640 --> 00:03:21.650 align:start position:0% so the red is what we are modeling here 00:03:21.650 --> 00:03:24.160 align:start position:0% so the red is what we are modeling here sort<00:03:21.860> of<00:03:21.890> all<00:03:22.100> possible<00:03:22.610> contracts<00:03:23.180> and<00:03:23.420> then 00:03:24.160 --> 00:03:24.170 align:start position:0% sort of all possible contracts and then 00:03:24.170 --> 00:03:25.750 align:start position:0% sort of all possible contracts and then we<00:03:24.260> have<00:03:24.410> the<00:03:24.590> deaths<00:03:24.800> and<00:03:25.160> then<00:03:25.400> we<00:03:25.460> have<00:03:25.610> the 00:03:25.750 --> 00:03:25.760 align:start position:0% we have the deaths and then we have the 00:03:25.760 --> 00:03:28.330 align:start position:0% we have the deaths and then we have the purple<00:03:26.000> is<00:03:26.390> where<00:03:26.660> is<00:03:26.930> where<00:03:27.350> we<00:03:27.470> can<00:03:27.680> help<00:03:28.130> you 00:03:28.330 --> 00:03:28.340 align:start position:0% purple is where is where we can help you 00:03:28.340 --> 00:03:31.540 align:start position:0% purple is where is where we can help you out<00:03:28.370> so<00:03:29.240> so<00:03:29.960> our<00:03:30.260> ideal<00:03:30.770> world<00:03:30.860> is<00:03:31.370> where 00:03:31.540 --> 00:03:31.550 align:start position:0% out so so our ideal world is where 00:03:31.550 --> 00:03:32.710 align:start position:0% out so so our ideal world is where you'll<00:03:31.730> write<00:03:32.000> your<00:03:32.030> write<00:03:32.480> your<00:03:32.600> little 00:03:32.710 --> 00:03:32.720 align:start position:0% you'll write your write your little 00:03:32.720 --> 00:03:33.790 align:start position:0% you'll write your write your little contract<00:03:33.110> you<00:03:33.230> won't<00:03:33.380> even<00:03:33.440> think<00:03:33.560> about 00:03:33.790 --> 00:03:33.800 align:start position:0% contract you won't even think about 00:03:33.800 --> 00:03:35.140 align:start position:0% contract you won't even think about aetherium<00:03:34.250> it'll<00:03:34.550> just<00:03:34.700> be<00:03:34.820> oh<00:03:34.850> they'll<00:03:35.090> be 00:03:35.140 --> 00:03:35.150 align:start position:0% aetherium it'll just be oh they'll be 00:03:35.150 --> 00:03:37.000 align:start position:0% aetherium it'll just be oh they'll be these<00:03:35.360> agents<00:03:35.750> with<00:03:35.870> these<00:03:35.990> obligation<00:03:36.530> blah 00:03:37.000 --> 00:03:37.010 align:start position:0% these agents with these obligation blah 00:03:37.010 --> 00:03:38.830 align:start position:0% these agents with these obligation blah and<00:03:37.220> then<00:03:37.790> and<00:03:38.030> then<00:03:38.120> it<00:03:38.209> will<00:03:38.300> just<00:03:38.420> compile 00:03:38.830 --> 00:03:38.840 align:start position:0% and then and then it will just compile 00:03:38.840 --> 00:03:40.900 align:start position:0% and then and then it will just compile and<00:03:39.140> you<00:03:39.560> can<00:03:39.680> for<00:03:39.830> the<00:03:39.890> most<00:03:40.040> part<00:03:40.340> just<00:03:40.550> not 00:03:40.900 --> 00:03:40.910 align:start position:0% and you can for the most part just not 00:03:40.910 --> 00:03:42.730 align:start position:0% and you can for the most part just not worry<00:03:41.120> about<00:03:41.180> it<00:03:41.360> and<00:03:41.780> in<00:03:42.260> the<00:03:42.350> future<00:03:42.530> you 00:03:42.730 --> 00:03:42.740 align:start position:0% worry about it and in the future you 00:03:42.740 --> 00:03:44.500 align:start position:0% worry about it and in the future you could<00:03:42.830> even<00:03:43.010> get<00:03:43.190> your<00:03:43.370> english<00:03:43.820> contract<00:03:44.330> as 00:03:44.500 --> 00:03:44.510 align:start position:0% could even get your english contract as 00:03:44.510 --> 00:03:48.580 align:start position:0% could even get your english contract as well<00:03:45.250> so<00:03:46.250> okay<00:03:46.610> so<00:03:46.820> let's<00:03:47.180> go<00:03:47.360> listen<00:03:47.900> okay<00:03:48.530> so 00:03:48.580 --> 00:03:48.590 align:start position:0% well so okay so let's go listen okay so 00:03:48.590 --> 00:03:50.470 align:start position:0% well so okay so let's go listen okay so the<00:03:48.709> first<00:03:48.830> thing<00:03:48.980> we'll<00:03:49.070> ask<00:03:49.280> well<00:03:50.180> we<00:03:50.300> love 00:03:50.470 --> 00:03:50.480 align:start position:0% the first thing we'll ask well we love 00:03:50.480 --> 00:03:51.760 align:start position:0% the first thing we'll ask well we love solidity<00:03:50.840> you<00:03:50.990> do<00:03:51.170> we<00:03:51.260> really<00:03:51.440> want<00:03:51.620> another 00:03:51.760 --> 00:03:51.770 align:start position:0% solidity you do we really want another 00:03:51.770 --> 00:03:53.680 align:start position:0% solidity you do we really want another language<00:03:51.980> and<00:03:52.400> the<00:03:53.120> first<00:03:53.330> answer<00:03:53.510> is<00:03:53.540> oh<00:03:53.660> oh 00:03:53.680 --> 00:03:53.690 align:start position:0% language and the first answer is oh oh 00:03:53.690 --> 00:03:55.540 align:start position:0% language and the first answer is oh oh you<00:03:53.959> can<00:03:54.170> still<00:03:54.380> have<00:03:54.560> your<00:03:54.590> solidity<00:03:55.010> and<00:03:55.220> if 00:03:55.540 --> 00:03:55.550 align:start position:0% you can still have your solidity and if 00:03:55.550 --> 00:03:57.100 align:start position:0% you can still have your solidity and if you<00:03:55.640> still<00:03:55.880> want<00:03:55.910> your<00:03:56.270> your<00:03:56.420> low-level<00:03:56.900> stuff 00:03:57.100 --> 00:03:57.110 align:start position:0% you still want your your low-level stuff 00:03:57.110 --> 00:03:58.780 align:start position:0% you still want your your low-level stuff you<00:03:57.709> should<00:03:58.040> you<00:03:58.160> should<00:03:58.190> use<00:03:58.400> just<00:03:58.550> do<00:03:58.640> it<00:03:58.700> you 00:03:58.780 --> 00:03:58.790 align:start position:0% you should you should use just do it you 00:03:58.790 --> 00:04:00.580 align:start position:0% you should you should use just do it you should<00:03:58.910> still<00:03:59.090> use<00:03:59.120> solidity<00:03:59.570> you<00:04:00.290> can<00:04:00.410> kind 00:04:00.580 --> 00:04:00.590 align:start position:0% should still use solidity you can kind 00:04:00.590 --> 00:04:03.310 align:start position:0% should still use solidity you can kind of<00:04:00.620> think<00:04:00.680> of<00:04:00.860> it<00:04:00.950> as<00:04:01.010> say<00:04:01.489> using<00:04:01.910> say<00:04:02.450> c<00:04:02.510> versus 00:04:03.310 --> 00:04:03.320 align:start position:0% of think of it as say using say c versus 00:04:03.320 --> 00:04:05.170 align:start position:0% of think of it as say using say c versus i<00:04:03.590> guess<00:04:04.010> something<00:04:04.220> like<00:04:04.250> python<00:04:04.730> i<00:04:04.760> suppose 00:04:05.170 --> 00:04:05.180 align:start position:0% i guess something like python i suppose 00:04:05.180 --> 00:04:07.750 align:start position:0% i guess something like python i suppose it's<00:04:05.930> not<00:04:06.050> quite<00:04:06.260> exactly<00:04:06.650> right<00:04:06.920> but<00:04:07.400> anyway 00:04:07.750 --> 00:04:07.760 align:start position:0% it's not quite exactly right but anyway 00:04:07.760 --> 00:04:09.760 align:start position:0% it's not quite exactly right but anyway the<00:04:08.000> idea<00:04:08.030> is<00:04:08.360> that<00:04:08.480> you<00:04:08.690> want<00:04:08.900> like<00:04:08.959> a<00:04:09.050> high 00:04:09.760 --> 00:04:09.770 align:start position:0% the idea is that you want like a high 00:04:09.770 --> 00:04:12.370 align:start position:0% the idea is that you want like a high level<00:04:09.980> language<00:04:10.420> for<00:04:11.420> for<00:04:11.660> doing<00:04:11.840> high<00:04:12.140> level 00:04:12.370 --> 00:04:12.380 align:start position:0% level language for for doing high level 00:04:12.380 --> 00:04:13.510 align:start position:0% level language for for doing high level things<00:04:12.620> you<00:04:12.800> don't<00:04:12.860> want<00:04:13.040> to<00:04:13.070> think<00:04:13.280> about<00:04:13.430> the 00:04:13.510 --> 00:04:13.520 align:start position:0% things you don't want to think about the 00:04:13.520 --> 00:04:14.860 align:start position:0% things you don't want to think about the rest<00:04:13.700> but<00:04:13.940> if<00:04:14.000> you're<00:04:14.090> doing<00:04:14.150> novel<00:04:14.630> things 00:04:14.860 --> 00:04:14.870 align:start position:0% rest but if you're doing novel things 00:04:14.870 --> 00:04:16.360 align:start position:0% rest but if you're doing novel things and<00:04:15.290> you<00:04:15.380> want<00:04:15.440> to<00:04:15.560> be<00:04:15.620> close<00:04:15.860> to<00:04:15.890> the<00:04:16.070> bottom 00:04:16.360 --> 00:04:16.370 align:start position:0% and you want to be close to the bottom 00:04:16.370 --> 00:04:19.060 align:start position:0% and you want to be close to the bottom then<00:04:16.580> you<00:04:16.609> still<00:04:16.880> use<00:04:17.090> your<00:04:17.359> solidity<00:04:17.919> so<00:04:18.919> we 00:04:19.060 --> 00:04:19.070 align:start position:0% then you still use your solidity so we 00:04:19.070 --> 00:04:20.979 align:start position:0% then you still use your solidity so we use<00:04:19.220> SQL<00:04:19.700> sort<00:04:19.970> of<00:04:20.030> an<00:04:20.120> example<00:04:20.209> for<00:04:20.690> why<00:04:20.840> it's 00:04:20.979 --> 00:04:20.989 align:start position:0% use SQL sort of an example for why it's 00:04:20.989 --> 00:04:22.990 align:start position:0% use SQL sort of an example for why it's a<00:04:21.080> good<00:04:21.200> idea<00:04:21.500> so<00:04:22.040> you<00:04:22.070> can<00:04:22.280> imagine<00:04:22.430> query<00:04:22.880> in 00:04:22.990 --> 00:04:23.000 align:start position:0% a good idea so you can imagine query in 00:04:23.000 --> 00:04:25.000 align:start position:0% a good idea so you can imagine query in your<00:04:23.120> database<00:04:23.510> in<00:04:23.750> C<00:04:24.020> or<00:04:24.200> Java<00:04:24.590> Script<00:04:24.680> would 00:04:25.000 --> 00:04:25.010 align:start position:0% your database in C or Java Script would 00:04:25.010 --> 00:04:26.920 align:start position:0% your database in C or Java Script would be<00:04:25.070> very<00:04:25.250> unpleasant<00:04:25.550> but<00:04:26.030> doing<00:04:26.240> it<00:04:26.330> in<00:04:26.390> SQL 00:04:26.920 --> 00:04:26.930 align:start position:0% be very unpleasant but doing it in SQL 00:04:26.930 --> 00:04:29.110 align:start position:0% be very unpleasant but doing it in SQL is<00:04:27.200> lovely<00:04:27.560> so<00:04:27.710> we're<00:04:28.130> gonna<00:04:28.250> give<00:04:28.400> you<00:04:28.430> an<00:04:28.640> SQL 00:04:29.110 --> 00:04:29.120 align:start position:0% is lovely so we're gonna give you an SQL 00:04:29.120 --> 00:04:33.400 align:start position:0% is lovely so we're gonna give you an SQL for<00:04:29.330> contracts<00:04:30.190> okay<00:04:31.660> yeah<00:04:32.660> that's<00:04:33.169> why<00:04:33.320> you 00:04:33.400 --> 00:04:33.410 align:start position:0% for contracts okay yeah that's why you 00:04:33.410 --> 00:04:35.920 align:start position:0% for contracts okay yeah that's why you want<00:04:33.530> to<00:04:33.560> do<00:04:33.650> it<00:04:33.770> yeah<00:04:34.669> and<00:04:34.910> the<00:04:35.510> cool<00:04:35.900> part 00:04:35.920 --> 00:04:35.930 align:start position:0% want to do it yeah and the cool part 00:04:35.930 --> 00:04:38.560 align:start position:0% want to do it yeah and the cool part about<00:04:36.140> this<00:04:36.380> is<00:04:36.440> that<00:04:36.620> that<00:04:37.150> so<00:04:38.150> we<00:04:38.240> can't<00:04:38.450> want 00:04:38.560 --> 00:04:38.570 align:start position:0% about this is that that so we can't want 00:04:38.570 --> 00:04:39.439 align:start position:0% about this is that that so we can't want to<00:04:38.630> do<00:04:38.690> this<00:04:38.780> is 00:04:39.439 --> 00:04:39.449 align:start position:0% to do this is 00:04:39.449 --> 00:04:41.239 align:start position:0% to do this is because<00:04:39.719> so<00:04:40.409> first<00:04:40.559> of<00:04:40.650> all<00:04:40.680> you<00:04:40.889> you<00:04:41.099> could 00:04:41.239 --> 00:04:41.249 align:start position:0% because so first of all you you could 00:04:41.249 --> 00:04:42.709 align:start position:0% because so first of all you you could eventually<00:04:41.460> one<00:04:41.729> day<00:04:41.759> compile<00:04:42.479> your 00:04:42.709 --> 00:04:42.719 align:start position:0% eventually one day compile your 00:04:42.719 --> 00:04:44.059 align:start position:0% eventually one day compile your aetherium<00:04:43.139> contracts<00:04:43.469> to<00:04:43.559> English<00:04:43.860> and 00:04:44.059 --> 00:04:44.069 align:start position:0% aetherium contracts to English and 00:04:44.069 --> 00:04:46.309 align:start position:0% aetherium contracts to English and number<00:04:44.729> two<00:04:44.939> we<00:04:45.360> could<00:04:45.479> eventually<00:04:45.659> start 00:04:46.309 --> 00:04:46.319 align:start position:0% number two we could eventually start 00:04:46.319 --> 00:04:49.189 align:start position:0% number two we could eventually start getting<00:04:46.559> Noir<00:04:47.460> like<00:04:47.639> like<00:04:47.909> normal<00:04:48.599> lawyers 00:04:49.189 --> 00:04:49.199 align:start position:0% getting Noir like like normal lawyers 00:04:49.199 --> 00:04:51.079 align:start position:0% getting Noir like like normal lawyers aren't<00:04:49.439> using<00:04:49.710> aetherium<00:04:50.279> because<00:04:50.849> here's 00:04:51.079 --> 00:04:51.089 align:start position:0% aren't using aetherium because here's 00:04:51.089 --> 00:04:53.089 align:start position:0% aren't using aetherium because here's the<00:04:51.210> cool<00:04:51.360> part<00:04:51.389> because<00:04:52.289> the<00:04:52.499> etherium 00:04:53.089 --> 00:04:53.099 align:start position:0% the cool part because the etherium 00:04:53.099 --> 00:04:55.700 align:start position:0% the cool part because the etherium system<00:04:53.490> is<00:04:53.669> more<00:04:54.330> reliable<00:04:54.659> than<00:04:55.259> than<00:04:55.680> a 00:04:55.700 --> 00:04:55.710 align:start position:0% system is more reliable than than a 00:04:55.710 --> 00:04:58.339 align:start position:0% system is more reliable than than a judge's<00:04:56.460> brain<00:04:56.759> so<00:04:57.330> you're<00:04:57.449> like<00:04:57.599> oh<00:04:57.779> so<00:04:58.199> it's 00:04:58.339 --> 00:04:58.349 align:start position:0% judge's brain so you're like oh so it's 00:04:58.349 --> 00:04:59.360 align:start position:0% judge's brain so you're like oh so it's like<00:04:58.469> so<00:04:58.650> if<00:04:58.710> you<00:04:58.770> say<00:04:58.889> oh<00:04:58.919> you<00:04:59.069> take<00:04:59.339> all 00:04:59.360 --> 00:04:59.370 align:start position:0% like so if you say oh you take all 00:04:59.370 --> 00:05:00.320 align:start position:0% like so if you say oh you take all lawyers<00:04:59.789> you<00:04:59.879> get<00:04:59.999> all<00:05:00.089> your<00:05:00.210> regular 00:05:00.320 --> 00:05:00.330 align:start position:0% lawyers you get all your regular 00:05:00.330 --> 00:05:01.790 align:start position:0% lawyers you get all your regular contractor<00:05:00.990> you<00:05:01.080> see<00:05:01.169> compiling<00:05:01.409> to<00:05:01.499> English 00:05:01.790 --> 00:05:01.800 align:start position:0% contractor you see compiling to English 00:05:01.800 --> 00:05:03.200 align:start position:0% contractor you see compiling to English but<00:05:02.189> now<00:05:02.309> you<00:05:02.370> just<00:05:02.490> run<00:05:02.580> them<00:05:02.729> on<00:05:02.789> aetherium 00:05:03.200 --> 00:05:03.210 align:start position:0% but now you just run them on aetherium 00:05:03.210 --> 00:05:04.909 align:start position:0% but now you just run them on aetherium and<00:05:03.360> they're<00:05:03.629> even<00:05:03.749> more<00:05:03.900> reliable<00:05:04.589> and<00:05:04.710> even 00:05:04.909 --> 00:05:04.919 align:start position:0% and they're even more reliable and even 00:05:04.919 --> 00:05:06.409 align:start position:0% and they're even more reliable and even more<00:05:05.069> predictable<00:05:05.520> and<00:05:05.699> they<00:05:06.120> would<00:05:06.210> be<00:05:06.270> like 00:05:06.409 --> 00:05:06.419 align:start position:0% more predictable and they would be like 00:05:06.419 --> 00:05:09.230 align:start position:0% more predictable and they would be like oh<00:05:06.539> my<00:05:06.689> god<00:05:06.870> yes<00:05:07.199> and<00:05:07.409> therefore<00:05:08.129> we<00:05:08.339> bring<00:05:08.580> you 00:05:09.230 --> 00:05:09.240 align:start position:0% oh my god yes and therefore we bring you 00:05:09.240 --> 00:05:12.730 align:start position:0% oh my god yes and therefore we bring you know<00:05:09.360> like<00:05:09.719> what<00:05:09.990> the<00:05:10.650> 90<00:05:11.580> billion<00:05:12.419> dollar 00:05:12.730 --> 00:05:12.740 align:start position:0% know like what the 90 billion dollar 00:05:12.740 --> 00:05:15.050 align:start position:0% know like what the 90 billion dollar contract<00:05:13.740> rafting<00:05:13.949> industry<00:05:14.310> into<00:05:14.789> aetherium 00:05:15.050 --> 00:05:15.060 align:start position:0% contract rafting industry into aetherium 00:05:15.060 --> 00:05:17.089 align:start position:0% contract rafting industry into aetherium which<00:05:15.419> will<00:05:15.659> make<00:05:15.810> all<00:05:15.990> your<00:05:16.199> ether<00:05:16.469> go<00:05:16.620> up<00:05:16.770> and 00:05:17.089 --> 00:05:17.099 align:start position:0% which will make all your ether go up and 00:05:17.099 --> 00:05:21.079 align:start position:0% which will make all your ether go up and that<00:05:17.249> will<00:05:17.339> make<00:05:17.430> all<00:05:17.610> of<00:05:17.639> you<00:05:17.819> happy<00:05:18.139> so<00:05:20.089> this 00:05:21.079 --> 00:05:21.089 align:start position:0% that will make all of you happy so this 00:05:21.089 --> 00:05:25.760 align:start position:0% that will make all of you happy so this is<00:05:21.270> our<00:05:21.389> start<00:05:21.889> go<00:05:23.300> so<00:05:24.300> we<00:05:24.810> have<00:05:25.080> rough 00:05:25.760 --> 00:05:25.770 align:start position:0% is our start go so we have rough 00:05:25.770 --> 00:05:30.170 align:start position:0% is our start go so we have rough consensus<00:05:26.610> but<00:05:27.089> not<00:05:27.539> running<00:05:28.080> code<00:05:28.349> and<00:05:29.180> the 00:05:30.170 --> 00:05:30.180 align:start position:0% consensus but not running code and the 00:05:30.180 --> 00:05:31.909 align:start position:0% consensus but not running code and the rest<00:05:30.389> of<00:05:30.449> this<00:05:30.569> talk<00:05:30.810> is<00:05:31.050> essentially<00:05:31.560> going 00:05:31.909 --> 00:05:31.919 align:start position:0% rest of this talk is essentially going 00:05:31.919 --> 00:05:38.269 align:start position:0% rest of this talk is essentially going to<00:05:32.069> be<00:05:32.219> a<00:05:36.080> fairly<00:05:37.080> high-level<00:05:37.469> literature 00:05:38.269 --> 00:05:38.279 align:start position:0% to be a fairly high-level literature 00:05:38.279 --> 00:05:42.170 align:start position:0% to be a fairly high-level literature review<00:05:38.699> of<00:05:39.319> ways<00:05:40.319> of<00:05:40.680> expressing<00:05:41.249> agreements 00:05:42.170 --> 00:05:42.180 align:start position:0% review of ways of expressing agreements 00:05:42.180 --> 00:05:44.439 align:start position:0% review of ways of expressing agreements and<00:05:42.449> ways<00:05:42.659> we<00:05:42.870> can<00:05:42.990> reason<00:05:43.289> about<00:05:43.349> them<00:05:43.680> and 00:05:44.439 --> 00:05:44.449 align:start position:0% and ways we can reason about them and 00:05:44.449 --> 00:05:48.980 align:start position:0% and ways we can reason about them and eventually<00:05:45.449> ways<00:05:45.810> in<00:05:46.289> which<00:05:47.120> we<00:05:48.120> can<00:05:48.419> compile 00:05:48.980 --> 00:05:48.990 align:start position:0% eventually ways in which we can compile 00:05:48.990 --> 00:05:52.040 align:start position:0% eventually ways in which we can compile those<00:05:49.259> in<00:05:49.620> to<00:05:50.129> code<00:05:50.370> which<00:05:50.729> is<00:05:50.939> interpreted<00:05:51.899> in 00:05:52.040 --> 00:05:52.050 align:start position:0% those in to code which is interpreted in 00:05:52.050 --> 00:06:01.189 align:start position:0% those in to code which is interpreted in a<00:05:52.139> way<00:05:52.289> that<00:05:52.469> preserves<00:05:52.620> those<00:05:53.129> semantics<00:06:00.199> so 00:06:01.189 --> 00:06:01.199 align:start position:0% a way that preserves those semantics so 00:06:01.199 --> 00:06:05.809 align:start position:0% a way that preserves those semantics so CL<00:06:01.860> is<00:06:02.189> a<00:06:02.669> logic<00:06:03.300> based<00:06:04.789> formalism<00:06:05.789> for 00:06:05.809 --> 00:06:05.819 align:start position:0% CL is a logic based formalism for 00:06:05.819 --> 00:06:09.260 align:start position:0% CL is a logic based formalism for expressing<00:06:06.479> contracts<00:06:06.899> and<00:06:07.669> this<00:06:08.669> is<00:06:08.849> its 00:06:09.260 --> 00:06:09.270 align:start position:0% expressing contracts and this is its 00:06:09.270 --> 00:06:11.809 align:start position:0% expressing contracts and this is its syntax<00:06:09.740> you<00:06:10.740> can<00:06:10.889> read<00:06:11.069> that<00:06:11.219> as<00:06:11.459> saying<00:06:11.490> that 00:06:11.809 --> 00:06:11.819 align:start position:0% syntax you can read that as saying that 00:06:11.819 --> 00:06:13.969 align:start position:0% syntax you can read that as saying that a<00:06:12.029> contract<00:06:12.479> either<00:06:12.810> indicates<00:06:13.649> an 00:06:13.969 --> 00:06:13.979 align:start position:0% a contract either indicates an 00:06:13.979 --> 00:06:16.429 align:start position:0% a contract either indicates an obligation<00:06:14.550> to<00:06:14.629> do<00:06:15.629> something<00:06:15.779> a<00:06:16.080> permission 00:06:16.429 --> 00:06:16.439 align:start position:0% obligation to do something a permission 00:06:16.439 --> 00:06:18.290 align:start position:0% obligation to do something a permission to<00:06:16.560> do<00:06:16.649> something<00:06:16.830> a<00:06:17.159> prohibition<00:06:17.789> from<00:06:17.999> doing 00:06:18.290 --> 00:06:18.300 align:start position:0% to do something a prohibition from doing 00:06:18.300 --> 00:06:21.499 align:start position:0% to do something a prohibition from doing something<00:06:19.129> the<00:06:20.129> conjunction<00:06:20.729> of<00:06:20.879> two<00:06:20.939> other 00:06:21.499 --> 00:06:21.509 align:start position:0% something the conjunction of two other 00:06:21.509 --> 00:06:25.879 align:start position:0% something the conjunction of two other clauses<00:06:21.930> or<00:06:23.240> some<00:06:24.240> contract<00:06:24.749> becomes<00:06:25.050> active 00:06:25.879 --> 00:06:25.889 align:start position:0% clauses or some contract becomes active 00:06:25.889 --> 00:06:29.239 align:start position:0% clauses or some contract becomes active dependent<00:06:26.639> on<00:06:27.259> some<00:06:28.259> other<00:06:28.560> action<00:06:29.039> having 00:06:29.239 --> 00:06:29.249 align:start position:0% dependent on some other action having 00:06:29.249 --> 00:06:30.889 align:start position:0% dependent on some other action having being<00:06:29.520> performed<00:06:29.879> and<00:06:30.330> we<00:06:30.449> can<00:06:30.599> look<00:06:30.719> at<00:06:30.810> the 00:06:30.889 --> 00:06:30.899 align:start position:0% being performed and we can look at the 00:06:30.899 --> 00:06:32.719 align:start position:0% being performed and we can look at the structure<00:06:31.169> of<00:06:31.319> obligations<00:06:32.129> where<00:06:32.459> we<00:06:32.610> have 00:06:32.719 --> 00:06:32.729 align:start position:0% structure of obligations where we have 00:06:32.729 --> 00:06:36.139 align:start position:0% structure of obligations where we have two<00:06:32.909> parameters<00:06:33.389> C<00:06:33.719> and<00:06:33.899> alpha<00:06:34.399> alpha<00:06:35.399> is<00:06:35.849> the 00:06:36.139 --> 00:06:36.149 align:start position:0% two parameters C and alpha alpha is the 00:06:36.149 --> 00:06:37.519 align:start position:0% two parameters C and alpha alpha is the thing<00:06:36.330> you're<00:06:36.479> expected<00:06:36.899> to<00:06:36.930> perform<00:06:37.319> right 00:06:37.519 --> 00:06:37.529 align:start position:0% thing you're expected to perform right 00:06:37.529 --> 00:06:40.459 align:start position:0% thing you're expected to perform right now<00:06:37.770> and<00:06:38.159> if<00:06:38.669> you<00:06:38.789> do<00:06:38.939> not<00:06:39.060> do<00:06:39.449> that<00:06:39.479> then<00:06:40.349> you 00:06:40.459 --> 00:06:40.469 align:start position:0% now and if you do not do that then you 00:06:40.469 --> 00:06:42.050 align:start position:0% now and if you do not do that then you have<00:06:40.529> to<00:06:40.800> fulfill<00:06:41.159> the<00:06:41.339> reclamation<00:06:41.610> clause 00:06:42.050 --> 00:06:42.060 align:start position:0% have to fulfill the reclamation clause 00:06:42.060 --> 00:06:45.019 align:start position:0% have to fulfill the reclamation clause see<00:06:42.419> that<00:06:43.199> Clause<00:06:43.409> C<00:06:43.740> can<00:06:44.099> be<00:06:44.249> the<00:06:44.520> far<00:06:44.759> right 00:06:45.019 --> 00:06:45.029 align:start position:0% see that Clause C can be the far right 00:06:45.029 --> 00:06:47.899 align:start position:0% see that Clause C can be the far right clause<00:06:45.569> which<00:06:45.959> is<00:06:45.990> unfulfilled<00:06:46.469> well<00:06:46.770> and<00:06:46.949> if 00:06:47.899 --> 00:06:47.909 align:start position:0% clause which is unfulfilled well and if 00:06:47.909 --> 00:06:49.429 align:start position:0% clause which is unfulfilled well and if you<00:06:48.000> ever<00:06:48.149> get<00:06:48.329> to<00:06:48.479> that<00:06:48.509> point<00:06:48.629> you're<00:06:49.199> in 00:06:49.429 --> 00:06:49.439 align:start position:0% you ever get to that point you're in 00:06:49.439 --> 00:06:50.960 align:start position:0% you ever get to that point you're in breach<00:06:49.649> of<00:06:49.709> contract 00:06:50.960 --> 00:06:50.970 align:start position:0% breach of contract 00:06:50.970 --> 00:06:53.180 align:start position:0% breach of contract actions<00:06:51.720> are<00:06:51.960> basic<00:06:52.320> propositional 00:06:53.180 --> 00:06:53.190 align:start position:0% actions are basic propositional 00:06:53.190 --> 00:06:57.440 align:start position:0% actions are basic propositional variables<00:06:54.320> which<00:06:55.320> can<00:06:55.590> be<00:06:55.980> either<00:06:56.460> expressed 00:06:57.440 --> 00:06:57.450 align:start position:0% variables which can be either expressed 00:06:57.450 --> 00:06:59.840 align:start position:0% variables which can be either expressed in<00:06:57.780> terms<00:06:58.050> of<00:06:58.260> concurrent<00:06:58.740> actions<00:06:59.070> I<00:06:59.430> do 00:06:59.840 --> 00:06:59.850 align:start position:0% in terms of concurrent actions I do 00:06:59.850 --> 00:07:01.510 align:start position:0% in terms of concurrent actions I do things<00:07:00.060> at<00:07:00.180> the<00:07:00.270> same<00:07:00.390> time<00:07:00.450> or<00:07:01.020> you 00:07:01.510 --> 00:07:01.520 align:start position:0% things at the same time or you 00:07:01.520 --> 00:07:03.380 align:start position:0% things at the same time or you sequencing<00:07:02.520> you<00:07:02.790> do<00:07:02.880> one<00:07:03.030> thing<00:07:03.060> after 00:07:03.380 --> 00:07:03.390 align:start position:0% sequencing you do one thing after 00:07:03.390 --> 00:07:05.540 align:start position:0% sequencing you do one thing after another<00:07:03.420> or<00:07:03.900> you<00:07:03.930> do<00:07:04.410> between<00:07:04.770> one<00:07:05.220> of<00:07:05.340> two 00:07:05.540 --> 00:07:05.550 align:start position:0% another or you do between one of two 00:07:05.550 --> 00:07:10.580 align:start position:0% another or you do between one of two things<00:07:08.570> this<00:07:09.570> is<00:07:09.720> to<00:07:10.050> make<00:07:10.170> that<00:07:10.320> concrete 00:07:10.580 --> 00:07:10.590 align:start position:0% things this is to make that concrete 00:07:10.590 --> 00:07:13.130 align:start position:0% things this is to make that concrete here's<00:07:11.010> an<00:07:11.160> example<00:07:11.430> of<00:07:11.850> a<00:07:12.180> fairly<00:07:12.600> simple 00:07:13.130 --> 00:07:13.140 align:start position:0% here's an example of a fairly simple 00:07:13.140 --> 00:07:16.450 align:start position:0% here's an example of a fairly simple clause<00:07:13.410> this<00:07:13.890> expresses<00:07:14.390> that<00:07:15.390> you<00:07:16.110> should 00:07:16.450 --> 00:07:16.460 align:start position:0% clause this expresses that you should 00:07:16.460 --> 00:07:20.180 align:start position:0% clause this expresses that you should that<00:07:17.460> if<00:07:17.670> you<00:07:17.820> do<00:07:18.000> a<00:07:18.270> you<00:07:18.810> must<00:07:19.020> then<00:07:19.350> perform<00:07:19.890> B 00:07:20.180 --> 00:07:20.190 align:start position:0% that if you do a you must then perform B 00:07:20.190 --> 00:07:24.020 align:start position:0% that if you do a you must then perform B and<00:07:20.550> if<00:07:21.210> you<00:07:21.390> do<00:07:21.780> B<00:07:22.140> you<00:07:22.620> must<00:07:22.890> not<00:07:23.160> perform<00:07:23.670> B 00:07:24.020 --> 00:07:24.030 align:start position:0% and if you do B you must not perform B 00:07:24.030 --> 00:07:26.480 align:start position:0% and if you do B you must not perform B and<00:07:24.390> if<00:07:25.350> you<00:07:25.500> breach<00:07:25.740> either<00:07:26.160> of<00:07:26.370> those 00:07:26.480 --> 00:07:26.490 align:start position:0% and if you breach either of those 00:07:26.490 --> 00:07:28.520 align:start position:0% and if you breach either of those commitments<00:07:26.850> then<00:07:27.780> you<00:07:27.900> are<00:07:28.050> in<00:07:28.260> breach<00:07:28.410> of 00:07:28.520 --> 00:07:28.530 align:start position:0% commitments then you are in breach of 00:07:28.530 --> 00:07:31.790 align:start position:0% commitments then you are in breach of contract<00:07:29.070> and<00:07:30.080> just<00:07:31.080> to<00:07:31.200> make<00:07:31.320> some<00:07:31.530> of<00:07:31.680> more 00:07:31.790 --> 00:07:31.800 align:start position:0% contract and just to make some of more 00:07:31.800 --> 00:07:33.650 align:start position:0% contract and just to make some of more later<00:07:32.100> slides<00:07:32.460> more<00:07:32.760> legible<00:07:33.150> we<00:07:33.420> sometimes 00:07:33.650 --> 00:07:33.660 align:start position:0% later slides more legible we sometimes 00:07:33.660 --> 00:07:37.100 align:start position:0% later slides more legible we sometimes omit<00:07:34.500> the<00:07:34.920> residual<00:07:35.700> clause<00:07:35.940> when<00:07:36.870> it<00:07:36.990> is 00:07:37.100 --> 00:07:37.110 align:start position:0% omit the residual clause when it is 00:07:37.110 --> 00:07:40.250 align:start position:0% omit the residual clause when it is unfulfilled<00:07:37.470> well<00:07:38.630> so<00:07:39.630> there<00:07:40.080> have<00:07:40.170> been 00:07:40.250 --> 00:07:40.260 align:start position:0% unfulfilled well so there have been 00:07:40.260 --> 00:07:45.500 align:start position:0% unfulfilled well so there have been several<00:07:40.590> semantics<00:07:41.300> that<00:07:42.740> have<00:07:44.090> been<00:07:45.090> defined 00:07:45.500 --> 00:07:45.510 align:start position:0% several semantics that have been defined 00:07:45.510 --> 00:07:48.020 align:start position:0% several semantics that have been defined for<00:07:45.750> this<00:07:46.350> language<00:07:46.850> originally<00:07:47.850> it<00:07:47.940> was 00:07:48.020 --> 00:07:48.030 align:start position:0% for this language originally it was 00:07:48.030 --> 00:07:50.000 align:start position:0% for this language originally it was equipped<00:07:48.300> with<00:07:48.480> branching<00:07:49.080> semantics<00:07:49.620> and 00:07:50.000 --> 00:07:50.010 align:start position:0% equipped with branching semantics and 00:07:50.010 --> 00:07:52.670 align:start position:0% equipped with branching semantics and the<00:07:50.970> idea<00:07:51.270> is<00:07:51.420> there<00:07:51.660> is<00:07:51.690> that<00:07:51.870> you<00:07:52.170> can<00:07:52.230> reason 00:07:52.670 --> 00:07:52.680 align:start position:0% the idea is there is that you can reason 00:07:52.680 --> 00:07:54.890 align:start position:0% the idea is there is that you can reason about<00:07:52.820> which<00:07:53.820> expressions<00:07:54.480> can<00:07:54.840> be 00:07:54.890 --> 00:07:54.900 align:start position:0% about which expressions can be 00:07:54.900 --> 00:07:57.470 align:start position:0% about which expressions can be substituted<00:07:55.770> for<00:07:55.919> each<00:07:56.010> other<00:07:56.220> and<00:07:56.520> the<00:07:57.090> sorts 00:07:57.470 --> 00:07:57.480 align:start position:0% substituted for each other and the sorts 00:07:57.480 --> 00:08:00.110 align:start position:0% substituted for each other and the sorts of<00:07:57.570> things<00:07:57.630> they<00:07:57.960> imply<00:07:58.290> for<00:07:59.280> example<00:07:59.730> you<00:07:59.940> can 00:08:00.110 --> 00:08:00.120 align:start position:0% of things they imply for example you can 00:08:00.120 --> 00:08:02.690 align:start position:0% of things they imply for example you can take<00:08:00.360> an<00:08:01.200> obligation<00:08:01.800> to<00:08:01.830> perform<00:08:02.310> some 00:08:02.690 --> 00:08:02.700 align:start position:0% take an obligation to perform some 00:08:02.700 --> 00:08:05.390 align:start position:0% take an obligation to perform some action<00:08:03.240> is<00:08:03.890> equivalent<00:08:04.890> to<00:08:04.980> the<00:08:05.220> prohibition 00:08:05.390 --> 00:08:05.400 align:start position:0% action is equivalent to the prohibition 00:08:05.400 --> 00:08:07.909 align:start position:0% action is equivalent to the prohibition from<00:08:06.000> not<00:08:06.210> performing<00:08:06.720> that<00:08:06.870> action<00:08:07.230> which 00:08:07.909 --> 00:08:07.919 align:start position:0% from not performing that action which 00:08:07.919 --> 00:08:10.250 align:start position:0% from not performing that action which seems<00:08:08.160> fairly<00:08:08.370> simple<00:08:08.990> we're<00:08:09.990> gonna<00:08:10.080> be 00:08:10.250 --> 00:08:10.260 align:start position:0% seems fairly simple we're gonna be 00:08:10.260 --> 00:08:13.070 align:start position:0% seems fairly simple we're gonna be focusing<00:08:10.650> here<00:08:10.950> mostly<00:08:11.400> on<00:08:11.700> Tracy<00:08:12.360> Mattox 00:08:13.070 --> 00:08:13.080 align:start position:0% focusing here mostly on Tracy Mattox 00:08:13.080 --> 00:08:16.790 align:start position:0% focusing here mostly on Tracy Mattox where<00:08:13.800> the<00:08:14.340> idea<00:08:14.730> is<00:08:15.090> I<00:08:15.570> want<00:08:16.200> to<00:08:16.260> say<00:08:16.470> that 00:08:16.790 --> 00:08:16.800 align:start position:0% where the idea is I want to say that 00:08:16.800 --> 00:08:19.640 align:start position:0% where the idea is I want to say that some<00:08:17.190> sequence<00:08:17.760> of<00:08:17.880> actions<00:08:18.360> is<00:08:18.720> consistent 00:08:19.640 --> 00:08:19.650 align:start position:0% some sequence of actions is consistent 00:08:19.650 --> 00:08:23.420 align:start position:0% some sequence of actions is consistent with<00:08:20.280> a<00:08:20.340> given<00:08:20.610> contract<00:08:21.950> you<00:08:22.950> can<00:08:23.100> read<00:08:23.310> this 00:08:23.420 --> 00:08:23.430 align:start position:0% with a given contract you can read this 00:08:23.430 --> 00:08:25.670 align:start position:0% with a given contract you can read this as<00:08:23.580> saying<00:08:23.790> the<00:08:24.120> sequence<00:08:24.510> of<00:08:24.750> performing<00:08:25.410> a 00:08:25.670 --> 00:08:25.680 align:start position:0% as saying the sequence of performing a 00:08:25.680 --> 00:08:30.220 align:start position:0% as saying the sequence of performing a and<00:08:26.610> then<00:08:27.030> later<00:08:27.330> B<00:08:28.070> as<00:08:29.070> the<00:08:29.520> claim<00:08:29.760> rather 00:08:30.220 --> 00:08:30.230 align:start position:0% and then later B as the claim rather 00:08:30.230 --> 00:08:32.360 align:start position:0% and then later B as the claim rather fulfills<00:08:31.230> the<00:08:31.500> contract<00:08:31.919> that<00:08:31.980> we<00:08:32.190> sold 00:08:32.360 --> 00:08:32.370 align:start position:0% fulfills the contract that we sold 00:08:32.370 --> 00:08:35.120 align:start position:0% fulfills the contract that we sold before<00:08:33.229> there<00:08:34.229> are<00:08:34.380> sets<00:08:34.650> inside<00:08:34.950> that 00:08:35.120 --> 00:08:35.130 align:start position:0% before there are sets inside that 00:08:35.130 --> 00:08:37.370 align:start position:0% before there are sets inside that sequence<00:08:35.490> to<00:08:35.640> accommodate<00:08:36.380> concurrent 00:08:37.370 --> 00:08:37.380 align:start position:0% sequence to accommodate concurrent 00:08:37.380 --> 00:08:43.339 align:start position:0% sequence to accommodate concurrent actions<00:08:37.830> and<00:08:41.450> I<00:08:42.450> seem<00:08:43.050> to<00:08:43.080> have<00:08:43.200> missed 00:08:43.339 --> 00:08:43.349 align:start position:0% actions and I seem to have missed 00:08:43.349 --> 00:08:45.650 align:start position:0% actions and I seem to have missed ordered<00:08:43.560> the<00:08:43.620> slides<00:08:43.830> but<00:08:44.730> essentially<00:08:45.420> the 00:08:45.650 --> 00:08:45.660 align:start position:0% ordered the slides but essentially the 00:08:45.660 --> 00:08:49.420 align:start position:0% ordered the slides but essentially the satisfaction<00:08:46.320> define<00:08:46.710> relation<00:08:47.700> is<00:08:48.200> defined 00:08:49.420 --> 00:08:49.430 align:start position:0% satisfaction define relation is defined 00:08:49.430 --> 00:08:52.550 align:start position:0% satisfaction define relation is defined pretty<00:08:50.430> much<00:08:50.610> as<00:08:50.880> you<00:08:51.210> would<00:08:51.330> expect<00:08:51.560> if 00:08:52.550 --> 00:08:52.560 align:start position:0% pretty much as you would expect if 00:08:52.560 --> 00:08:55.370 align:start position:0% pretty much as you would expect if you're<00:08:52.740> obliged<00:08:53.220> to<00:08:53.520> form<00:08:53.790> some<00:08:54.380> concurrent 00:08:55.370 --> 00:08:55.380 align:start position:0% you're obliged to form some concurrent 00:08:55.380 --> 00:08:56.720 align:start position:0% you're obliged to form some concurrent set<00:08:55.500> of<00:08:55.589> actions<00:08:56.040> then<00:08:56.339> you<00:08:56.430> should<00:08:56.610> perform 00:08:56.720 --> 00:08:56.730 align:start position:0% set of actions then you should perform 00:08:56.730 --> 00:08:58.550 align:start position:0% set of actions then you should perform them<00:08:57.180> or<00:08:57.420> otherwise<00:08:57.810> you<00:08:57.990> must<00:08:58.140> have<00:08:58.260> fill<00:08:58.410> the 00:08:58.550 --> 00:08:58.560 align:start position:0% them or otherwise you must have fill the 00:08:58.560 --> 00:09:02.120 align:start position:0% them or otherwise you must have fill the reparation<00:08:59.339> if<00:09:00.030> you<00:09:00.570> are<00:09:00.930> obliged<00:09:01.860> to<00:09:02.010> perform 00:09:02.120 --> 00:09:02.130 align:start position:0% reparation if you are obliged to perform 00:09:02.130 --> 00:09:03.990 align:start position:0% reparation if you are obliged to perform some<00:09:02.640> sequence<00:09:02.970> of<00:09:03.060> actions 00:09:03.990 --> 00:09:04.000 align:start position:0% some sequence of actions 00:09:04.000 --> 00:09:06.540 align:start position:0% some sequence of actions you<00:09:04.240> should<00:09:04.480> perform<00:09:04.720> one<00:09:05.440> and<00:09:05.920> then<00:09:06.250> the 00:09:06.540 --> 00:09:06.550 align:start position:0% you should perform one and then the 00:09:06.550 --> 00:09:08.310 align:start position:0% you should perform one and then the other<00:09:06.700> or<00:09:07.060> otherwise<00:09:07.390> fill<00:09:07.660> that<00:09:07.810> reparation 00:09:08.310 --> 00:09:08.320 align:start position:0% other or otherwise fill that reparation 00:09:08.320 --> 00:09:11.570 align:start position:0% other or otherwise fill that reparation and<00:09:08.710> this<00:09:09.700> sort<00:09:09.880> of<00:09:09.940> reasoning<00:09:10.180> is<00:09:10.570> enough<00:09:10.840> to 00:09:11.570 --> 00:09:11.580 align:start position:0% and this sort of reasoning is enough to 00:09:11.580 --> 00:09:16.200 align:start position:0% and this sort of reasoning is enough to derive<00:09:12.780> that<00:09:13.860> claim<00:09:14.860> we<00:09:15.220> made<00:09:15.430> before<00:09:15.610> if 00:09:16.200 --> 00:09:16.210 align:start position:0% derive that claim we made before if 00:09:16.210 --> 00:09:17.580 align:start position:0% derive that claim we made before if you'll<00:09:16.690> admit<00:09:16.810> the<00:09:17.110> somewhat<00:09:17.380> aggressive 00:09:17.580 --> 00:09:17.590 align:start position:0% you'll admit the somewhat aggressive 00:09:17.590 --> 00:09:21.960 align:start position:0% you'll admit the somewhat aggressive normalization<00:09:18.340> here<00:09:18.790> so<00:09:19.390> to<00:09:19.450> show<00:09:19.870> that<00:09:20.970> if 00:09:21.960 --> 00:09:21.970 align:start position:0% normalization here so to show that if 00:09:21.970 --> 00:09:25.800 align:start position:0% normalization here so to show that if you<00:09:22.480> do<00:09:22.690> a<00:09:23.140> you<00:09:24.010> must<00:09:24.490> do<00:09:24.670> B<00:09:24.970> and<00:09:25.300> if<00:09:25.360> you<00:09:25.450> do<00:09:25.570> B 00:09:25.800 --> 00:09:25.810 align:start position:0% you do a you must do B and if you do B 00:09:25.810 --> 00:09:30.330 align:start position:0% you do a you must do B and if you do B you<00:09:26.230> must<00:09:26.380> not<00:09:26.650> do<00:09:26.860> B<00:09:27.450> in<00:09:28.450> rough<00:09:29.140> sequence<00:09:29.590> well 00:09:30.330 --> 00:09:30.340 align:start position:0% you must not do B in rough sequence well 00:09:30.340 --> 00:09:32.550 align:start position:0% you must not do B in rough sequence well we<00:09:30.580> know<00:09:30.730> that<00:09:30.760> the<00:09:31.000> sequence<00:09:31.390> a<00:09:31.630> B<00:09:32.050> does<00:09:32.440> not 00:09:32.550 --> 00:09:32.560 align:start position:0% we know that the sequence a B does not 00:09:32.560 --> 00:09:35.160 align:start position:0% we know that the sequence a B does not involve<00:09:32.800> initially<00:09:33.340> doing<00:09:33.490> a<00:09:33.820> and<00:09:34.120> so<00:09:34.840> that 00:09:35.160 --> 00:09:35.170 align:start position:0% involve initially doing a and so that 00:09:35.170 --> 00:09:37.380 align:start position:0% involve initially doing a and so that Clause<00:09:35.410> is<00:09:35.440> trivially<00:09:35.950> fulfilled<00:09:36.310> and<00:09:36.730> in<00:09:37.240> the 00:09:37.380 --> 00:09:37.390 align:start position:0% Clause is trivially fulfilled and in the 00:09:37.390 --> 00:09:38.700 align:start position:0% Clause is trivially fulfilled and in the other<00:09:37.480> clause<00:09:37.720> because<00:09:38.050> we<00:09:38.140> do<00:09:38.260> a<00:09:38.290> initially 00:09:38.700 --> 00:09:38.710 align:start position:0% other clause because we do a initially 00:09:38.710 --> 00:09:41.580 align:start position:0% other clause because we do a initially we<00:09:39.130> have<00:09:39.250> a<00:09:39.280> residual<00:09:39.960> we<00:09:40.960> have<00:09:41.200> the<00:09:41.290> residual 00:09:41.580 --> 00:09:41.590 align:start position:0% we have a residual we have the residual 00:09:41.590 --> 00:09:43.170 align:start position:0% we have a residual we have the residual obligation<00:09:42.040> of<00:09:42.160> having<00:09:42.190> to<00:09:42.520> do<00:09:42.640> B<00:09:42.820> and<00:09:43.060> that's 00:09:43.170 --> 00:09:43.180 align:start position:0% obligation of having to do B and that's 00:09:43.180 --> 00:09:44.730 align:start position:0% obligation of having to do B and that's a<00:09:43.270> filled<00:09:43.480> by<00:09:43.630> the<00:09:43.690> second<00:09:44.110> component<00:09:44.530> in<00:09:44.620> the 00:09:44.730 --> 00:09:44.740 align:start position:0% a filled by the second component in the 00:09:44.740 --> 00:09:52.610 align:start position:0% a filled by the second component in the sequence 00:09:52.610 --> 00:09:52.620 align:start position:0% 00:09:52.620 --> 00:09:56.900 align:start position:0% I'm<00:09:53.160> going<00:09:53.490> on<00:09:53.580> the<00:09:53.640> wrong<00:09:53.820> order<00:09:55.670> it's<00:09:56.670> the 00:09:56.900 --> 00:09:56.910 align:start position:0% I'm going on the wrong order it's the 00:09:56.910 --> 00:09:59.000 align:start position:0% I'm going on the wrong order it's the other<00:09:57.330> way<00:09:57.420> button<00:09:57.690> the<00:09:57.840> down<00:09:58.050> button<00:09:58.320> yes<00:09:58.860> the 00:09:59.000 --> 00:09:59.010 align:start position:0% other way button the down button yes the 00:09:59.010 --> 00:10:06.740 align:start position:0% other way button the down button yes the down<00:09:59.160> thank<00:09:59.790> you<00:09:59.880> for<00:10:00.030> the<00:10:00.120> down<00:10:00.270> button<00:10:05.750> so 00:10:06.740 --> 00:10:06.750 align:start position:0% down thank you for the down button so 00:10:06.750 --> 00:10:09.290 align:start position:0% down thank you for the down button so that's<00:10:07.590> really<00:10:07.860> well<00:10:08.040> but<00:10:08.940> the<00:10:09.120> cool<00:10:09.270> thing 00:10:09.290 --> 00:10:09.300 align:start position:0% that's really well but the cool thing 00:10:09.300 --> 00:10:10.970 align:start position:0% that's really well but the cool thing about<00:10:09.480> this<00:10:09.960> particular<00:10:10.380> satisfaction 00:10:10.970 --> 00:10:10.980 align:start position:0% about this particular satisfaction 00:10:10.980 --> 00:10:14.600 align:start position:0% about this particular satisfaction relation<00:10:11.700> is<00:10:11.940> its<00:10:12.450> decidable<00:10:13.170> and<00:10:13.440> there's<00:10:14.310> a 00:10:14.600 --> 00:10:14.610 align:start position:0% relation is its decidable and there's a 00:10:14.610 --> 00:10:17.810 align:start position:0% relation is its decidable and there's a rendering<00:10:14.970> on<00:10:15.300> to<00:10:15.570> automata<00:10:16.200> so<00:10:16.560> that<00:10:16.890> you<00:10:17.640> can 00:10:17.810 --> 00:10:17.820 align:start position:0% rendering on to automata so that you can 00:10:17.820 --> 00:10:19.730 align:start position:0% rendering on to automata so that you can essentially<00:10:18.120> just<00:10:18.390> pass<00:10:18.600> these<00:10:18.840> things<00:10:19.260> to 00:10:19.730 --> 00:10:19.740 align:start position:0% essentially just pass these things to 00:10:19.740 --> 00:10:22.930 align:start position:0% essentially just pass these things to this<00:10:20.130> machine<00:10:20.340> and<00:10:20.880> it<00:10:21.450> can<00:10:21.600> tell<00:10:21.810> you<00:10:21.990> whether 00:10:22.930 --> 00:10:22.940 align:start position:0% this machine and it can tell you whether 00:10:22.940 --> 00:10:26.300 align:start position:0% this machine and it can tell you whether you're<00:10:23.940> in<00:10:24.210> compliance<00:10:24.660> or<00:10:25.050> in<00:10:25.650> breach<00:10:25.950> or 00:10:26.300 --> 00:10:26.310 align:start position:0% you're in compliance or in breach or 00:10:26.310 --> 00:10:29.210 align:start position:0% you're in compliance or in breach or whether<00:10:27.000> you<00:10:27.210> have<00:10:27.420> residual<00:10:28.220> obligations 00:10:29.210 --> 00:10:29.220 align:start position:0% whether you have residual obligations 00:10:29.220 --> 00:10:32.630 align:start position:0% whether you have residual obligations which<00:10:29.550> later<00:10:30.060> actions<00:10:31.050> in<00:10:31.290> the<00:10:31.410> trace<00:10:31.650> may<00:10:32.490> or 00:10:32.630 --> 00:10:32.640 align:start position:0% which later actions in the trace may or 00:10:32.640 --> 00:10:38.510 align:start position:0% which later actions in the trace may or may<00:10:32.790> not<00:10:32.820> let<00:10:33.210> you<00:10:33.240> fulfill<00:10:36.590> and<00:10:37.590> the<00:10:38.370> cool 00:10:38.510 --> 00:10:38.520 align:start position:0% may not let you fulfill and the cool 00:10:38.520 --> 00:10:40.940 align:start position:0% may not let you fulfill and the cool thing<00:10:38.670> about<00:10:38.700> these<00:10:39.000> graphs<00:10:39.440> this<00:10:40.440> is<00:10:40.500> an 00:10:40.940 --> 00:10:40.950 align:start position:0% thing about these graphs this is an 00:10:40.950 --> 00:10:43.370 align:start position:0% thing about these graphs this is an alternative<00:10:41.610> alternating<00:10:42.390> all<00:10:42.480> automata<00:10:42.690> but 00:10:43.370 --> 00:10:43.380 align:start position:0% alternative alternating all automata but 00:10:43.380 --> 00:10:44.870 align:start position:0% alternative alternating all automata but it<00:10:43.470> doesn't<00:10:43.680> have<00:10:43.770> to<00:10:43.920> be<00:10:44.040> but<00:10:44.400> never<00:10:44.670> mind 00:10:44.870 --> 00:10:44.880 align:start position:0% it doesn't have to be but never mind 00:10:44.880 --> 00:10:48.680 align:start position:0% it doesn't have to be but never mind because<00:10:45.060> time<00:10:46.280> is<00:10:47.280> that<00:10:47.760> you<00:10:48.000> can<00:10:48.180> do<00:10:48.330> a<00:10:48.360> bunch 00:10:48.680 --> 00:10:48.690 align:start position:0% because time is that you can do a bunch 00:10:48.690 --> 00:10:51.410 align:start position:0% because time is that you can do a bunch of<00:10:48.900> analyses<00:10:49.320> about<00:10:49.590> these<00:10:49.740> which<00:10:50.040> say<00:10:50.420> which 00:10:51.410 --> 00:10:51.420 align:start position:0% of analyses about these which say which 00:10:51.420 --> 00:10:52.730 align:start position:0% of analyses about these which say which tell<00:10:51.660> you<00:10:51.750> properties<00:10:52.080> about<00:10:52.200> your<00:10:52.350> contract 00:10:52.730 --> 00:10:52.740 align:start position:0% tell you properties about your contract 00:10:52.740 --> 00:10:54.440 align:start position:0% tell you properties about your contract so<00:10:52.950> you<00:10:53.010> can<00:10:53.220> say<00:10:53.370> that<00:10:53.550> the<00:10:53.670> sequence<00:10:53.910> a<00:10:54.210> B 00:10:54.440 --> 00:10:54.450 align:start position:0% so you can say that the sequence a B 00:10:54.450 --> 00:10:56.510 align:start position:0% so you can say that the sequence a B satisfies<00:10:55.050> it<00:10:55.260> and<00:10:55.470> so<00:10:55.560> to<00:10:55.620> the<00:10:55.740> sequence<00:10:56.070> a<00:10:56.280> a 00:10:56.510 --> 00:10:56.520 align:start position:0% satisfies it and so to the sequence a a 00:10:56.520 --> 00:10:59.200 align:start position:0% satisfies it and so to the sequence a a and<00:10:56.820> B<00:10:57.000> and<00:10:57.300> so<00:10:57.780> does<00:10:57.960> the<00:10:58.020> sequence<00:10:58.260> B<00:10:58.620> a 00:10:59.200 --> 00:10:59.210 align:start position:0% and B and so does the sequence B a 00:10:59.210 --> 00:11:02.810 align:start position:0% and B and so does the sequence B a because<00:11:00.210> that<00:11:00.590> validates<00:11:01.590> in<00:11:01.950> both<00:11:02.250> automata 00:11:02.810 --> 00:11:02.820 align:start position:0% because that validates in both automata 00:11:02.820 --> 00:11:05.000 align:start position:0% because that validates in both automata you<00:11:03.570> can<00:11:03.720> say<00:11:03.930> further<00:11:04.470> that<00:11:04.830> it's 00:11:05.000 --> 00:11:05.010 align:start position:0% you can say further that it's 00:11:05.010 --> 00:11:07.430 align:start position:0% you can say further that it's satisfiable<00:11:05.640> because<00:11:05.970> there<00:11:06.240> exists<00:11:06.810> a<00:11:06.930> trace 00:11:07.430 --> 00:11:07.440 align:start position:0% satisfiable because there exists a trace 00:11:07.440 --> 00:11:14.870 align:start position:0% satisfiable because there exists a trace which<00:11:08.040> is<00:11:08.190> compliant<00:11:13.430> another<00:11:14.430> interesting 00:11:14.870 --> 00:11:14.880 align:start position:0% which is compliant another interesting 00:11:14.880 --> 00:11:16.700 align:start position:0% which is compliant another interesting thing<00:11:14.910> about<00:11:15.180> this<00:11:15.420> particular<00:11:15.750> automata<00:11:16.290> is 00:11:16.700 --> 00:11:16.710 align:start position:0% thing about this particular automata is 00:11:16.710 --> 00:11:19.820 align:start position:0% thing about this particular automata is that<00:11:17.130> if<00:11:17.340> you<00:11:17.430> consider<00:11:17.700> the<00:11:18.620> sequence<00:11:19.620> in 00:11:19.820 --> 00:11:19.830 align:start position:0% that if you consider the sequence in 00:11:19.830 --> 00:11:21.980 align:start position:0% that if you consider the sequence in which<00:11:19.860> you<00:11:20.100> initially<00:11:20.490> perform<00:11:20.880> both<00:11:21.150> a<00:11:21.360> and<00:11:21.780> B 00:11:21.980 --> 00:11:21.990 align:start position:0% which you initially perform both a and B 00:11:21.990 --> 00:11:24.440 align:start position:0% which you initially perform both a and B at<00:11:22.170> the<00:11:22.290> same<00:11:22.500> time<00:11:22.770> there<00:11:23.490> is<00:11:23.580> no<00:11:23.730> valid<00:11:24.090> trace 00:11:24.440 --> 00:11:24.450 align:start position:0% at the same time there is no valid trace 00:11:24.450 --> 00:11:28.520 align:start position:0% at the same time there is no valid trace that<00:11:26.300> valid<00:11:27.300> extension<00:11:27.750> of<00:11:27.840> that<00:11:27.870> trace<00:11:28.200> and 00:11:28.520 --> 00:11:28.530 align:start position:0% that valid extension of that trace and 00:11:28.530 --> 00:11:30.740 align:start position:0% that valid extension of that trace and so<00:11:28.740> with<00:11:29.190> respect<00:11:29.280> to<00:11:29.700> your<00:11:30.030> standard<00:11:30.510> tre 00:11:30.740 --> 00:11:30.750 align:start position:0% so with respect to your standard tre 00:11:30.750 --> 00:11:34.970 align:start position:0% so with respect to your standard tre semantics<00:11:31.940> that's<00:11:32.940> probably<00:11:33.780> fine<00:11:34.110> but<00:11:34.860> we 00:11:34.970 --> 00:11:34.980 align:start position:0% semantics that's probably fine but we 00:11:34.980 --> 00:11:37.040 align:start position:0% semantics that's probably fine but we see<00:11:35.130> something<00:11:35.340> here<00:11:35.640> we<00:11:35.910> see<00:11:36.090> that<00:11:36.300> at<00:11:36.840> this 00:11:37.040 --> 00:11:37.050 align:start position:0% see something here we see that at this 00:11:37.050 --> 00:11:38.390 align:start position:0% see something here we see that at this coordinate<00:11:37.500> we<00:11:37.710> have<00:11:37.890> the<00:11:38.010> deontic 00:11:38.390 --> 00:11:38.400 align:start position:0% coordinate we have the deontic 00:11:38.400 --> 00:11:40.970 align:start position:0% coordinate we have the deontic obligation<00:11:38.970> to<00:11:39.150> perform<00:11:39.300> both<00:11:39.810> B<00:11:40.080> and<00:11:40.110> not 00:11:40.970 --> 00:11:40.980 align:start position:0% obligation to perform both B and not 00:11:40.980 --> 00:11:43.490 align:start position:0% obligation to perform both B and not perform<00:11:41.400> B<00:11:41.550> ie<00:11:42.270> the<00:11:42.570> contract<00:11:43.020> is<00:11:43.140> telling<00:11:43.410> us 00:11:43.490 --> 00:11:43.500 align:start position:0% perform B ie the contract is telling us 00:11:43.500 --> 00:11:46.330 align:start position:0% perform B ie the contract is telling us that<00:11:43.560> under<00:11:43.860> some<00:11:44.160> sequence<00:11:44.640> that<00:11:45.480> we<00:11:45.660> have 00:11:46.330 --> 00:11:46.340 align:start position:0% that under some sequence that we have 00:11:46.340 --> 00:11:48.770 align:start position:0% that under some sequence that we have conflicting<00:11:47.340> obligations<00:11:48.210> and<00:11:48.510> this<00:11:48.630> is 00:11:48.770 --> 00:11:48.780 align:start position:0% conflicting obligations and this is 00:11:48.780 --> 00:11:54.550 align:start position:0% conflicting obligations and this is somewhat<00:11:49.080> undesirable<00:11:49.800> and<00:11:50.840> so<00:11:53.210> there<00:11:54.210> was 00:11:54.550 --> 00:11:54.560 align:start position:0% somewhat undesirable and so there was 00:11:54.560 --> 00:11:58.340 align:start position:0% somewhat undesirable and so there was another<00:11:55.560> paper<00:11:55.800> which<00:11:56.250> essentially<00:11:57.350> extended 00:11:58.340 --> 00:11:58.350 align:start position:0% another paper which essentially extended 00:11:58.350 --> 00:11:59.960 align:start position:0% another paper which essentially extended the<00:11:58.440> semantics<00:11:58.860> to<00:11:59.040> account<00:11:59.280> for<00:11:59.400> the<00:11:59.820> G<00:11:59.910> on 00:11:59.960 --> 00:11:59.970 align:start position:0% the semantics to account for the G on 00:11:59.970 --> 00:12:01.160 align:start position:0% the semantics to account for the G on take<00:12:00.120> responsibility<00:12:00.780> is<00:12:00.930> it<00:12:01.080> each 00:12:01.160 --> 00:12:01.170 align:start position:0% take responsibility is it each 00:12:01.170 --> 00:12:05.620 align:start position:0% take responsibility is it each coordinate<00:12:01.560> and<00:12:03.260> essentially<00:12:04.260> designed<00:12:04.530> what 00:12:05.620 --> 00:12:05.630 align:start position:0% coordinate and essentially designed what 00:12:05.630 --> 00:12:08.260 align:start position:0% coordinate and essentially designed what patterns<00:12:06.170> you<00:12:06.380> need<00:12:06.500> to<00:12:06.590> fulfill<00:12:06.710> in<00:12:07.340> order<00:12:08.090> to 00:12:08.260 --> 00:12:08.270 align:start position:0% patterns you need to fulfill in order to 00:12:08.270 --> 00:12:11.830 align:start position:0% patterns you need to fulfill in order to not<00:12:08.570> have<00:12:08.870> a<00:12:10.030> conflict<00:12:11.030> and<00:12:11.510> this<00:12:11.600> should<00:12:11.720> be 00:12:11.830 --> 00:12:11.840 align:start position:0% not have a conflict and this should be 00:12:11.840 --> 00:12:14.620 align:start position:0% not have a conflict and this should be true<00:12:12.050> of<00:12:12.410> all<00:12:12.800> traces<00:12:13.520> you<00:12:14.180> can<00:12:14.300> render<00:12:14.450> this 00:12:14.620 --> 00:12:14.630 align:start position:0% true of all traces you can render this 00:12:14.630 --> 00:12:16.000 align:start position:0% true of all traces you can render this into<00:12:14.810> an<00:12:14.900> automata<00:12:15.260> but<00:12:15.590> you're<00:12:15.710> mushing 00:12:16.000 --> 00:12:16.010 align:start position:0% into an automata but you're mushing 00:12:16.010 --> 00:12:17.350 align:start position:0% into an automata but you're mushing things<00:12:16.220> together<00:12:16.370> so<00:12:16.640> all<00:12:17.120> the<00:12:17.210> obligations 00:12:17.350 --> 00:12:17.360 align:start position:0% things together so all the obligations 00:12:17.360 --> 00:12:20.740 align:start position:0% things together so all the obligations are<00:12:17.900> in<00:12:18.020> the<00:12:18.110> same<00:12:18.260> place<00:12:18.500> and<00:12:19.390> then<00:12:20.390> you<00:12:20.570> just 00:12:20.740 --> 00:12:20.750 align:start position:0% are in the same place and then you just 00:12:20.750 --> 00:12:21.900 align:start position:0% are in the same place and then you just pattern<00:12:21.020> match<00:12:21.170> on<00:12:21.350> these<00:12:21.530> to<00:12:21.770> determine 00:12:21.900 --> 00:12:21.910 align:start position:0% pattern match on these to determine 00:12:21.910 --> 00:12:24.810 align:start position:0% pattern match on these to determine whether<00:12:22.910> you're<00:12:23.150> saying<00:12:23.540> two<00:12:23.930> things<00:12:24.200> which 00:12:24.810 --> 00:12:24.820 align:start position:0% whether you're saying two things which 00:12:24.820 --> 00:12:28.480 align:start position:0% whether you're saying two things which you<00:12:25.820> should<00:12:26.000> not<00:12:26.150> be<00:12:26.330> saying<00:12:26.510> at<00:12:27.380> the<00:12:28.190> same 00:12:28.480 --> 00:12:28.490 align:start position:0% you should not be saying at the same 00:12:28.490 --> 00:12:37.990 align:start position:0% you should not be saying at the same time<00:12:32.170> okay<00:12:33.170> so<00:12:35.290> okay<00:12:36.290> so<00:12:36.860> this<00:12:37.010> is<00:12:37.190> so<00:12:37.790> this<00:12:37.880> is 00:12:37.990 --> 00:12:38.000 align:start position:0% time okay so okay so this is so this is 00:12:38.000 --> 00:12:42.340 align:start position:0% time okay so okay so this is so this is the<00:12:38.030> one<00:12:38.240> that<00:12:38.420> I<00:12:38.600> liked<00:12:38.870> best<00:12:39.170> so<00:12:39.560> I<00:12:39.790> am<00:12:41.350> so 00:12:42.340 --> 00:12:42.350 align:start position:0% the one that I liked best so I am so 00:12:42.350 --> 00:12:44.860 align:start position:0% the one that I liked best so I am so this<00:12:42.500> one's<00:12:42.710> a<00:12:42.770> little<00:12:42.890> neat<00:12:43.100> because<00:12:43.730> so<00:12:44.630> this 00:12:44.860 --> 00:12:44.870 align:start position:0% this one's a little neat because so this 00:12:44.870 --> 00:12:47.890 align:start position:0% this one's a little neat because so this so<00:12:45.110> goes<00:12:45.350> okay<00:12:45.920> the<00:12:46.070> previous<00:12:46.490> one<00:12:46.670> you<00:12:46.700> saw<00:12:47.090> it 00:12:47.890 --> 00:12:47.900 align:start position:0% so goes okay the previous one you saw it 00:12:47.900 --> 00:12:49.450 align:start position:0% so goes okay the previous one you saw it gives<00:12:48.140> a<00:12:48.380> really<00:12:48.650> nice<00:12:48.740> flexible<00:12:49.250> way<00:12:49.370> of 00:12:49.450 --> 00:12:49.460 align:start position:0% gives a really nice flexible way of 00:12:49.460 --> 00:12:51.400 align:start position:0% gives a really nice flexible way of representing<00:12:49.820> contracts<00:12:50.330> but<00:12:50.780> when<00:12:51.050> the 00:12:51.400 --> 00:12:51.410 align:start position:0% representing contracts but when the 00:12:51.410 --> 00:12:53.710 align:start position:0% representing contracts but when the hits<00:12:51.620> the<00:12:51.680> fan<00:12:51.800> you<00:12:52.520> don't<00:12:52.730> know<00:12:52.970> know<00:12:53.300> whom<00:12:53.540> to 00:12:53.710 --> 00:12:53.720 align:start position:0% hits the fan you don't know know whom to 00:12:53.720 --> 00:12:54.970 align:start position:0% hits the fan you don't know know whom to blame<00:12:53.810> and<00:12:54.290> you're<00:12:54.530> like<00:12:54.620> oh<00:12:54.740> you<00:12:54.860> always 00:12:54.970 --> 00:12:54.980 align:start position:0% blame and you're like oh you always 00:12:54.980 --> 00:12:58.660 align:start position:0% blame and you're like oh you always gonna<00:12:55.100> blame<00:12:55.340> someone<00:12:55.370> right<00:12:55.820> and<00:12:56.560> and<00:12:57.670> in 00:12:58.660 --> 00:12:58.670 align:start position:0% gonna blame someone right and and in 00:12:58.670 --> 00:13:01.630 align:start position:0% gonna blame someone right and and in particular<00:12:59.350> so<00:13:00.350> this<00:13:00.590> is<00:13:00.770> this<00:13:00.920> is<00:13:01.130> a<00:13:01.160> sort<00:13:01.610> of 00:13:01.630 --> 00:13:01.640 align:start position:0% particular so this is this is a sort of 00:13:01.640 --> 00:13:03.850 align:start position:0% particular so this is this is a sort of a<00:13:01.730> novel<00:13:02.150> approach<00:13:02.270> that<00:13:03.050> allows<00:13:03.170> you<00:13:03.560> to<00:13:03.620> say 00:13:03.850 --> 00:13:03.860 align:start position:0% a novel approach that allows you to say 00:13:03.860 --> 00:13:06.070 align:start position:0% a novel approach that allows you to say oh<00:13:03.890> well<00:13:04.550> when<00:13:05.030> when<00:13:05.450> someone<00:13:05.810> doesn't 00:13:06.070 --> 00:13:06.080 align:start position:0% oh well when when someone doesn't 00:13:06.080 --> 00:13:10.480 align:start position:0% oh well when when someone doesn't doesn't<00:13:06.500> do<00:13:06.860> their<00:13:07.340> job<00:13:07.750> it<00:13:08.750> says<00:13:09.260> so<00:13:09.470> and<00:13:09.740> you 00:13:10.480 --> 00:13:10.490 align:start position:0% doesn't do their job it says so and you 00:13:10.490 --> 00:13:11.650 align:start position:0% doesn't do their job it says so and you know<00:13:10.550> you<00:13:10.610> can<00:13:10.790> see<00:13:10.880> exactly<00:13:11.150> who<00:13:11.360> that<00:13:11.390> is 00:13:11.650 --> 00:13:11.660 align:start position:0% know you can see exactly who that is 00:13:11.660 --> 00:13:14.290 align:start position:0% know you can see exactly who that is this<00:13:12.140> is<00:13:12.320> nice<00:13:12.500> because<00:13:13.090> then<00:13:14.090> you<00:13:14.210> could 00:13:14.290 --> 00:13:14.300 align:start position:0% this is nice because then you could 00:13:14.300 --> 00:13:17.740 align:start position:0% this is nice because then you could hypothetically<00:13:15.730> aetherium<00:13:16.730> eyes<00:13:16.970> judges<00:13:17.510> and 00:13:17.740 --> 00:13:17.750 align:start position:0% hypothetically aetherium eyes judges and 00:13:17.750 --> 00:13:19.720 align:start position:0% hypothetically aetherium eyes judges and this<00:13:18.110> is<00:13:18.260> one<00:13:18.440> where<00:13:18.590> the<00:13:18.680> lawyers<00:13:19.040> would<00:13:19.580> like 00:13:19.720 --> 00:13:19.730 align:start position:0% this is one where the lawyers would like 00:13:19.730 --> 00:13:22.690 align:start position:0% this is one where the lawyers would like fully<00:13:20.000> join<00:13:20.300> us<00:13:20.480> and<00:13:20.660> that<00:13:21.020> would<00:13:21.140> be<00:13:21.230> great<00:13:21.700> so 00:13:22.690 --> 00:13:22.700 align:start position:0% fully join us and that would be great so 00:13:22.700 --> 00:13:25.630 align:start position:0% fully join us and that would be great so so<00:13:23.150> right<00:13:23.660> now<00:13:24.050> the<00:13:24.110> way<00:13:24.530> things<00:13:24.560> go<00:13:25.010> is<00:13:25.250> that 00:13:25.630 --> 00:13:25.640 align:start position:0% so right now the way things go is that 00:13:25.640 --> 00:13:26.800 align:start position:0% so right now the way things go is that you<00:13:25.820> would<00:13:25.970> write<00:13:26.090> your<00:13:26.270> things<00:13:26.540> your 00:13:26.800 --> 00:13:26.810 align:start position:0% you would write your things your 00:13:26.810 --> 00:13:28.960 align:start position:0% you would write your things your anything<00:13:26.960> is<00:13:27.140> a<00:13:27.170> little<00:13:27.350> contract<00:13:27.680> but<00:13:28.640> but 00:13:28.960 --> 00:13:28.970 align:start position:0% anything is a little contract but but 00:13:28.970 --> 00:13:30.940 align:start position:0% anything is a little contract but but when<00:13:29.120> it<00:13:29.210> goes<00:13:29.330> awry<00:13:29.660> I<00:13:29.900> mean<00:13:30.530> you<00:13:30.680> still<00:13:30.860> have 00:13:30.940 --> 00:13:30.950 align:start position:0% when it goes awry I mean you still have 00:13:30.950 --> 00:13:32.230 align:start position:0% when it goes awry I mean you still have to<00:13:31.010> go<00:13:31.100> to<00:13:31.130> go<00:13:31.370> back<00:13:31.460> to<00:13:31.730> the<00:13:31.850> traditional 00:13:32.230 --> 00:13:32.240 align:start position:0% to go to go back to the traditional 00:13:32.240 --> 00:13:35.230 align:start position:0% to go to go back to the traditional legal<00:13:32.510> system<00:13:32.870> so<00:13:33.560> this<00:13:33.950> ideas<00:13:34.190> them<00:13:35.060> at<00:13:35.120> all 00:13:35.230 --> 00:13:35.240 align:start position:0% legal system so this ideas them at all 00:13:35.240 --> 00:13:37.210 align:start position:0% legal system so this ideas them at all because<00:13:35.540> you<00:13:35.900> know<00:13:36.020> exactly<00:13:36.410> who<00:13:36.800> is<00:13:36.950> to<00:13:37.100> blame 00:13:37.210 --> 00:13:37.220 align:start position:0% because you know exactly who is to blame 00:13:37.220 --> 00:13:40.300 align:start position:0% because you know exactly who is to blame for<00:13:37.790> every<00:13:38.150> possible<00:13:38.710> every<00:13:39.710> possible<00:13:40.010> path 00:13:40.300 --> 00:13:40.310 align:start position:0% for every possible every possible path 00:13:40.310 --> 00:13:42.520 align:start position:0% for every possible every possible path through<00:13:40.570> through<00:13:41.570> through<00:13:41.750> the<00:13:41.780> contract<00:13:42.290> and 00:13:42.520 --> 00:13:42.530 align:start position:0% through through through the contract and 00:13:42.530 --> 00:13:44.680 align:start position:0% through through through the contract and that<00:13:42.800> would<00:13:42.920> just<00:13:42.950> be<00:13:43.160> great<00:13:43.450> so<00:13:44.450> I'll<00:13:44.570> show 00:13:44.680 --> 00:13:44.690 align:start position:0% that would just be great so I'll show 00:13:44.690 --> 00:13:47.020 align:start position:0% that would just be great so I'll show you<00:13:44.720> roughly<00:13:44.840> how<00:13:45.080> it<00:13:45.230> goes<00:13:45.410> so<00:13:46.400> this<00:13:46.700> button 00:13:47.020 --> 00:13:47.030 align:start position:0% you roughly how it goes so this button 00:13:47.030 --> 00:13:49.990 align:start position:0% you roughly how it goes so this button so<00:13:47.930> basically<00:13:48.200> there<00:13:48.530> is<00:13:48.560> a<00:13:48.980> verdict<00:13:49.460> which<00:13:49.850> is 00:13:49.990 --> 00:13:50.000 align:start position:0% so basically there is a verdict which is 00:13:50.000 --> 00:13:52.420 align:start position:0% so basically there is a verdict which is V<00:13:50.270> and<00:13:50.480> there's<00:13:51.110> two<00:13:51.320> ways<00:13:51.470> a<00:13:51.830> verdict<00:13:52.160> can<00:13:52.280> go 00:13:52.420 --> 00:13:52.430 align:start position:0% V and there's two ways a verdict can go 00:13:52.430 --> 00:13:53.740 align:start position:0% V and there's two ways a verdict can go over<00:13:52.550> a<00:13:52.580> contract<00:13:53.000> it<00:13:53.180> can<00:13:53.270> be<00:13:53.360> a<00:13:53.420> check<00:13:53.600> mark 00:13:53.740 --> 00:13:53.750 align:start position:0% over a contract it can be a check mark 00:13:53.750 --> 00:13:55.540 align:start position:0% over a contract it can be a check mark which<00:13:53.990> means<00:13:54.020> everything's<00:13:54.500> great<00:13:54.740> or<00:13:55.220> it<00:13:55.460> can 00:13:55.540 --> 00:13:55.550 align:start position:0% which means everything's great or it can 00:13:55.550 --> 00:13:57.580 align:start position:0% which means everything's great or it can say<00:13:55.790> there's<00:13:56.450> a<00:13:56.540> time<00:13:56.720> stamp<00:13:56.960> with<00:13:57.320> a<00:13:57.350> little 00:13:57.580 --> 00:13:57.590 align:start position:0% say there's a time stamp with a little 00:13:57.590 --> 00:13:59.620 align:start position:0% say there's a time stamp with a little towel<00:13:57.860> and<00:13:58.220> there's<00:13:58.580> a<00:13:58.640> blame<00:13:58.850> mean<00:13:59.210> someone 00:13:59.620 --> 00:13:59.630 align:start position:0% towel and there's a blame mean someone 00:13:59.630 --> 00:14:02.320 align:start position:0% towel and there's a blame mean someone need<00:13:59.840> someone<00:14:00.380> someone<00:14:00.980> up<00:14:01.330> and 00:14:02.320 --> 00:14:02.330 align:start position:0% need someone someone up and 00:14:02.330 --> 00:14:05.380 align:start position:0% need someone someone up and basically<00:14:02.570> and<00:14:02.810> every<00:14:03.260> contract<00:14:03.890> is<00:14:04.730> defined 00:14:05.380 --> 00:14:05.390 align:start position:0% basically and every contract is defined 00:14:05.390 --> 00:14:07.960 align:start position:0% basically and every contract is defined as<00:14:05.750> a<00:14:05.810> function<00:14:06.500> that<00:14:06.980> map's<00:14:07.580> sort<00:14:07.880> of<00:14:07.940> a 00:14:07.960 --> 00:14:07.970 align:start position:0% as a function that map's sort of a 00:14:07.970 --> 00:14:09.940 align:start position:0% as a function that map's sort of a sequence<00:14:08.450> of<00:14:08.570> events<00:14:08.990> or<00:14:09.170> sequence<00:14:09.890> of 00:14:09.940 --> 00:14:09.950 align:start position:0% sequence of events or sequence of 00:14:09.950 --> 00:14:13.540 align:start position:0% sequence of events or sequence of actions<00:14:10.400> Sigma<00:14:10.970> to<00:14:11.960> either<00:14:12.200> a<00:14:12.500> a<00:14:13.130> check<00:14:13.400> mark 00:14:13.540 --> 00:14:13.550 align:start position:0% actions Sigma to either a a check mark 00:14:13.550 --> 00:14:15.820 align:start position:0% actions Sigma to either a a check mark meaning<00:14:13.910> it's<00:14:14.000> great<00:14:14.240> or<00:14:14.690> a<00:14:14.750> timestamp<00:14:15.530> and 00:14:15.820 --> 00:14:15.830 align:start position:0% meaning it's great or a timestamp and 00:14:15.830 --> 00:14:16.780 align:start position:0% meaning it's great or a timestamp and then<00:14:16.070> in 00:14:16.780 --> 00:14:16.790 align:start position:0% then in 00:14:16.790 --> 00:14:19.930 align:start position:0% then in someone<00:14:17.360> up<00:14:17.890> and<00:14:18.890> yeah<00:14:19.310> so<00:14:19.580> in<00:14:19.790> like 00:14:19.930 --> 00:14:19.940 align:start position:0% someone up and yeah so in like 00:14:19.940 --> 00:14:22.030 align:start position:0% someone up and yeah so in like and<00:14:20.150> like<00:14:20.270> that's<00:14:20.720> it<00:14:20.960> and<00:14:21.260> so<00:14:21.740> you<00:14:21.830> can<00:14:21.860> say<00:14:21.980> oh 00:14:22.030 --> 00:14:22.040 align:start position:0% and like that's it and so you can say oh 00:14:22.040 --> 00:14:24.810 align:start position:0% and like that's it and so you can say oh okay<00:14:22.580> so<00:14:22.640> and<00:14:23.030> so<00:14:23.330> you<00:14:23.390> can<00:14:23.570> fully<00:14:23.750> describe 00:14:24.810 --> 00:14:24.820 align:start position:0% okay so and so you can fully describe 00:14:24.820 --> 00:14:26.620 align:start position:0% okay so and so you can fully describe the<00:14:25.820> ways<00:14:25.940> through<00:14:26.060> a<00:14:26.150> contract<00:14:26.510> through 00:14:26.620 --> 00:14:26.630 align:start position:0% the ways through a contract through 00:14:26.630 --> 00:14:29.290 align:start position:0% the ways through a contract through through<00:14:26.900> all<00:14:27.050> these<00:14:27.200> different<00:14:27.290> Sigma's<00:14:28.300> okay 00:14:29.290 --> 00:14:29.300 align:start position:0% through all these different Sigma's okay 00:14:29.300 --> 00:14:31.120 align:start position:0% through all these different Sigma's okay and<00:14:29.690> you<00:14:29.990> can<00:14:30.110> do<00:14:30.200> like<00:14:30.350> cool<00:14:30.590> cool<00:14:30.920> cool 00:14:31.120 --> 00:14:31.130 align:start position:0% and you can do like cool cool cool 00:14:31.130 --> 00:14:32.800 align:start position:0% and you can do like cool cool cool composition<00:14:31.640> on<00:14:31.730> contracts<00:14:32.150> too<00:14:32.360> so<00:14:32.720> you<00:14:32.780> can 00:14:32.800 --> 00:14:32.810 align:start position:0% composition on contracts too so you can 00:14:32.810 --> 00:14:34.030 align:start position:0% composition on contracts too so you can say<00:14:32.960> oh<00:14:32.990> well<00:14:33.350> see<00:14:33.470> how<00:14:33.530> can<00:14:33.920> you<00:14:33.980> have 00:14:34.030 --> 00:14:34.040 align:start position:0% say oh well see how can you have 00:14:34.040 --> 00:14:36.490 align:start position:0% say oh well see how can you have contract<00:14:34.460> v1<00:14:34.820> and<00:14:34.970> v2<00:14:35.090> so<00:14:35.750> you<00:14:35.810> can<00:14:36.080> and<00:14:36.350> them 00:14:36.490 --> 00:14:36.500 align:start position:0% contract v1 and v2 so you can and them 00:14:36.500 --> 00:14:38.170 align:start position:0% contract v1 and v2 so you can and them or<00:14:36.710> you<00:14:36.920> can<00:14:36.950> or<00:14:37.310> them<00:14:37.490> so<00:14:37.790> you<00:14:37.850> know<00:14:38.030> it's<00:14:38.120> a 00:14:38.170 --> 00:14:38.180 align:start position:0% or you can or them so you know it's a 00:14:38.180 --> 00:14:39.910 align:start position:0% or you can or them so you know it's a little<00:14:38.240> operations<00:14:39.200> there<00:14:39.380> and<00:14:39.680> they<00:14:39.770> sit 00:14:39.910 --> 00:14:39.920 align:start position:0% little operations there and they sit 00:14:39.920 --> 00:14:42.850 align:start position:0% little operations there and they sit tells<00:14:40.070> you<00:14:40.130> how<00:14:40.250> they<00:14:40.430> go<00:14:40.580> I<00:14:41.480> mean<00:14:42.140> and<00:14:42.560> you<00:14:42.740> can 00:14:42.850 --> 00:14:42.860 align:start position:0% tells you how they go I mean and you can 00:14:42.860 --> 00:14:44.560 align:start position:0% tells you how they go I mean and you can do<00:14:43.010> a<00:14:43.040> more<00:14:43.370> interesting<00:14:43.520> things<00:14:43.880> so<00:14:44.420> you<00:14:44.510> can 00:14:44.560 --> 00:14:44.570 align:start position:0% do a more interesting things so you can 00:14:44.570 --> 00:14:46.660 align:start position:0% do a more interesting things so you can say<00:14:44.840> oh<00:14:45.020> so<00:14:45.260> here's<00:14:45.830> why<00:14:45.980> the<00:14:46.040> coolest<00:14:46.400> one<00:14:46.520> is 00:14:46.660 --> 00:14:46.670 align:start position:0% say oh so here's why the coolest one is 00:14:46.670 --> 00:14:48.340 align:start position:0% say oh so here's why the coolest one is to<00:14:46.790> look<00:14:46.880> at<00:14:47.060> this<00:14:47.210> this<00:14:47.360> is<00:14:47.570> this<00:14:47.930> on<00:14:48.140> this 00:14:48.340 --> 00:14:48.350 align:start position:0% to look at this this is this on this 00:14:48.350 --> 00:14:51.370 align:start position:0% to look at this this is this on this application<00:14:49.010> clause<00:14:49.700> so<00:14:50.390> you<00:14:50.450> have<00:14:50.690> a<00:14:50.720> agent 00:14:51.370 --> 00:14:51.380 align:start position:0% application clause so you have a agent 00:14:51.380 --> 00:14:55.030 align:start position:0% application clause so you have a agent so<00:14:51.650> this<00:14:51.770> is<00:14:51.890> this<00:14:52.070> go<00:14:52.970> back<00:14:53.290> there<00:14:54.290> so<00:14:55.010> you 00:14:55.030 --> 00:14:55.040 align:start position:0% so this is this go back there so you 00:14:55.040 --> 00:14:58.870 align:start position:0% so this is this go back there so you have<00:14:55.280> h<00:14:55.760> an<00:14:55.910> e1<00:14:56.560> executing<00:14:57.560> these<00:14:58.370> these 00:14:58.870 --> 00:14:58.880 align:start position:0% have h an e1 executing these these 00:14:58.880 --> 00:15:01.480 align:start position:0% have h an e1 executing these these actions<00:14:59.360> kay<00:14:59.660> and<00:14:59.930> takes<00:15:00.230> parameters<00:15:00.740> X<00:15:01.250> the 00:15:01.480 --> 00:15:01.490 align:start position:0% actions kay and takes parameters X the 00:15:01.490 --> 00:15:06.340 align:start position:0% actions kay and takes parameters X the little<00:15:01.700> thing<00:15:01.820> over<00:15:01.910> it<00:15:02.060> and<00:15:03.400> and<00:15:04.400> so<00:15:04.820> and<00:15:05.350> it's 00:15:06.340 --> 00:15:06.350 align:start position:0% little thing over it and and so and it's 00:15:06.350 --> 00:15:08.470 align:start position:0% little thing over it and and so and it's do<00:15:06.650> with<00:15:07.070> within<00:15:07.310> some<00:15:07.520> of<00:15:07.610> the<00:15:07.670> window<00:15:07.970> D<00:15:08.240> and 00:15:08.470 --> 00:15:08.480 align:start position:0% do with within some of the window D and 00:15:08.480 --> 00:15:10.870 align:start position:0% do with within some of the window D and if<00:15:09.140> it<00:15:09.590> and<00:15:09.710> if<00:15:09.800> it<00:15:09.890> wins<00:15:10.130> I'm<00:15:10.490> sorry<00:15:10.700> and<00:15:10.820> if 00:15:10.870 --> 00:15:10.880 align:start position:0% if it and if it wins I'm sorry and if 00:15:10.880 --> 00:15:13.990 align:start position:0% if it and if it wins I'm sorry and if it's<00:15:11.000> and<00:15:11.600> if<00:15:11.720> it<00:15:11.900> satisfies<00:15:12.830> all<00:15:13.220> of<00:15:13.460> it<00:15:13.760> then 00:15:13.990 --> 00:15:14.000 align:start position:0% it's and if it satisfies all of it then 00:15:14.000 --> 00:15:16.450 align:start position:0% it's and if it satisfies all of it then it<00:15:14.120> says<00:15:14.300> oh<00:15:14.480> oh<00:15:14.780> there's<00:15:15.020> they're<00:15:15.440> still<00:15:15.710> you 00:15:16.450 --> 00:15:16.460 align:start position:0% it says oh oh there's they're still you 00:15:16.460 --> 00:15:18.880 align:start position:0% it says oh oh there's they're still you get<00:15:16.670> time<00:15:17.150> left<00:15:17.480> z<00:15:17.900> so<00:15:18.170> like<00:15:18.350> so<00:15:18.500> she<00:15:18.560> had<00:15:18.770> like 00:15:18.880 --> 00:15:18.890 align:start position:0% get time left z so like so she had like 00:15:18.890 --> 00:15:20.290 align:start position:0% get time left z so like so she had like five<00:15:19.160> days<00:15:19.430> to<00:15:19.520> do<00:15:19.580> something<00:15:19.910> and<00:15:19.970> you<00:15:20.060> finish 00:15:20.290 --> 00:15:20.300 align:start position:0% five days to do something and you finish 00:15:20.300 --> 00:15:21.190 align:start position:0% five days to do something and you finish it<00:15:20.330> in<00:15:20.420> three<00:15:20.450> days 00:15:21.190 --> 00:15:21.200 align:start position:0% it in three days 00:15:21.200 --> 00:15:25.510 align:start position:0% it in three days z<00:15:21.680> z<00:15:22.130> becomes<00:15:22.840> two<00:15:23.840> and<00:15:24.110> and<00:15:24.950> then<00:15:25.160> it<00:15:25.250> goes<00:15:25.370> on 00:15:25.510 --> 00:15:25.520 align:start position:0% z z becomes two and and then it goes on 00:15:25.520 --> 00:15:26.770 align:start position:0% z z becomes two and and then it goes on to<00:15:25.610> the<00:15:25.640> next<00:15:25.820> contract<00:15:26.150> so<00:15:26.420> you<00:15:26.510> can<00:15:26.630> sort<00:15:26.750> of 00:15:26.770 --> 00:15:26.780 align:start position:0% to the next contract so you can sort of 00:15:26.780 --> 00:15:28.600 align:start position:0% to the next contract so you can sort of chain<00:15:27.110> contracts<00:15:27.800> together<00:15:27.980> and<00:15:28.370> that's 00:15:28.600 --> 00:15:28.610 align:start position:0% chain contracts together and that's 00:15:28.610 --> 00:15:31.210 align:start position:0% chain contracts together and that's gonna<00:15:28.730> in<00:15:29.000> this<00:15:29.330> recursive<00:15:30.140> form<00:15:30.650> and<00:15:30.920> that's 00:15:31.210 --> 00:15:31.220 align:start position:0% gonna in this recursive form and that's 00:15:31.220 --> 00:15:32.620 align:start position:0% gonna in this recursive form and that's like<00:15:31.370> really<00:15:31.400> neat<00:15:31.790> I<00:15:31.910> mean<00:15:32.180> so<00:15:32.300> it's<00:15:32.450> kind<00:15:32.600> of 00:15:32.620 --> 00:15:32.630 align:start position:0% like really neat I mean so it's kind of 00:15:32.630 --> 00:15:34.570 align:start position:0% like really neat I mean so it's kind of this<00:15:32.720> idea<00:15:32.870> oh<00:15:33.320> so<00:15:33.590> so<00:15:33.860> so<00:15:34.130> we're<00:15:34.400> kind<00:15:34.550> of 00:15:34.570 --> 00:15:34.580 align:start position:0% this idea oh so so so we're kind of 00:15:34.580 --> 00:15:36.040 align:start position:0% this idea oh so so so we're kind of doing<00:15:34.670> the<00:15:34.790> beginning<00:15:35.060> here<00:15:35.360> we<00:15:35.510> were<00:15:35.810> doing 00:15:36.040 --> 00:15:36.050 align:start position:0% doing the beginning here we were doing 00:15:36.050 --> 00:15:37.150 align:start position:0% doing the beginning here we were doing sort<00:15:36.230> of<00:15:36.290> like<00:15:36.380> like<00:15:36.650> what<00:15:36.800> are<00:15:36.890> the<00:15:36.980> what<00:15:37.130> are 00:15:37.150 --> 00:15:37.160 align:start position:0% sort of like like what are the what are 00:15:37.160 --> 00:15:40.000 align:start position:0% sort of like like what are the what are the<00:15:37.250> atoms<00:15:37.670> of<00:15:38.050> of<00:15:39.050> contracts<00:15:39.560> so<00:15:39.680> I<00:15:39.740> was<00:15:39.890> like 00:15:40.000 --> 00:15:40.010 align:start position:0% the atoms of of contracts so I was like 00:15:40.010 --> 00:15:41.710 align:start position:0% the atoms of of contracts so I was like the<00:15:40.070> periodic<00:15:40.400> table<00:15:40.730> and<00:15:40.850> these<00:15:41.420> give<00:15:41.630> you 00:15:41.710 --> 00:15:41.720 align:start position:0% the periodic table and these give you 00:15:41.720 --> 00:15:42.910 align:start position:0% the periodic table and these give you all<00:15:41.840> different<00:15:41.960> ways<00:15:42.230> that<00:15:42.380> you<00:15:42.500> can<00:15:42.620> chain 00:15:42.910 --> 00:15:42.920 align:start position:0% all different ways that you can chain 00:15:42.920 --> 00:15:44.290 align:start position:0% all different ways that you can chain them<00:15:43.070> together<00:15:43.250> into<00:15:43.670> a<00:15:43.700> chemistry<00:15:44.060> of 00:15:44.290 --> 00:15:44.300 align:start position:0% them together into a chemistry of 00:15:44.300 --> 00:15:46.600 align:start position:0% them together into a chemistry of contracts<00:15:44.750> and<00:15:44.990> make<00:15:45.320> cool<00:15:45.740> molecules<00:15:46.280> out<00:15:46.490> of 00:15:46.600 --> 00:15:46.610 align:start position:0% contracts and make cool molecules out of 00:15:46.610 --> 00:15:47.850 align:start position:0% contracts and make cool molecules out of them<00:15:46.700> and<00:15:46.790> you<00:15:46.880> can<00:15:47.000> make<00:15:47.090> like<00:15:47.210> crazy 00:15:47.850 --> 00:15:47.860 align:start position:0% them and you can make like crazy 00:15:47.860 --> 00:15:51.630 align:start position:0% them and you can make like crazy yeah<00:15:48.890> so<00:15:49.160> this<00:15:49.370> says<00:15:49.580> this<00:15:49.760> is<00:15:49.910> really<00:15:50.540> fertile 00:15:51.630 --> 00:15:51.640 align:start position:0% yeah so this says this is really fertile 00:15:51.640 --> 00:15:54.280 align:start position:0% yeah so this says this is really fertile okay<00:15:52.640> yeah<00:15:53.060> so<00:15:53.210> here's<00:15:53.450> an<00:15:53.600> example<00:15:53.690> one<00:15:54.110> right 00:15:54.280 --> 00:15:54.290 align:start position:0% okay yeah so here's an example one right 00:15:54.290 --> 00:15:57.160 align:start position:0% okay yeah so here's an example one right here<00:15:54.560> so<00:15:54.710> this<00:15:55.160> is<00:15:55.220> an<00:15:55.400> NDA<00:15:55.730> contract<00:15:56.420> so<00:15:56.870> this 00:15:57.160 --> 00:15:57.170 align:start position:0% here so this is an NDA contract so this 00:15:57.170 --> 00:15:59.830 align:start position:0% here so this is an NDA contract so this ppreciate<00:15:57.470> board<00:15:57.680> so<00:15:58.460> you<00:15:58.520> see<00:15:59.270> yep<00:15:59.390> see<00:15:59.570> it<00:15:59.750> so 00:15:59.830 --> 00:15:59.840 align:start position:0% ppreciate board so you see yep see it so 00:15:59.840 --> 00:16:01.480 align:start position:0% ppreciate board so you see yep see it so it<00:15:59.900> takes<00:16:00.110> one<00:16:00.320> argument<00:16:00.350> the<00:16:00.830> employee<00:16:01.130> and 00:16:01.480 --> 00:16:01.490 align:start position:0% it takes one argument the employee and 00:16:01.490 --> 00:16:04.630 align:start position:0% it takes one argument the employee and it<00:16:01.760> says<00:16:02.000> oh<00:16:02.180> if<00:16:02.510> you<00:16:02.690> ever<00:16:02.900> get<00:16:03.200> if<00:16:04.010> you<00:16:04.220> if<00:16:04.430> you 00:16:04.630 --> 00:16:04.640 align:start position:0% it says oh if you ever get if you if you 00:16:04.640 --> 00:16:07.200 align:start position:0% it says oh if you ever get if you if you if<00:16:04.850> you<00:16:05.120> ever<00:16:05.300> get<00:16:06.050> a<00:16:06.140> disclosure<00:16:06.560> reported 00:16:07.200 --> 00:16:07.210 align:start position:0% if you ever get a disclosure reported 00:16:07.210 --> 00:16:10.510 align:start position:0% if you ever get a disclosure reported when<00:16:08.210> it<00:16:08.300> takes<00:16:08.480> takes<00:16:08.930> an<00:16:09.080> E<00:16:09.230> and<00:16:09.470> if<00:16:09.710> E<00:16:09.950> is<00:16:10.250> the 00:16:10.510 --> 00:16:10.520 align:start position:0% when it takes takes an E and if E is the 00:16:10.520 --> 00:16:12.700 align:start position:0% when it takes takes an E and if E is the employee<00:16:10.840> and<00:16:11.840> it's<00:16:12.050> happened<00:16:12.410> within<00:16:12.560> the 00:16:12.700 --> 00:16:12.710 align:start position:0% employee and it's happened within the 00:16:12.710 --> 00:16:15.880 align:start position:0% employee and it's happened within the past<00:16:12.740> five<00:16:13.190> years<00:16:13.220> then<00:16:14.060> breach<00:16:14.660> and<00:16:14.990> and 00:16:15.880 --> 00:16:15.890 align:start position:0% past five years then breach and and 00:16:15.890 --> 00:16:18.340 align:start position:0% past five years then breach and and that's<00:16:16.130> and<00:16:16.520> and<00:16:16.820> that<00:16:16.940> employee<00:16:17.180> is<00:16:17.510> is<00:16:17.750> at 00:16:18.340 --> 00:16:18.350 align:start position:0% that's and and that employee is is at 00:16:18.350 --> 00:16:20.980 align:start position:0% that's and and that employee is is at fault<00:16:18.590> and<00:16:18.830> the<00:16:19.250> little<00:16:19.490> little<00:16:20.330> VIN<00:16:20.630> employee 00:16:20.980 --> 00:16:20.990 align:start position:0% fault and the little little VIN employee 00:16:20.990 --> 00:16:23.830 align:start position:0% fault and the little little VIN employee says<00:16:21.260> the<00:16:21.440> employee<00:16:21.830> at<00:16:22.040> blame<00:16:22.460> and<00:16:22.850> it<00:16:23.660> says 00:16:23.830 --> 00:16:23.840 align:start position:0% says the employee at blame and it says 00:16:23.840 --> 00:16:25.690 align:start position:0% says the employee at blame and it says Ellen<00:16:24.170> by<00:16:24.290> the<00:16:24.350> way<00:16:24.500> and<00:16:24.740> it<00:16:24.830> starts<00:16:24.860> now<00:16:25.160> and 00:16:25.690 --> 00:16:25.700 align:start position:0% Ellen by the way and it starts now and 00:16:25.700 --> 00:16:28.120 align:start position:0% Ellen by the way and it starts now and sort<00:16:26.630> of<00:16:26.690> in<00:16:26.840> this<00:16:26.960> little<00:16:27.020> simple<00:16:27.470> code<00:16:27.680> you 00:16:28.120 --> 00:16:28.130 align:start position:0% sort of in this little simple code you 00:16:28.130 --> 00:16:29.910 align:start position:0% sort of in this little simple code you can<00:16:28.280> compile<00:16:28.610> this<00:16:28.820> to<00:16:28.970> English<00:16:29.300> in<00:16:29.480> ER 00:16:29.910 --> 00:16:29.920 align:start position:0% can compile this to English in ER 00:16:29.920 --> 00:16:31.560 align:start position:0% can compile this to English in ER jurisdiction<00:16:30.579> you<00:16:30.790> could<00:16:30.940> do<00:16:31.029> it<00:16:31.149> instead<00:16:31.420> you 00:16:31.560 --> 00:16:31.570 align:start position:0% jurisdiction you could do it instead you 00:16:31.570 --> 00:16:33.960 align:start position:0% jurisdiction you could do it instead you know<00:16:31.690> of<00:16:31.959> you<00:16:32.800> know<00:16:32.829> English<00:16:33.279> French<00:16:33.550> Mandarin 00:16:33.960 --> 00:16:33.970 align:start position:0% know of you know English French Mandarin 00:16:33.970 --> 00:16:35.040 align:start position:0% know of you know English French Mandarin whatever<00:16:34.269> or<00:16:34.570> aetherium 00:16:35.040 --> 00:16:35.050 align:start position:0% whatever or aetherium 00:16:35.050 --> 00:16:38.970 align:start position:0% whatever or aetherium and<00:16:35.560> I<00:16:36.040> and<00:16:36.399> it<00:16:36.550> would<00:16:36.670> all<00:16:36.790> just<00:16:37.269> work<00:16:37.980> okay 00:16:38.970 --> 00:16:38.980 align:start position:0% and I and it would all just work okay 00:16:38.980 --> 00:16:40.170 align:start position:0% and I and it would all just work okay cool 00:16:40.170 --> 00:16:40.180 align:start position:0% cool 00:16:40.180 --> 00:16:43.410 align:start position:0% cool so<00:16:40.690> this<00:16:41.649> is<00:16:41.740> a<00:16:41.800> saline<00:16:42.070> here<00:16:42.339> for<00:16:42.610> the<00:16:42.880> for<00:16:43.269> the 00:16:43.410 --> 00:16:43.420 align:start position:0% so this is a saline here for the for the 00:16:43.420 --> 00:16:44.759 align:start position:0% so this is a saline here for the for the languages<00:16:43.839> and<00:16:43.990> math<00:16:44.079> people<00:16:44.380> who<00:16:44.529> want<00:16:44.709> to 00:16:44.759 --> 00:16:44.769 align:start position:0% languages and math people who want to 00:16:44.769 --> 00:16:47.340 align:start position:0% languages and math people who want to know<00:16:44.860> how<00:16:44.920> you<00:16:45.160> actually<00:16:45.430> implement<00:16:46.350> these 00:16:47.340 --> 00:16:47.350 align:start position:0% know how you actually implement these 00:16:47.350 --> 00:16:53.129 align:start position:0% know how you actually implement these ideas<00:16:47.940> that's<00:16:48.940> it<00:16:49.149> this<00:16:49.480> is<00:16:49.540> for<00:16:49.930> you<00:16:50.110> and<00:16:52.139> so 00:16:53.129 --> 00:16:53.139 align:start position:0% ideas that's it this is for you and so 00:16:53.139 --> 00:16:54.660 align:start position:0% ideas that's it this is for you and so this<00:16:53.680> so<00:16:53.889> there<00:16:54.160> there<00:16:54.370> are<00:16:54.399> some 00:16:54.660 --> 00:16:54.670 align:start position:0% this so there there are some 00:16:54.670 --> 00:16:55.949 align:start position:0% this so there there are some complications<00:16:55.120> in<00:16:55.389> the<00:16:55.480> way<00:16:55.570> that<00:16:55.750> you<00:16:55.810> can 00:16:55.949 --> 00:16:55.959 align:start position:0% complications in the way that you can 00:16:55.959 --> 00:16:57.780 align:start position:0% complications in the way that you can merge<00:16:56.110> contracts<00:16:56.680> there<00:16:56.949> are<00:16:57.040> there<00:16:57.190> are<00:16:57.220> some 00:16:57.780 --> 00:16:57.790 align:start position:0% merge contracts there are there are some 00:16:57.790 --> 00:17:00.960 align:start position:0% merge contracts there are there are some restrictions<00:16:58.089> so<00:16:58.930> for<00:16:59.230> example<00:16:59.649> so<00:17:00.610> if<00:17:00.820> you 00:17:00.960 --> 00:17:00.970 align:start position:0% restrictions so for example so if you 00:17:00.970 --> 00:17:03.240 align:start position:0% restrictions so for example so if you have<00:17:01.300> so<00:17:02.170> yet<00:17:02.290> so<00:17:02.529> you<00:17:02.589> so<00:17:02.920> you<00:17:02.980> have<00:17:03.220> a 00:17:03.240 --> 00:17:03.250 align:start position:0% have so yet so you so you have a 00:17:03.250 --> 00:17:04.829 align:start position:0% have so yet so you so you have a different<00:17:03.790> contract<00:17:04.120> with<00:17:04.270> it<00:17:04.390> but<00:17:04.510> the 00:17:04.829 --> 00:17:04.839 align:start position:0% different contract with it but the 00:17:04.839 --> 00:17:06.480 align:start position:0% different contract with it but the people<00:17:05.049> who<00:17:05.140> they<00:17:05.260> blame<00:17:05.589> aren't<00:17:06.040> always<00:17:06.189> the 00:17:06.480 --> 00:17:06.490 align:start position:0% people who they blame aren't always the 00:17:06.490 --> 00:17:09.090 align:start position:0% people who they blame aren't always the same<00:17:06.730> you<00:17:07.600> you<00:17:07.900> you<00:17:08.079> you<00:17:08.319> can't<00:17:08.559> combine<00:17:08.740> them 00:17:09.090 --> 00:17:09.100 align:start position:0% same you you you you can't combine them 00:17:09.100 --> 00:17:10.439 align:start position:0% same you you you you can't combine them and<00:17:09.280> that's<00:17:09.610> kind<00:17:09.760> of<00:17:09.790> a<00:17:09.880> limitation<00:17:10.179> and 00:17:10.439 --> 00:17:10.449 align:start position:0% and that's kind of a limitation and 00:17:10.449 --> 00:17:12.059 align:start position:0% and that's kind of a limitation and that's<00:17:10.569> annoying<00:17:10.839> and<00:17:11.169> we<00:17:11.230> should<00:17:11.350> pay<00:17:11.530> a<00:17:11.559> PhD 00:17:12.059 --> 00:17:12.069 align:start position:0% that's annoying and we should pay a PhD 00:17:12.069 --> 00:17:15.630 align:start position:0% that's annoying and we should pay a PhD to<00:17:12.100> figure<00:17:12.189> that<00:17:12.459> out<00:17:13.169> okay<00:17:14.169> so<00:17:14.860> this<00:17:15.400> is<00:17:15.549> where 00:17:15.630 --> 00:17:15.640 align:start position:0% to figure that out okay so this is where 00:17:15.640 --> 00:17:17.250 align:start position:0% to figure that out okay so this is where the<00:17:15.790> next<00:17:15.939> one<00:17:16.059> this<00:17:16.240> is<00:17:16.299> how<00:17:16.569> this<00:17:16.780> connects 00:17:17.250 --> 00:17:17.260 align:start position:0% the next one this is how this connects 00:17:17.260 --> 00:17:19.350 align:start position:0% the next one this is how this connects to<00:17:17.470> the<00:17:17.790> upcoming<00:17:18.790> literature<00:17:19.150> which<00:17:19.270> you'll 00:17:19.350 --> 00:17:19.360 align:start position:0% to the upcoming literature which you'll 00:17:19.360 --> 00:17:20.579 align:start position:0% to the upcoming literature which you'll probably<00:17:19.390> hear<00:17:19.689> about<00:17:19.809> probably<00:17:20.079> tomorrow<00:17:20.230> on 00:17:20.579 --> 00:17:20.589 align:start position:0% probably hear about probably tomorrow on 00:17:20.589 --> 00:17:25.439 align:start position:0% probably hear about probably tomorrow on a<00:17:20.650> specifically<00:17:21.579> etherium<00:17:23.640> how<00:17:24.640> much<00:17:24.790> time<00:17:25.150> do 00:17:25.439 --> 00:17:25.449 align:start position:0% a specifically etherium how much time do 00:17:25.449 --> 00:17:26.909 align:start position:0% a specifically etherium how much time do we<00:17:25.569> have<00:17:25.600> because<00:17:26.110> the<00:17:26.199> things<00:17:26.410> is<00:17:26.589> like<00:17:26.740> 30 00:17:26.909 --> 00:17:26.919 align:start position:0% we have because the things is like 30 00:17:26.919 --> 00:17:29.970 align:start position:0% we have because the things is like 30 seconds<00:17:27.690> I'm<00:17:28.690> just<00:17:29.320> gonna<00:17:29.440> skip<00:17:29.679> to<00:17:29.860> the<00:17:29.950> next 00:17:29.970 --> 00:17:29.980 align:start position:0% seconds I'm just gonna skip to the next 00:17:29.980 --> 00:17:34.650 align:start position:0% seconds I'm just gonna skip to the next slide<00:17:30.340> and<00:17:31.980> deccan<00:17:32.980> beddings<00:17:33.309> are<00:17:33.460> cool<00:17:33.660> and 00:17:34.650 --> 00:17:34.660 align:start position:0% slide and deccan beddings are cool and 00:17:34.660 --> 00:17:39.480 align:start position:0% slide and deccan beddings are cool and we<00:17:35.530> can<00:17:37.080> we<00:17:38.080> have<00:17:38.110> a<00:17:38.260> very<00:17:38.530> well<00:17:38.710> defined<00:17:38.770> idea 00:17:39.480 --> 00:17:39.490 align:start position:0% we can we have a very well defined idea 00:17:39.490 --> 00:17:42.570 align:start position:0% we can we have a very well defined idea in<00:17:39.820> terms<00:17:40.390> of<00:17:40.750> the<00:17:41.320> space<00:17:41.590> of<00:17:41.890> variation<00:17:42.429> in 00:17:42.570 --> 00:17:42.580 align:start position:0% in terms of the space of variation in 00:17:42.580 --> 00:17:45.140 align:start position:0% in terms of the space of variation in the<00:17:42.669> contracts<00:17:43.090> you<00:17:43.179> can<00:17:43.299> express<00:17:43.980> what 00:17:45.140 --> 00:17:45.150 align:start position:0% the contracts you can express what 00:17:45.150 --> 00:17:50.190 align:start position:0% the contracts you can express what indicates<00:17:47.160> good<00:17:48.160> behavior<00:17:48.700> and<00:17:49.000> the<00:17:49.809> rest<00:17:49.990> is 00:17:50.190 --> 00:17:50.200 align:start position:0% indicates good behavior and the rest is 00:17:50.200 --> 00:17:54.240 align:start position:0% indicates good behavior and the rest is basically<00:17:51.600> relates<00:17:52.600> to<00:17:52.900> the<00:17:53.230> compiler<00:17:53.950> and 00:17:54.240 --> 00:17:54.250 align:start position:0% basically relates to the compiler and 00:17:54.250 --> 00:17:57.120 align:start position:0% basically relates to the compiler and you<00:17:54.669> want<00:17:54.880> to<00:17:55.120> be<00:17:55.299> able<00:17:55.419> to<00:17:55.770> say<00:17:56.770> that 00:17:57.120 --> 00:17:57.130 align:start position:0% you want to be able to say that 00:17:57.130 --> 00:17:59.370 align:start position:0% you want to be able to say that normalization<00:17:57.820> with<00:17:58.150> respect<00:17:58.570> to<00:17:58.870> a<00:17:58.900> logic 00:17:59.370 --> 00:17:59.380 align:start position:0% normalization with respect to a logic 00:17:59.380 --> 00:18:01.289 align:start position:0% normalization with respect to a logic behaves<00:18:00.070> equivalently<00:18:00.610> in<00:18:00.910> your<00:18:01.059> source 00:18:01.289 --> 00:18:01.299 align:start position:0% behaves equivalently in your source 00:18:01.299 --> 00:18:05.850 align:start position:0% behaves equivalently in your source logic<00:18:01.750> and<00:18:01.960> in<00:18:02.590> your<00:18:02.980> compiled<00:18:03.370> output<00:18:03.640> and<00:18:04.860> we 00:18:05.850 --> 00:18:05.860 align:start position:0% logic and in your compiled output and we 00:18:05.860 --> 00:18:10.740 align:start position:0% logic and in your compiled output and we can<00:18:06.100> do<00:18:06.760> that<00:18:06.940> and<00:18:07.809> stuff<00:18:08.940> alright<00:18:09.940> next<00:18:10.240> last 00:18:10.740 --> 00:18:10.750 align:start position:0% can do that and stuff alright next last 00:18:10.750 --> 00:18:14.880 align:start position:0% can do that and stuff alright next last one<00:18:10.960> you<00:18:11.080> have<00:18:11.169> to<00:18:11.230> hit<00:18:11.350> it<00:18:13.350> all<00:18:14.350> right<00:18:14.470> so<00:18:14.799> this 00:18:14.880 --> 00:18:14.890 align:start position:0% one you have to hit it all right so this 00:18:14.890 --> 00:18:15.450 align:start position:0% one you have to hit it all right so this is<00:18:15.010> the<00:18:15.100> end 00:18:15.450 --> 00:18:15.460 align:start position:0% is the end 00:18:15.460 --> 00:18:19.169 align:start position:0% is the end oh<00:18:15.490> no<00:18:16.390> next<00:18:16.900> the<00:18:17.740> other<00:18:17.860> button<00:18:18.160> there<00:18:18.820> you<00:18:18.880> go 00:18:19.169 --> 00:18:19.179 align:start position:0% oh no next the other button there you go 00:18:19.179 --> 00:18:21.780 align:start position:0% oh no next the other button there you go um<00:18:19.570> so<00:18:19.809> okay<00:18:19.840> so<00:18:20.169> this<00:18:20.440> may<00:18:20.559> see<00:18:20.620> our<00:18:20.799> thing<00:18:21.010> so 00:18:21.780 --> 00:18:21.790 align:start position:0% um so okay so this may see our thing so 00:18:21.790 --> 00:18:23.700 align:start position:0% um so okay so this may see our thing so basically<00:18:22.120> where<00:18:22.450> we're<00:18:22.660> here<00:18:22.990> so<00:18:23.260> we<00:18:23.530> are 00:18:23.700 --> 00:18:23.710 align:start position:0% basically where we're here so we are 00:18:23.710 --> 00:18:25.470 align:start position:0% basically where we're here so we are busy<00:18:23.950> formalizing<00:18:24.640> contracts<00:18:25.150> sort<00:18:25.330> of<00:18:25.390> in 00:18:25.470 --> 00:18:25.480 align:start position:0% busy formalizing contracts sort of in 00:18:25.480 --> 00:18:28.110 align:start position:0% busy formalizing contracts sort of in the<00:18:25.570> broad<00:18:25.809> sense<00:18:26.080> we<00:18:26.799> expect<00:18:27.130> the<00:18:27.220> authority 00:18:28.110 --> 00:18:28.120 align:start position:0% the broad sense we expect the authority 00:18:28.120 --> 00:18:30.270 align:start position:0% the broad sense we expect the authority to<00:18:28.240> be<00:18:28.330> our<00:18:28.450> power<00:18:28.690> users<00:18:28.960> so<00:18:29.590> if<00:18:29.950> you<00:18:30.100> want 00:18:30.270 --> 00:18:30.280 align:start position:0% to be our power users so if you want 00:18:30.280 --> 00:18:31.860 align:start position:0% to be our power users so if you want features<00:18:30.610> you<00:18:30.940> should<00:18:30.970> let<00:18:31.270> us<00:18:31.360> know<00:18:31.540> because 00:18:31.860 --> 00:18:31.870 align:start position:0% features you should let us know because 00:18:31.870 --> 00:18:34.139 align:start position:0% features you should let us know because we're<00:18:32.169> designing<00:18:32.500> this<00:18:32.740> and 00:18:34.139 --> 00:18:34.149 align:start position:0% we're designing this and 00:18:34.149 --> 00:18:35.779 align:start position:0% we're designing this and yeah<00:18:34.299> and<00:18:34.479> we'll<00:18:34.599> do<00:18:34.719> like<00:18:34.809> free<00:18:35.049> work<00:18:35.229> for<00:18:35.379> you 00:18:35.779 --> 00:18:35.789 align:start position:0% yeah and we'll do like free work for you 00:18:35.789 --> 00:18:37.949 align:start position:0% yeah and we'll do like free work for you and<00:18:36.789> if<00:18:37.149> you're<00:18:37.269> in<00:18:37.359> this<00:18:37.479> kind<00:18:37.629> of<00:18:37.659> thing<00:18:37.779> come 00:18:37.949 --> 00:18:37.959 align:start position:0% and if you're in this kind of thing come 00:18:37.959 --> 00:18:39.599 align:start position:0% and if you're in this kind of thing come hang<00:18:38.109> out<00:18:38.169> with<00:18:38.289> us<00:18:38.349> and<00:18:38.649> if<00:18:39.279> you<00:18:39.369> want<00:18:39.489> to 00:18:39.599 --> 00:18:39.609 align:start position:0% hang out with us and if you want to 00:18:39.609 --> 00:18:41.069 align:start position:0% hang out with us and if you want to follow<00:18:39.819> us<00:18:39.969> there's<00:18:40.209> our<00:18:40.419> mailing<00:18:40.689> list<00:18:40.719> and 00:18:41.069 --> 00:18:41.079 align:start position:0% follow us there's our mailing list and 00:18:41.079 --> 00:18:43.499 align:start position:0% follow us there's our mailing list and there's<00:18:41.319> our<00:18:41.379> email<00:18:41.679> address<00:18:41.999> yep<00:18:43.029> come<00:18:43.329> talks 00:18:43.499 --> 00:18:43.509 align:start position:0% there's our email address yep come talks 00:18:43.509 --> 00:18:46.349 align:start position:0% there's our email address yep come talks about<00:18:43.659> languages<00:18:44.019> sometime