WEBVTT Kind: captions Language: en 00:00:17.550 --> 00:00:22.500 align:start position:0% so<00:00:18.720> first<00:00:19.720> of<00:00:19.900> all<00:00:20.280> thanks<00:00:21.280> to<00:00:21.330> italic<00:00:22.330> and 00:00:22.500 --> 00:00:22.510 align:start position:0% so first of all thanks to italic and 00:00:22.510 --> 00:00:25.890 align:start position:0% so first of all thanks to italic and glad<00:00:22.840> for<00:00:23.200> asking<00:00:23.890> me<00:00:23.980> to<00:00:24.010> come<00:00:24.130> and<00:00:24.670> it's<00:00:25.540> it's 00:00:25.890 --> 00:00:25.900 align:start position:0% glad for asking me to come and it's it's 00:00:25.900 --> 00:00:28.290 align:start position:0% glad for asking me to come and it's it's great<00:00:26.050> to<00:00:26.230> be<00:00:26.350> here<00:00:26.560> I'm<00:00:26.740> glad<00:00:27.220> glad<00:00:27.910> to<00:00:28.180> be 00:00:28.290 --> 00:00:28.300 align:start position:0% great to be here I'm glad glad to be 00:00:28.300 --> 00:00:30.570 align:start position:0% great to be here I'm glad glad to be able<00:00:28.390> to<00:00:28.630> deliver<00:00:29.500> a<00:00:29.560> few<00:00:29.860> impressions<00:00:30.460> I 00:00:30.570 --> 00:00:30.580 align:start position:0% able to deliver a few impressions I 00:00:30.580 --> 00:00:32.100 align:start position:0% able to deliver a few impressions I think<00:00:30.790> in<00:00:30.880> in<00:00:31.090> twenty<00:00:31.420> five<00:00:31.570> minutes<00:00:31.930> that's 00:00:32.100 --> 00:00:32.110 align:start position:0% think in in twenty five minutes that's 00:00:32.110 --> 00:00:34.230 align:start position:0% think in in twenty five minutes that's all<00:00:32.230> I<00:00:32.290> can<00:00:32.439> do<00:00:32.680> is<00:00:32.830> is<00:00:33.100> deliver<00:00:33.880> a<00:00:33.970> few 00:00:34.230 --> 00:00:34.240 align:start position:0% all I can do is is deliver a few 00:00:34.240 --> 00:00:36.390 align:start position:0% all I can do is is deliver a few impressions<00:00:34.840> of<00:00:35.080> ladin<00:00:35.800> I've<00:00:35.890> been<00:00:36.010> working<00:00:36.370> a 00:00:36.390 --> 00:00:36.400 align:start position:0% impressions of ladin I've been working a 00:00:36.400 --> 00:00:40.980 align:start position:0% impressions of ladin I've been working a lot<00:00:36.910> on<00:00:36.970> Casper<00:00:37.630> and<00:00:38.880> and<00:00:39.880> kind<00:00:40.540> of<00:00:40.630> the 00:00:40.980 --> 00:00:40.990 align:start position:0% lot on Casper and and kind of the 00:00:40.990 --> 00:00:44.130 align:start position:0% lot on Casper and and kind of the technologies<00:00:41.860> and<00:00:42.370> tools<00:00:42.670> and<00:00:43.150> ideas<00:00:43.660> that 00:00:44.130 --> 00:00:44.140 align:start position:0% technologies and tools and ideas that 00:00:44.140 --> 00:00:45.630 align:start position:0% technologies and tools and ideas that I'm<00:00:44.260> bringing<00:00:44.470> to<00:00:44.620> the<00:00:44.829> formal<00:00:45.460> verification 00:00:45.630 --> 00:00:45.640 align:start position:0% I'm bringing to the formal verification 00:00:45.640 --> 00:00:49.410 align:start position:0% I'm bringing to the formal verification of<00:00:46.090> Casper<00:00:46.630> are<00:00:47.230> also<00:00:47.940> embodied<00:00:48.940> and<00:00:49.120> in<00:00:49.210> some 00:00:49.410 --> 00:00:49.420 align:start position:0% of Casper are also embodied and in some 00:00:49.420 --> 00:00:50.970 align:start position:0% of Casper are also embodied and in some of<00:00:49.480> the<00:00:49.570> ideas<00:00:50.500> that<00:00:50.530> I'll<00:00:50.740> be<00:00:50.829> presenting 00:00:50.970 --> 00:00:50.980 align:start position:0% of the ideas that I'll be presenting 00:00:50.980 --> 00:00:55.979 align:start position:0% of the ideas that I'll be presenting here<00:00:51.660> so<00:00:52.770> kind<00:00:53.770> of<00:00:53.800> the<00:00:54.210> you<00:00:55.210> know<00:00:55.329> just<00:00:55.840> want 00:00:55.979 --> 00:00:55.989 align:start position:0% here so kind of the you know just want 00:00:55.989 --> 00:00:58.410 align:start position:0% here so kind of the you know just want to<00:00:56.110> touch<00:00:56.470> on<00:00:56.710> the<00:00:56.829> an<00:00:57.280> overall<00:00:57.700> narrative<00:00:57.940> and 00:00:58.410 --> 00:00:58.420 align:start position:0% to touch on the an overall narrative and 00:00:58.420 --> 00:01:01.229 align:start position:0% to touch on the an overall narrative and then<00:00:58.690> and<00:00:58.960> really<00:00:59.590> if<00:01:00.100> you<00:01:00.399> if<00:01:00.670> you<00:01:00.820> walk<00:01:01.060> away 00:01:01.229 --> 00:01:01.239 align:start position:0% then and really if you if you walk away 00:01:01.239 --> 00:01:02.460 align:start position:0% then and really if you if you walk away with<00:01:01.450> nothing<00:01:01.720> else<00:01:01.810> I<00:01:01.989> want<00:01:02.140> to<00:01:02.200> leave<00:01:02.350> you 00:01:02.460 --> 00:01:02.470 align:start position:0% with nothing else I want to leave you 00:01:02.470 --> 00:01:05.490 align:start position:0% with nothing else I want to leave you with<00:01:02.590> this<00:01:02.710> one<00:01:02.980> big<00:01:03.250> picture<00:01:03.520> idea<00:01:04.170> but<00:01:05.170> but 00:01:05.490 --> 00:01:05.500 align:start position:0% with this one big picture idea but but 00:01:05.500 --> 00:01:08.250 align:start position:0% with this one big picture idea but but you<00:01:05.710> know<00:01:05.970> in<00:01:06.970> the<00:01:07.120> details<00:01:07.570> there's<00:01:08.020> enough 00:01:08.250 --> 00:01:08.260 align:start position:0% you know in the details there's enough 00:01:08.260 --> 00:01:10.320 align:start position:0% you know in the details there's enough space<00:01:08.440> for<00:01:08.830> God<00:01:08.979> and<00:01:09.220> the<00:01:09.310> devil<00:01:09.729> right<00:01:09.970> so 00:01:10.320 --> 00:01:10.330 align:start position:0% space for God and the devil right so 00:01:10.330 --> 00:01:12.210 align:start position:0% space for God and the devil right so there's<00:01:10.900> always<00:01:11.110> lots<00:01:11.500> and<00:01:11.800> lots<00:01:11.950> of<00:01:12.100> space 00:01:12.210 --> 00:01:12.220 align:start position:0% there's always lots and lots of space 00:01:12.220 --> 00:01:14.670 align:start position:0% there's always lots and lots of space and<00:01:12.400> in<00:01:12.790> the<00:01:12.880> details<00:01:13.270> and<00:01:13.540> and<00:01:14.229> maybe<00:01:14.409> talk 00:01:14.670 --> 00:01:14.680 align:start position:0% and in the details and and maybe talk 00:01:14.680 --> 00:01:16.620 align:start position:0% and in the details and and maybe talk about<00:01:14.710> some<00:01:15.100> next<00:01:15.340> steps<00:01:15.400> so<00:01:16.120> that's<00:01:16.390> kind<00:01:16.600> of 00:01:16.620 --> 00:01:16.630 align:start position:0% about some next steps so that's kind of 00:01:16.630 --> 00:01:18.840 align:start position:0% about some next steps so that's kind of what<00:01:16.750> we're<00:01:16.870> going<00:01:16.990> to<00:01:17.020> do<00:01:17.250> and<00:01:18.250> the<00:01:18.460> narrative 00:01:18.840 --> 00:01:18.850 align:start position:0% what we're going to do and the narrative 00:01:18.850 --> 00:01:20.370 align:start position:0% what we're going to do and the narrative is<00:01:18.909> actually<00:01:19.240> a<00:01:19.270> fairly<00:01:19.600> simple<00:01:19.750> one<00:01:20.200> it's 00:01:20.370 --> 00:01:20.380 align:start position:0% is actually a fairly simple one it's 00:01:20.380 --> 00:01:22.830 align:start position:0% is actually a fairly simple one it's fairly<00:01:20.530> straightforward<00:01:21.630> consensus<00:01:22.630> is<00:01:22.810> a 00:01:22.830 --> 00:01:22.840 align:start position:0% fairly straightforward consensus is a 00:01:22.840 --> 00:01:24.600 align:start position:0% fairly straightforward consensus is a necessary<00:01:23.409> component<00:01:23.680> of<00:01:24.040> the<00:01:24.130> blockchain 00:01:24.600 --> 00:01:24.610 align:start position:0% necessary component of the blockchain 00:01:24.610 --> 00:01:27.510 align:start position:0% necessary component of the blockchain so<00:01:24.760> you<00:01:24.880> heard<00:01:25.030> Vlad<00:01:25.390> talk<00:01:25.720> rather<00:01:26.590> eloquently 00:01:27.510 --> 00:01:27.520 align:start position:0% so you heard Vlad talk rather eloquently 00:01:27.520 --> 00:01:29.370 align:start position:0% so you heard Vlad talk rather eloquently about<00:01:27.850> consensus<00:01:28.450> and<00:01:28.659> some<00:01:28.810> of<00:01:28.900> the<00:01:28.960> problems 00:01:29.370 --> 00:01:29.380 align:start position:0% about consensus and some of the problems 00:01:29.380 --> 00:01:33.330 align:start position:0% about consensus and some of the problems there<00:01:30.600> it<00:01:31.600> turns<00:01:32.200> out<00:01:32.409> I<00:01:32.590> mean<00:01:32.770> I<00:01:32.860> think<00:01:32.920> I 00:01:33.330 --> 00:01:33.340 align:start position:0% there it turns out I mean I think I 00:01:33.340 --> 00:01:35.370 align:start position:0% there it turns out I mean I think I think<00:01:33.520> many<00:01:33.880> of<00:01:34.030> the<00:01:34.090> people<00:01:34.240> here<00:01:34.840> know<00:01:35.080> that 00:01:35.370 --> 00:01:35.380 align:start position:0% think many of the people here know that 00:01:35.380 --> 00:01:38.399 align:start position:0% think many of the people here know that that<00:01:35.950> blockchain<00:01:36.490> currently<00:01:37.360> you<00:01:37.840> know<00:01:37.869> as 00:01:38.399 --> 00:01:38.409 align:start position:0% that blockchain currently you know as 00:01:38.409 --> 00:01:42.630 align:start position:0% that blockchain currently you know as embodied<00:01:39.960> doesn't<00:01:40.960> doesn't<00:01:41.830> scale<00:01:42.130> very<00:01:42.159> well 00:01:42.630 --> 00:01:42.640 align:start position:0% embodied doesn't doesn't scale very well 00:01:42.640 --> 00:01:45.090 align:start position:0% embodied doesn't doesn't scale very well and<00:01:42.960> Casper's<00:01:43.960> variation<00:01:44.590> the<00:01:44.770> proof<00:01:44.950> of 00:01:45.090 --> 00:01:45.100 align:start position:0% and Casper's variation the proof of 00:01:45.100 --> 00:01:47.070 align:start position:0% and Casper's variation the proof of stake<00:01:45.310> is<00:01:45.460> an<00:01:45.580> important<00:01:46.030> step<00:01:46.330> along<00:01:46.780> the<00:01:47.049> way 00:01:47.070 --> 00:01:47.080 align:start position:0% stake is an important step along the way 00:01:47.080 --> 00:01:48.870 align:start position:0% stake is an important step along the way towards<00:01:47.590> scaling<00:01:48.040> I<00:01:48.159> wouldn't<00:01:48.430> say<00:01:48.580> that<00:01:48.700> it's 00:01:48.870 --> 00:01:48.880 align:start position:0% towards scaling I wouldn't say that it's 00:01:48.880 --> 00:01:50.760 align:start position:0% towards scaling I wouldn't say that it's it's<00:01:49.450> the<00:01:49.659> solution<00:01:50.110> to<00:01:50.170> scaling<00:01:50.409> but<00:01:50.590> it's 00:01:50.760 --> 00:01:50.770 align:start position:0% it's the solution to scaling but it's 00:01:50.770 --> 00:01:54.080 align:start position:0% it's the solution to scaling but it's it's<00:01:50.950> one<00:01:51.189> component<00:01:51.670> of<00:01:52.030> a<00:01:52.990> scaling<00:01:53.380> solution 00:01:54.080 --> 00:01:54.090 align:start position:0% it's one component of a scaling solution 00:01:54.090 --> 00:01:58.679 align:start position:0% it's one component of a scaling solution and<00:01:55.500> so<00:01:56.500> so<00:01:57.280> we<00:01:57.400> want<00:01:57.880> to<00:01:57.970> look<00:01:58.060> at<00:01:58.210> proof<00:01:58.540> of 00:01:58.679 --> 00:01:58.689 align:start position:0% and so so we want to look at proof of 00:01:58.689 --> 00:02:01.289 align:start position:0% and so so we want to look at proof of stake<00:01:58.990> and<00:01:59.320> in<00:01:59.409> particular<00:01:59.979> the<00:02:00.189> the<00:02:00.820> Casper 00:02:01.289 --> 00:02:01.299 align:start position:0% stake and in particular the the Casper 00:02:01.299 --> 00:02:03.539 align:start position:0% stake and in particular the the Casper variant<00:02:01.750> of<00:02:01.900> proof<00:02:02.080> of<00:02:02.259> stake<00:02:02.470> and<00:02:03.250> really 00:02:03.539 --> 00:02:03.549 align:start position:0% variant of proof of stake and really 00:02:03.549 --> 00:02:05.190 align:start position:0% variant of proof of stake and really bash<00:02:03.790> on<00:02:04.060> it<00:02:04.240> from<00:02:04.479> from<00:02:04.780> the<00:02:04.810> point<00:02:05.080> of<00:02:05.140> view 00:02:05.190 --> 00:02:05.200 align:start position:0% bash on it from from the point of view 00:02:05.200 --> 00:02:08.009 align:start position:0% bash on it from from the point of view of<00:02:05.500> a<00:02:05.530> formal<00:02:06.070> verification<00:02:06.689> we'd<00:02:07.689> like<00:02:07.869> to 00:02:08.009 --> 00:02:08.019 align:start position:0% of a formal verification we'd like to 00:02:08.019 --> 00:02:10.139 align:start position:0% of a formal verification we'd like to know<00:02:08.229> for<00:02:08.649> sure<00:02:08.709> once<00:02:09.369> and<00:02:09.609> for<00:02:09.759> all<00:02:09.819> whether 00:02:10.139 --> 00:02:10.149 align:start position:0% know for sure once and for all whether 00:02:10.149 --> 00:02:13.009 align:start position:0% know for sure once and for all whether Casper<00:02:11.079> enjoys<00:02:11.379> certain<00:02:11.739> properties 00:02:13.009 --> 00:02:13.019 align:start position:0% Casper enjoys certain properties 00:02:13.019 --> 00:02:15.920 align:start position:0% Casper enjoys certain properties and<00:02:13.439> so<00:02:14.040> we're<00:02:14.790> one<00:02:15.090> of<00:02:15.209> the<00:02:15.299> tools<00:02:15.510> that<00:02:15.810> were 00:02:15.920 --> 00:02:15.930 align:start position:0% and so we're one of the tools that were 00:02:15.930 --> 00:02:17.449 align:start position:0% and so we're one of the tools that were using<00:02:16.110> to<00:02:16.379> go<00:02:16.500> about<00:02:16.709> this<00:02:16.980> is<00:02:17.159> something 00:02:17.449 --> 00:02:17.459 align:start position:0% using to go about this is something 00:02:17.459 --> 00:02:20.300 align:start position:0% using to go about this is something called<00:02:17.610> the<00:02:17.790> applied<00:02:18.150> PI<00:02:18.420> calculus<00:02:19.159> and<00:02:20.159> this 00:02:20.300 --> 00:02:20.310 align:start position:0% called the applied PI calculus and this 00:02:20.310 --> 00:02:23.479 align:start position:0% called the applied PI calculus and this gives<00:02:20.519> us<00:02:20.670> and<00:02:21.299> I'll<00:02:21.420> show<00:02:22.129> kind<00:02:23.129> of<00:02:23.159> where<00:02:23.340> we 00:02:23.479 --> 00:02:23.489 align:start position:0% gives us and I'll show kind of where we 00:02:23.489 --> 00:02:26.179 align:start position:0% gives us and I'll show kind of where we are<00:02:23.519> and<00:02:23.970> in<00:02:24.209> the<00:02:24.329> state<00:02:24.540> of<00:02:24.659> that<00:02:25.010> later<00:02:26.010> in 00:02:26.179 --> 00:02:26.189 align:start position:0% are and in the state of that later in 00:02:26.189 --> 00:02:26.780 align:start position:0% are and in the state of that later in the<00:02:26.280> talk 00:02:26.780 --> 00:02:26.790 align:start position:0% the talk 00:02:26.790 --> 00:02:29.149 align:start position:0% the talk but<00:02:27.090> this<00:02:27.239> gives<00:02:27.450> us<00:02:27.599> access<00:02:27.930> to<00:02:28.470> automated 00:02:29.149 --> 00:02:29.159 align:start position:0% but this gives us access to automated 00:02:29.159 --> 00:02:32.539 align:start position:0% but this gives us access to automated support<00:02:29.700> for<00:02:29.939> a<00:02:29.970> proof<00:02:30.269> of<00:02:30.420> correctness<00:02:31.549> so 00:02:32.539 --> 00:02:32.549 align:start position:0% support for a proof of correctness so 00:02:32.549 --> 00:02:34.490 align:start position:0% support for a proof of correctness so the<00:02:32.700> tools<00:02:32.939> that<00:02:33.120> we're<00:02:33.329> employing<00:02:34.079> right<00:02:34.290> now 00:02:34.490 --> 00:02:34.500 align:start position:0% the tools that we're employing right now 00:02:34.500 --> 00:02:38.690 align:start position:0% the tools that we're employing right now in<00:02:34.859> include<00:02:36.019> Provera<00:02:37.019> f--<00:02:37.170> but<00:02:37.439> but<00:02:37.620> much<00:02:38.430> more 00:02:38.690 --> 00:02:38.700 align:start position:0% in include Provera f-- but but much more 00:02:38.700 --> 00:02:40.460 align:start position:0% in include Provera f-- but but much more the<00:02:38.939> spatial<00:02:39.390> logic<00:02:39.689> model<00:02:39.959> checker<00:02:40.200> which 00:02:40.460 --> 00:02:40.470 align:start position:0% the spatial logic model checker which 00:02:40.470 --> 00:02:45.949 align:start position:0% the spatial logic model checker which was<00:02:40.620> developed<00:02:41.010> by<00:02:41.069> lewis<00:02:41.430> Scotties<00:02:42.109> and<00:02:44.959> that 00:02:45.949 --> 00:02:45.959 align:start position:0% was developed by lewis Scotties and that 00:02:45.959 --> 00:02:47.960 align:start position:0% was developed by lewis Scotties and that turns<00:02:46.200> out<00:02:46.349> to<00:02:46.470> be<00:02:46.500> good<00:02:46.769> fun<00:02:47.010> and<00:02:47.310> if<00:02:47.609> you<00:02:47.730> want 00:02:47.960 --> 00:02:47.970 align:start position:0% turns out to be good fun and if you want 00:02:47.970 --> 00:02:50.149 align:start position:0% turns out to be good fun and if you want to<00:02:48.030> look<00:02:48.150> at<00:02:48.299> the<00:02:48.389> code<00:02:48.659> it's<00:02:49.650> up<00:02:49.829> on<00:02:49.950> github 00:02:50.149 --> 00:02:50.159 align:start position:0% to look at the code it's up on github 00:02:50.159 --> 00:02:52.250 align:start position:0% to look at the code it's up on github and<00:02:50.579> i'll<00:02:50.639> give<00:02:51.030> you<00:02:51.120> a<00:02:51.150> link<00:02:51.359> of<00:02:51.510> it<00:02:51.659> in<00:02:51.870> a<00:02:52.079> bit 00:02:52.250 --> 00:02:52.260 align:start position:0% and i'll give you a link of it in a bit 00:02:52.260 --> 00:02:55.339 align:start position:0% and i'll give you a link of it in a bit later<00:02:52.470> but<00:02:53.430> it<00:02:53.579> turns<00:02:53.849> out<00:02:54.090> that<00:02:54.569> if<00:02:55.019> you<00:02:55.319> have 00:02:55.339 --> 00:02:55.349 align:start position:0% later but it turns out that if you have 00:02:55.349 --> 00:02:58.369 align:start position:0% later but it turns out that if you have a<00:02:55.620> speck<00:02:56.159> in<00:02:56.489> the<00:02:56.579> applied<00:02:57.329> PI<00:02:57.599> calculus<00:02:58.170> well 00:02:58.369 --> 00:02:58.379 align:start position:0% a speck in the applied PI calculus well 00:02:58.379 --> 00:03:00.530 align:start position:0% a speck in the applied PI calculus well I<00:02:58.409> have<00:02:58.709> a<00:02:58.739> bunch<00:02:59.010> of<00:02:59.129> libraries<00:02:59.700> that<00:02:59.909> up<00:03:00.329> on 00:03:00.530 --> 00:03:00.540 align:start position:0% I have a bunch of libraries that up on 00:03:00.540 --> 00:03:03.379 align:start position:0% I have a bunch of libraries that up on github<00:03:00.689> called<00:03:01.170> Special<00:03:01.680> K<00:03:01.889> and<00:03:02.220> they<00:03:02.970> are<00:03:03.269> an 00:03:03.379 --> 00:03:03.389 align:start position:0% github called Special K and they are an 00:03:03.389 --> 00:03:08.360 align:start position:0% github called Special K and they are an implementation<00:03:05.180> an<00:03:06.180> executable<00:03:07.370> distributed 00:03:08.360 --> 00:03:08.370 align:start position:0% implementation an executable distributed 00:03:08.370 --> 00:03:10.280 align:start position:0% implementation an executable distributed virtual<00:03:08.790> machine<00:03:09.209> of<00:03:09.569> the<00:03:09.780> applied<00:03:10.079> PI 00:03:10.280 --> 00:03:10.290 align:start position:0% virtual machine of the applied PI 00:03:10.290 --> 00:03:13.490 align:start position:0% virtual machine of the applied PI calculus<00:03:10.859> so<00:03:11.549> if<00:03:11.790> you<00:03:11.939> have<00:03:12.120> a<00:03:12.150> spec<00:03:12.569> you<00:03:13.439> can 00:03:13.490 --> 00:03:13.500 align:start position:0% calculus so if you have a spec you can 00:03:13.500 --> 00:03:15.640 align:start position:0% calculus so if you have a spec you can turn<00:03:13.799> it<00:03:13.980> straight<00:03:14.189> into<00:03:14.519> an<00:03:14.670> implementation 00:03:15.640 --> 00:03:15.650 align:start position:0% turn it straight into an implementation 00:03:15.650 --> 00:03:17.659 align:start position:0% turn it straight into an implementation so<00:03:16.650> if<00:03:16.709> you<00:03:16.799> have<00:03:16.889> a<00:03:16.919> spec<00:03:17.220> that<00:03:17.250> you<00:03:17.489> can 00:03:17.659 --> 00:03:17.669 align:start position:0% so if you have a spec that you can 00:03:17.669 --> 00:03:20.629 align:start position:0% so if you have a spec that you can reason<00:03:18.269> about<00:03:18.359> the<00:03:19.040> correctness<00:03:20.040> properties 00:03:20.629 --> 00:03:20.639 align:start position:0% reason about the correctness properties 00:03:20.639 --> 00:03:25.369 align:start position:0% reason about the correctness properties then<00:03:21.299> you<00:03:21.480> can<00:03:21.660> actually<00:03:21.810> run<00:03:22.139> Casper<00:03:22.709> and<00:03:24.379> so 00:03:25.369 --> 00:03:25.379 align:start position:0% then you can actually run Casper and so 00:03:25.379 --> 00:03:27.559 align:start position:0% then you can actually run Casper and so this<00:03:25.590> this<00:03:25.859> is<00:03:25.919> has<00:03:26.340> big<00:03:26.579> implications<00:03:26.790> for 00:03:27.559 --> 00:03:27.569 align:start position:0% this this is has big implications for 00:03:27.569 --> 00:03:29.059 align:start position:0% this this is has big implications for the<00:03:27.810> correctness<00:03:28.079> of<00:03:28.260> an<00:03:28.379> implementation 00:03:29.059 --> 00:03:29.069 align:start position:0% the correctness of an implementation 00:03:29.069 --> 00:03:31.220 align:start position:0% the correctness of an implementation what<00:03:29.639> you<00:03:29.790> get<00:03:30.000> is<00:03:30.180> correct<00:03:30.480> by<00:03:30.599> construction 00:03:31.220 --> 00:03:31.230 align:start position:0% what you get is correct by construction 00:03:31.230 --> 00:03:33.920 align:start position:0% what you get is correct by construction and<00:03:31.609> that's<00:03:32.609> that's<00:03:32.819> a<00:03:33.000> that's<00:03:33.150> a<00:03:33.419> different 00:03:33.920 --> 00:03:33.930 align:start position:0% and that's that's a that's a different 00:03:33.930 --> 00:03:36.409 align:start position:0% and that's that's a that's a different approach<00:03:34.349> to<00:03:34.680> design<00:03:35.069> than<00:03:35.370> I<00:03:35.430> think<00:03:35.489> you<00:03:36.299> know 00:03:36.409 --> 00:03:36.419 align:start position:0% approach to design than I think you know 00:03:36.419 --> 00:03:40.339 align:start position:0% approach to design than I think you know happens<00:03:37.230> in<00:03:37.889> a<00:03:38.159> lot<00:03:38.340> of<00:03:38.810> software<00:03:39.810> a<00:03:40.049> lot<00:03:40.230> of 00:03:40.339 --> 00:03:40.349 align:start position:0% happens in a lot of software a lot of 00:03:40.349 --> 00:03:42.559 align:start position:0% happens in a lot of software a lot of the<00:03:40.440> software<00:03:40.739> industry<00:03:40.859> but<00:03:41.699> it<00:03:41.849> but<00:03:42.419> in 00:03:42.559 --> 00:03:42.569 align:start position:0% the software industry but it but in 00:03:42.569 --> 00:03:45.050 align:start position:0% the software industry but it but in particular<00:03:43.109> in<00:03:43.229> this<00:03:43.379> space<00:03:43.669> I'm<00:03:44.669> not<00:03:44.729> sure 00:03:45.050 --> 00:03:45.060 align:start position:0% particular in this space I'm not sure 00:03:45.060 --> 00:03:49.430 align:start position:0% particular in this space I'm not sure that<00:03:45.090> that<00:03:45.449> that<00:03:47.659> the<00:03:48.659> blockchain<00:03:48.930> as 00:03:49.430 --> 00:03:49.440 align:start position:0% that that that the blockchain as 00:03:49.440 --> 00:03:51.379 align:start position:0% that that that the blockchain as originally<00:03:49.919> conceived<00:03:50.340> was<00:03:50.579> was<00:03:50.879> done<00:03:51.150> in<00:03:51.299> a 00:03:51.379 --> 00:03:51.389 align:start position:0% originally conceived was was done in a 00:03:51.389 --> 00:03:53.449 align:start position:0% originally conceived was was done in a correct<00:03:51.750> by<00:03:51.870> construction<00:03:52.349> style<00:03:52.739> and<00:03:53.400> I 00:03:53.449 --> 00:03:53.459 align:start position:0% correct by construction style and I 00:03:53.459 --> 00:03:55.099 align:start position:0% correct by construction style and I think<00:03:53.639> it<00:03:53.699> was<00:03:53.819> quite<00:03:54.239> quite<00:03:54.449> the<00:03:54.690> opposite 00:03:55.099 --> 00:03:55.109 align:start position:0% think it was quite quite the opposite 00:03:55.109 --> 00:03:58.129 align:start position:0% think it was quite quite the opposite actually<00:03:55.849> but<00:03:56.849> but<00:03:57.090> if<00:03:57.239> you<00:03:57.389> didn't<00:03:57.720> take<00:03:57.930> on 00:03:58.129 --> 00:03:58.139 align:start position:0% actually but but if you didn't take on 00:03:58.139 --> 00:04:00.439 align:start position:0% actually but but if you didn't take on correct<00:03:58.560> by<00:03:58.680> construction<00:03:59.099> one<00:03:59.370> this<00:04:00.120> helps 00:04:00.439 --> 00:04:00.449 align:start position:0% correct by construction one this helps 00:04:00.449 --> 00:04:01.849 align:start position:0% correct by construction one this helps with<00:04:00.599> scaling<00:04:01.049> there<00:04:01.560> are<00:04:01.620> a<00:04:01.680> lot<00:04:01.829> of 00:04:01.849 --> 00:04:01.859 align:start position:0% with scaling there are a lot of 00:04:01.859 --> 00:04:04.129 align:start position:0% with scaling there are a lot of different<00:04:02.250> aspects<00:04:02.699> to<00:04:02.879> scaling<00:04:03.150> right<00:04:03.510> it's 00:04:04.129 --> 00:04:04.139 align:start position:0% different aspects to scaling right it's 00:04:04.139 --> 00:04:06.170 align:start position:0% different aspects to scaling right it's not<00:04:04.409> just<00:04:04.769> about<00:04:04.889> volume<00:04:05.489> and<00:04:05.579> performance 00:04:06.170 --> 00:04:06.180 align:start position:0% not just about volume and performance 00:04:06.180 --> 00:04:10.009 align:start position:0% not just about volume and performance right<00:04:07.109> it's<00:04:07.530> also<00:04:07.889> about<00:04:08.750> when<00:04:09.750> you<00:04:09.840> have 00:04:10.009 --> 00:04:10.019 align:start position:0% right it's also about when you have 00:04:10.019 --> 00:04:11.990 align:start position:0% right it's also about when you have reliability<00:04:10.799> reliability<00:04:11.069> is<00:04:11.819> what 00:04:11.990 --> 00:04:12.000 align:start position:0% reliability reliability is what 00:04:12.000 --> 00:04:14.930 align:start position:0% reliability reliability is what engenders<00:04:12.599> adoption<00:04:13.290> right<00:04:14.280> so<00:04:14.489> you<00:04:14.579> think 00:04:14.930 --> 00:04:14.940 align:start position:0% engenders adoption right so you think 00:04:14.940 --> 00:04:18.080 align:start position:0% engenders adoption right so you think about<00:04:15.120> your<00:04:15.349> yours<00:04:16.349> your<00:04:16.769> you're<00:04:17.579> someone<00:04:17.940> who 00:04:18.080 --> 00:04:18.090 align:start position:0% about your yours your you're someone who 00:04:18.090 --> 00:04:20.180 align:start position:0% about your yours your you're someone who manages<00:04:18.359> a<00:04:18.690> large<00:04:18.989> financial<00:04:19.680> firm<00:04:19.949> and 00:04:20.180 --> 00:04:20.190 align:start position:0% manages a large financial firm and 00:04:20.190 --> 00:04:22.399 align:start position:0% manages a large financial firm and there's<00:04:20.760> this<00:04:20.940> great<00:04:21.269> new<00:04:21.380> technology<00:04:22.380> that 00:04:22.399 --> 00:04:22.409 align:start position:0% there's this great new technology that 00:04:22.409 --> 00:04:24.920 align:start position:0% there's this great new technology that promises<00:04:23.159> wonderful<00:04:23.610> things<00:04:23.849> but<00:04:24.539> am<00:04:24.690> I<00:04:24.779> going 00:04:24.920 --> 00:04:24.930 align:start position:0% promises wonderful things but am I going 00:04:24.930 --> 00:04:26.060 align:start position:0% promises wonderful things but am I going to<00:04:25.050> swap<00:04:25.289> it<00:04:25.469> out<00:04:25.560> for<00:04:25.620> the<00:04:25.860> thing 00:04:26.060 --> 00:04:26.070 align:start position:0% to swap it out for the thing 00:04:26.070 --> 00:04:29.120 align:start position:0% to swap it out for the thing it<00:04:26.190> works<00:04:26.690> well<00:04:27.690> I<00:04:27.720> might<00:04:28.170> be<00:04:28.200> more<00:04:28.680> inclined 00:04:29.120 --> 00:04:29.130 align:start position:0% it works well I might be more inclined 00:04:29.130 --> 00:04:31.760 align:start position:0% it works well I might be more inclined to<00:04:29.280> do<00:04:29.520> that<00:04:29.930> take<00:04:30.930> take<00:04:31.200> on<00:04:31.380> some<00:04:31.620> of<00:04:31.740> that 00:04:31.760 --> 00:04:31.770 align:start position:0% to do that take take on some of that 00:04:31.770 --> 00:04:33.740 align:start position:0% to do that take take on some of that risk<00:04:32.100> if<00:04:32.400> I<00:04:32.550> knew<00:04:32.820> that<00:04:33.210> it<00:04:33.300> had<00:04:33.330> certain 00:04:33.740 --> 00:04:33.750 align:start position:0% risk if I knew that it had certain 00:04:33.750 --> 00:04:35.480 align:start position:0% risk if I knew that it had certain reliability<00:04:33.990> properties<00:04:34.950> that<00:04:35.340> were 00:04:35.480 --> 00:04:35.490 align:start position:0% reliability properties that were 00:04:35.490 --> 00:04:39.920 align:start position:0% reliability properties that were formally<00:04:36.120> and<00:04:36.330> automatically<00:04:36.930> verified<00:04:38.930> it 00:04:39.920 --> 00:04:39.930 align:start position:0% formally and automatically verified it 00:04:39.930 --> 00:04:43.880 align:start position:0% formally and automatically verified it also<00:04:40.080> helps<00:04:41.030> with<00:04:42.030> with<00:04:42.630> maintenance<00:04:43.320> and 00:04:43.880 --> 00:04:43.890 align:start position:0% also helps with with maintenance and 00:04:43.890 --> 00:04:46.520 align:start position:0% also helps with with maintenance and evolution<00:04:44.490> because<00:04:45.270> as<00:04:45.660> we<00:04:45.810> know<00:04:45.840> this<00:04:46.350> space 00:04:46.520 --> 00:04:46.530 align:start position:0% evolution because as we know this space 00:04:46.530 --> 00:04:49.370 align:start position:0% evolution because as we know this space is<00:04:46.770> changing<00:04:46.980> very<00:04:47.220> fast<00:04:47.460> and<00:04:48.210> so<00:04:48.870> it's<00:04:49.170> kind 00:04:49.370 --> 00:04:49.380 align:start position:0% is changing very fast and so it's kind 00:04:49.380 --> 00:04:53.840 align:start position:0% is changing very fast and so it's kind of<00:04:49.440> important<00:04:50.010> to<00:04:50.220> be<00:04:50.550> able<00:04:50.670> to<00:04:51.000> to<00:04:51.890> adapt<00:04:52.890> the 00:04:53.840 --> 00:04:53.850 align:start position:0% of important to be able to to adapt the 00:04:53.850 --> 00:05:00.830 align:start position:0% of important to be able to to adapt the code<00:04:54.090> to<00:04:54.780> the<00:04:54.810> needs<00:04:55.170> of<00:04:55.350> the<00:04:55.470> space<00:04:56.690> so<00:04:59.840> it 00:05:00.830 --> 00:05:00.840 align:start position:0% code to the needs of the space so it 00:05:00.840 --> 00:05:04.790 align:start position:0% code to the needs of the space so it turns<00:05:01.200> out<00:05:01.440> that<00:05:02.210> in<00:05:03.210> addition<00:05:03.930> to<00:05:04.290> some<00:05:04.770> of 00:05:04.790 --> 00:05:04.800 align:start position:0% turns out that in addition to some of 00:05:04.800 --> 00:05:08.750 align:start position:0% turns out that in addition to some of these<00:05:05.010> benefits<00:05:06.620> Special<00:05:07.620> K<00:05:07.830> provide<00:05:08.250> already 00:05:08.750 --> 00:05:08.760 align:start position:0% these benefits Special K provide already 00:05:08.760 --> 00:05:11.930 align:start position:0% these benefits Special K provide already of<00:05:09.360> its<00:05:09.900> own<00:05:10.110> provides<00:05:10.770> a<00:05:10.920> broad<00:05:11.220> range<00:05:11.580> of 00:05:11.930 --> 00:05:11.940 align:start position:0% of its own provides a broad range of 00:05:11.940 --> 00:05:15.140 align:start position:0% of its own provides a broad range of transactional<00:05:12.660> semantics<00:05:13.230> and<00:05:13.680> and<00:05:14.490> we<00:05:14.940> get 00:05:15.140 --> 00:05:15.150 align:start position:0% transactional semantics and and we get 00:05:15.150 --> 00:05:17.890 align:start position:0% transactional semantics and and we get these<00:05:15.420> because<00:05:16.200> of<00:05:16.560> the<00:05:16.980> monadic 00:05:17.890 --> 00:05:17.900 align:start position:0% these because of the monadic 00:05:17.900 --> 00:05:21.050 align:start position:0% these because of the monadic decomposition<00:05:18.900> of<00:05:18.930> the<00:05:19.920> the<00:05:20.190> elements<00:05:20.820> that 00:05:21.050 --> 00:05:21.060 align:start position:0% decomposition of the the elements that 00:05:21.060 --> 00:05:23.420 align:start position:0% decomposition of the the elements that are<00:05:21.180> that<00:05:21.450> are<00:05:21.570> used<00:05:21.840> to<00:05:22.110> to<00:05:22.620> make<00:05:22.860> these<00:05:23.100> kinds 00:05:23.420 --> 00:05:23.430 align:start position:0% are that are used to to make these kinds 00:05:23.430 --> 00:05:25.280 align:start position:0% are that are used to to make these kinds of<00:05:23.490> transactions<00:05:24.150> and<00:05:24.540> I'll<00:05:24.630> go<00:05:25.050> through 00:05:25.280 --> 00:05:25.290 align:start position:0% of transactions and I'll go through 00:05:25.290 --> 00:05:27.170 align:start position:0% of transactions and I'll go through those<00:05:25.440> but<00:05:26.070> you<00:05:26.340> know<00:05:26.460> there's<00:05:26.880> there's 00:05:27.170 --> 00:05:27.180 align:start position:0% those but you know there's there's 00:05:27.180 --> 00:05:29.990 align:start position:0% those but you know there's there's basically<00:05:27.600> a<00:05:27.720> handful<00:05:28.500> of<00:05:29.000> programming 00:05:29.990 --> 00:05:30.000 align:start position:0% basically a handful of programming 00:05:30.000 --> 00:05:32.150 align:start position:0% basically a handful of programming paradigms<00:05:30.900> that<00:05:31.080> are<00:05:31.200> used<00:05:31.500> successfully 00:05:32.150 --> 00:05:32.160 align:start position:0% paradigms that are used successfully 00:05:32.160 --> 00:05:34.760 align:start position:0% paradigms that are used successfully today<00:05:32.820> in<00:05:33.060> building<00:05:33.450> distributed<00:05:34.410> systems 00:05:34.760 --> 00:05:34.770 align:start position:0% today in building distributed systems 00:05:34.770 --> 00:05:36.950 align:start position:0% today in building distributed systems and<00:05:35.070> and<00:05:35.790> it<00:05:35.970> turns<00:05:36.180> out<00:05:36.390> that<00:05:36.630> you<00:05:36.780> can 00:05:36.950 --> 00:05:36.960 align:start position:0% and and it turns out that you can 00:05:36.960 --> 00:05:40.160 align:start position:0% and and it turns out that you can organize<00:05:37.170> all<00:05:38.040> of<00:05:38.460> those<00:05:38.640> under<00:05:39.630> a<00:05:39.660> single 00:05:40.160 --> 00:05:40.170 align:start position:0% organize all of those under a single 00:05:40.170 --> 00:05:44.830 align:start position:0% organize all of those under a single rubric<00:05:40.680> under<00:05:41.010> essentially<00:05:41.670> a<00:05:41.700> single<00:05:42.060> API 00:05:44.830 --> 00:05:44.840 align:start position:0% 00:05:44.840 --> 00:05:47.960 align:start position:0% additionally<00:05:45.840> the<00:05:46.560> compositional<00:05:47.250> nature<00:05:47.670> of 00:05:47.960 --> 00:05:47.970 align:start position:0% additionally the compositional nature of 00:05:47.970 --> 00:05:52.670 align:start position:0% additionally the compositional nature of the<00:05:48.800> the<00:05:49.800> PI<00:05:49.950> calculus<00:05:50.550> so<00:05:51.540> I'm<00:05:51.960> just<00:05:52.230> giving 00:05:52.670 --> 00:05:52.680 align:start position:0% the the PI calculus so I'm just giving 00:05:52.680 --> 00:05:55.610 align:start position:0% the the PI calculus so I'm just giving you<00:05:52.860> some<00:05:53.130> sense<00:05:53.730> of<00:05:53.940> all<00:05:54.150> the<00:05:54.300> benefits<00:05:54.810> of<00:05:55.080> of 00:05:55.610 --> 00:05:55.620 align:start position:0% you some sense of all the benefits of of 00:05:55.620 --> 00:05:58.160 align:start position:0% you some sense of all the benefits of of this<00:05:56.190> kind<00:05:56.580> of<00:05:56.730> approach<00:05:57.150> makes<00:05:57.840> it<00:05:57.990> possible 00:05:58.160 --> 00:05:58.170 align:start position:0% this kind of approach makes it possible 00:05:58.170 --> 00:06:01.510 align:start position:0% this kind of approach makes it possible to<00:05:58.500> write<00:05:58.770> down<00:05:59.040> in<00:05:59.190> a<00:05:59.280> single<00:05:59.550> page<00:06:00.000> a<00:06:00.450> metered 00:06:01.510 --> 00:06:01.520 align:start position:0% to write down in a single page a metered 00:06:01.520 --> 00:06:05.060 align:start position:0% to write down in a single page a metered distributed<00:06:02.520> concurrent<00:06:03.210> VM<00:06:03.510> so<00:06:04.200> just<00:06:04.860> for 00:06:05.060 --> 00:06:05.070 align:start position:0% distributed concurrent VM so just for 00:06:05.070 --> 00:06:07.670 align:start position:0% distributed concurrent VM so just for fun<00:06:05.130> I'll<00:06:05.760> show<00:06:06.510> you<00:06:06.570> that<00:06:06.840> spec<00:06:07.170> right<00:06:07.410> at<00:06:07.560> the 00:06:07.670 --> 00:06:07.680 align:start position:0% fun I'll show you that spec right at the 00:06:07.680 --> 00:06:10.910 align:start position:0% fun I'll show you that spec right at the end<00:06:07.830> ooh<00:06:08.660> that's<00:06:09.660> some<00:06:09.840> nice<00:06:10.050> feedback<00:06:10.380> that's 00:06:10.910 --> 00:06:10.920 align:start position:0% end ooh that's some nice feedback that's 00:06:10.920 --> 00:06:15.140 align:start position:0% end ooh that's some nice feedback that's some<00:06:11.070> really<00:06:11.420> nice<00:06:12.420> high<00:06:12.690> frequencies 00:06:15.140 --> 00:06:15.150 align:start position:0% some really nice high frequencies 00:06:15.150 --> 00:06:17.790 align:start position:0% some really nice high frequencies okay<00:06:16.150> so<00:06:16.210> so<00:06:16.840> the<00:06:16.870> big<00:06:17.139> picture<00:06:17.560> is<00:06:17.770> that 00:06:17.790 --> 00:06:17.800 align:start position:0% okay so so the big picture is that 00:06:17.800 --> 00:06:20.189 align:start position:0% okay so so the big picture is that compositionality<00:06:18.730> is<00:06:19.180> the<00:06:19.360> key<00:06:19.540> to<00:06:19.750> scaling 00:06:20.189 --> 00:06:20.199 align:start position:0% compositionality is the key to scaling 00:06:20.199 --> 00:06:22.500 align:start position:0% compositionality is the key to scaling any<00:06:20.290> system<00:06:20.770> so<00:06:21.370> if<00:06:21.639> you<00:06:21.790> forget<00:06:22.120> every 00:06:22.500 --> 00:06:22.510 align:start position:0% any system so if you forget every 00:06:22.510 --> 00:06:24.990 align:start position:0% any system so if you forget every everything<00:06:22.990> else<00:06:23.290> in<00:06:23.530> this<00:06:23.650> talk<00:06:23.919> if<00:06:24.250> you 00:06:24.990 --> 00:06:25.000 align:start position:0% everything else in this talk if you 00:06:25.000 --> 00:06:27.420 align:start position:0% everything else in this talk if you remember<00:06:25.449> that<00:06:25.479> one<00:06:25.870> idea<00:06:26.290> you<00:06:27.130> know<00:06:27.250> I'm 00:06:27.420 --> 00:06:27.430 align:start position:0% remember that one idea you know I'm 00:06:27.430 --> 00:06:29.400 align:start position:0% remember that one idea you know I'm hoping<00:06:28.030> to<00:06:28.150> plant<00:06:28.389> that<00:06:28.570> seed<00:06:28.840> in<00:06:29.050> your<00:06:29.139> mind 00:06:29.400 --> 00:06:29.410 align:start position:0% hoping to plant that seed in your mind 00:06:29.410 --> 00:06:31.890 align:start position:0% hoping to plant that seed in your mind and<00:06:29.710> go<00:06:30.520> home<00:06:30.790> and<00:06:31.030> think<00:06:31.210> about<00:06:31.419> that<00:06:31.570> so<00:06:31.780> what 00:06:31.890 --> 00:06:31.900 align:start position:0% and go home and think about that so what 00:06:31.900 --> 00:06:33.659 align:start position:0% and go home and think about that so what the<00:06:31.990> hell<00:06:32.139> is<00:06:32.290> compositionality<00:06:32.919> is<00:06:33.250> it<00:06:33.370> even 00:06:33.659 --> 00:06:33.669 align:start position:0% the hell is compositionality is it even 00:06:33.669 --> 00:06:36.840 align:start position:0% the hell is compositionality is it even a<00:06:33.760> word<00:06:34.030> right<00:06:34.810> if<00:06:35.520> spellcheck<00:06:36.520> is<00:06:36.669> gonna 00:06:36.840 --> 00:06:36.850 align:start position:0% a word right if spellcheck is gonna 00:06:36.850 --> 00:06:40.920 align:start position:0% a word right if spellcheck is gonna underline<00:06:37.210> it<00:06:37.540> in<00:06:37.690> red<00:06:37.930> I<00:06:37.960> guarantee<00:06:38.830> you<00:06:39.930> so 00:06:40.920 --> 00:06:40.930 align:start position:0% underline it in red I guarantee you so 00:06:40.930 --> 00:06:42.659 align:start position:0% underline it in red I guarantee you so let<00:06:41.110> me<00:06:41.139> let<00:06:41.380> me<00:06:41.410> kind<00:06:41.650> of<00:06:41.740> unpack<00:06:42.070> this<00:06:42.280> idea 00:06:42.659 --> 00:06:42.669 align:start position:0% let me let me kind of unpack this idea 00:06:42.669 --> 00:06:45.629 align:start position:0% let me let me kind of unpack this idea so<00:06:43.120> so<00:06:43.840> in<00:06:44.199> computing<00:06:44.919> I<00:06:45.130> think<00:06:45.340> we're<00:06:45.490> all 00:06:45.629 --> 00:06:45.639 align:start position:0% so so in computing I think we're all 00:06:45.639 --> 00:06:47.250 align:start position:0% so so in computing I think we're all familiar<00:06:45.820> with<00:06:46.090> the<00:06:46.240> idea<00:06:46.600> that<00:06:46.690> scaling 00:06:47.250 --> 00:06:47.260 align:start position:0% familiar with the idea that scaling 00:06:47.260 --> 00:06:49.110 align:start position:0% familiar with the idea that scaling refers<00:06:47.680> to<00:06:47.710> lots<00:06:48.070> and<00:06:48.280> lots<00:06:48.400> of<00:06:48.520> copies<00:06:48.760> of 00:06:49.110 --> 00:06:49.120 align:start position:0% refers to lots and lots of copies of 00:06:49.120 --> 00:06:51.210 align:start position:0% refers to lots and lots of copies of things<00:06:49.600> that<00:06:49.840> are<00:06:49.960> you<00:06:50.320> know<00:06:50.350> potentially<00:06:51.010> not 00:06:51.210 --> 00:06:51.220 align:start position:0% things that are you know potentially not 00:06:51.220 --> 00:06:53.520 align:start position:0% things that are you know potentially not reliable<00:06:51.790> individually<00:06:52.450> right<00:06:53.080> so<00:06:53.200> lots<00:06:53.380> of 00:06:53.520 --> 00:06:53.530 align:start position:0% reliable individually right so lots of 00:06:53.530 --> 00:06:56.940 align:start position:0% reliable individually right so lots of chips<00:06:53.770> lots<00:06:54.430> of<00:06:54.580> boxes<00:06:54.900> lots<00:06:55.900> of<00:06:56.139> databases 00:06:56.940 --> 00:06:56.950 align:start position:0% chips lots of boxes lots of databases 00:06:56.950 --> 00:06:59.070 align:start position:0% chips lots of boxes lots of databases lots<00:06:57.610> of<00:06:57.729> servers<00:06:58.120> lots<00:06:58.419> of<00:06:58.510> data<00:06:58.720> centers 00:06:59.070 --> 00:06:59.080 align:start position:0% lots of servers lots of data centers 00:06:59.080 --> 00:07:01.760 align:start position:0% lots of servers lots of data centers right<00:06:59.290> so<00:06:59.440> that's<00:06:59.560> the<00:06:59.919> traditional<00:07:00.729> you<00:07:01.389> know 00:07:01.760 --> 00:07:01.770 align:start position:0% right so that's the traditional you know 00:07:01.770 --> 00:07:04.190 align:start position:0% right so that's the traditional you know high-volume<00:07:02.790> high-performance 00:07:04.190 --> 00:07:04.200 align:start position:0% high-volume high-performance 00:07:04.200 --> 00:07:08.340 align:start position:0% high-volume high-performance notion<00:07:05.200> of<00:07:05.320> scaling<00:07:06.840> compositionality<00:07:07.840> turns 00:07:08.340 --> 00:07:08.350 align:start position:0% notion of scaling compositionality turns 00:07:08.350 --> 00:07:11.219 align:start position:0% notion of scaling compositionality turns this<00:07:08.560> upside<00:07:08.950> down<00:07:09.479> and<00:07:10.479> what<00:07:10.630> it<00:07:10.750> says<00:07:10.930> is 00:07:11.219 --> 00:07:11.229 align:start position:0% this upside down and what it says is 00:07:11.229 --> 00:07:14.070 align:start position:0% this upside down and what it says is that<00:07:11.260> scaling<00:07:11.710> is<00:07:11.979> about<00:07:12.280> making<00:07:12.610> the<00:07:13.449> the 00:07:14.070 --> 00:07:14.080 align:start position:0% that scaling is about making the the 00:07:14.080 --> 00:07:17.550 align:start position:0% that scaling is about making the the large<00:07:14.470> reflect<00:07:15.250> the<00:07:15.520> small<00:07:16.020> right<00:07:17.020> and<00:07:17.199> and 00:07:17.550 --> 00:07:17.560 align:start position:0% large reflect the small right and and 00:07:17.560 --> 00:07:20.790 align:start position:0% large reflect the small right and and every<00:07:18.039> child<00:07:18.630> understands<00:07:19.630> this<00:07:19.840> idea<00:07:20.229> they 00:07:20.790 --> 00:07:20.800 align:start position:0% every child understands this idea they 00:07:20.800 --> 00:07:23.010 align:start position:0% every child understands this idea they hold<00:07:21.039> up<00:07:21.190> the<00:07:21.310> leaf<00:07:21.490> they<00:07:22.450> look<00:07:22.630> at<00:07:22.750> the<00:07:22.840> leaf 00:07:23.010 --> 00:07:23.020 align:start position:0% hold up the leaf they look at the leaf 00:07:23.020 --> 00:07:25.740 align:start position:0% hold up the leaf they look at the leaf and<00:07:23.229> they<00:07:23.560> say<00:07:23.800> hey<00:07:24.100> there's<00:07:24.940> a<00:07:25.030> tree<00:07:25.389> inside 00:07:25.740 --> 00:07:25.750 align:start position:0% and they say hey there's a tree inside 00:07:25.750 --> 00:07:30.900 align:start position:0% and they say hey there's a tree inside this<00:07:25.990> leaf<00:07:26.820> right<00:07:28.710> and<00:07:29.710> that<00:07:30.130> is<00:07:30.310> in<00:07:30.460> fact<00:07:30.490> how 00:07:30.900 --> 00:07:30.910 align:start position:0% this leaf right and that is in fact how 00:07:30.910 --> 00:07:33.210 align:start position:0% this leaf right and that is in fact how nature<00:07:31.180> scales<00:07:31.599> then<00:07:32.200> we<00:07:32.320> see<00:07:32.530> it<00:07:32.620> again<00:07:32.979> and 00:07:33.210 --> 00:07:33.220 align:start position:0% nature scales then we see it again and 00:07:33.220 --> 00:07:36.060 align:start position:0% nature scales then we see it again and again<00:07:33.639> and<00:07:34.090> again<00:07:34.510> and<00:07:34.750> it's<00:07:35.470> kind<00:07:35.710> of<00:07:35.770> funny 00:07:36.060 --> 00:07:36.070 align:start position:0% again and again and it's kind of funny 00:07:36.070 --> 00:07:39.870 align:start position:0% again and again and it's kind of funny why<00:07:36.490> is<00:07:36.550> it<00:07:36.910> that<00:07:37.000> we<00:07:37.150> forget<00:07:37.830> we<00:07:38.830> knew<00:07:39.190> this<00:07:39.460> at 00:07:39.870 --> 00:07:39.880 align:start position:0% why is it that we forget we knew this at 00:07:39.880 --> 00:07:43.860 align:start position:0% why is it that we forget we knew this at one<00:07:40.210> point<00:07:40.479> and<00:07:40.950> then<00:07:41.950> we<00:07:42.160> forget<00:07:42.580> it<00:07:42.760> and<00:07:43.660> why 00:07:43.860 --> 00:07:43.870 align:start position:0% one point and then we forget it and why 00:07:43.870 --> 00:07:46.740 align:start position:0% one point and then we forget it and why is<00:07:43.930> it<00:07:44.169> that<00:07:44.320> we<00:07:44.440> forget<00:07:44.800> this<00:07:45.389> well<00:07:46.389> it<00:07:46.479> turns 00:07:46.740 --> 00:07:46.750 align:start position:0% is it that we forget this well it turns 00:07:46.750 --> 00:07:49.200 align:start position:0% is it that we forget this well it turns out<00:07:47.050> that<00:07:47.349> it's<00:07:47.740> actually<00:07:47.889> a<00:07:48.130> fairly<00:07:48.729> new 00:07:49.200 --> 00:07:49.210 align:start position:0% out that it's actually a fairly new 00:07:49.210 --> 00:07:53.580 align:start position:0% out that it's actually a fairly new thing<00:07:49.260> for<00:07:50.260> culture<00:07:50.770> to<00:07:50.979> remember<00:07:51.430> this<00:07:52.590> so 00:07:53.580 --> 00:07:53.590 align:start position:0% thing for culture to remember this so 00:07:53.590 --> 00:07:55.589 align:start position:0% thing for culture to remember this so I'm<00:07:53.860> just<00:07:54.070> giving<00:07:54.340> you<00:07:54.370> a<00:07:54.490> few<00:07:54.849> examples<00:07:54.910> from 00:07:55.589 --> 00:07:55.599 align:start position:0% I'm just giving you a few examples from 00:07:55.599 --> 00:07:59.730 align:start position:0% I'm just giving you a few examples from pop<00:07:55.810> culture<00:07:56.320> of<00:07:56.639> of<00:07:57.639> this<00:07:58.210> idea<00:07:58.720> and<00:07:59.080> you'll 00:07:59.730 --> 00:07:59.740 align:start position:0% pop culture of of this idea and you'll 00:07:59.740 --> 00:08:01.469 align:start position:0% pop culture of of this idea and you'll notice<00:08:00.099> that<00:08:00.280> all<00:08:00.610> of<00:08:00.820> them<00:08:00.970> I<00:08:01.090> mean<00:08:01.240> even 00:08:01.469 --> 00:08:01.479 align:start position:0% notice that all of them I mean even 00:08:01.479 --> 00:08:05.010 align:start position:0% notice that all of them I mean even Mandelbrot<00:08:02.229> sets<00:08:02.590> are<00:08:02.889> very<00:08:03.130> new<00:08:03.910> on<00:08:04.479> culture 00:08:05.010 --> 00:08:05.020 align:start position:0% Mandelbrot sets are very new on culture 00:08:05.020 --> 00:08:08.129 align:start position:0% Mandelbrot sets are very new on culture on<00:08:05.169> the<00:08:05.349> cultural<00:08:05.710> landscape<00:08:06.270> right<00:08:07.270> and<00:08:07.510> just 00:08:08.129 --> 00:08:08.139 align:start position:0% on the cultural landscape right and just 00:08:08.139 --> 00:08:11.029 align:start position:0% on the cultural landscape right and just to<00:08:08.260> give<00:08:08.410> you<00:08:08.500> another<00:08:08.770> sense<00:08:09.130> of<00:08:09.370> how<00:08:09.789> how 00:08:11.029 --> 00:08:11.039 align:start position:0% to give you another sense of how how 00:08:11.039 --> 00:08:13.230 align:start position:0% to give you another sense of how how interesting<00:08:12.039> and<00:08:12.190> different<00:08:12.760> this<00:08:12.880> way<00:08:13.090> of 00:08:13.230 --> 00:08:13.240 align:start position:0% interesting and different this way of 00:08:13.240 --> 00:08:15.719 align:start position:0% interesting and different this way of thinking<00:08:13.270> is<00:08:13.810> so<00:08:14.530> here's<00:08:14.770> a<00:08:14.830> bunch<00:08:15.070> of<00:08:15.310> people 00:08:15.719 --> 00:08:15.729 align:start position:0% thinking is so here's a bunch of people 00:08:15.729 --> 00:08:18.240 align:start position:0% thinking is so here's a bunch of people who<00:08:16.210> had<00:08:16.500> computationally<00:08:17.500> very<00:08:17.770> effective 00:08:18.240 --> 00:08:18.250 align:start position:0% who had computationally very effective 00:08:18.250 --> 00:08:21.240 align:start position:0% who had computationally very effective ideas<00:08:18.700> right<00:08:19.660> so<00:08:20.169> you<00:08:20.530> know<00:08:20.620> maybe<00:08:20.800> you<00:08:20.889> know<00:08:21.190> - 00:08:21.240 --> 00:08:21.250 align:start position:0% ideas right so you know maybe you know - 00:08:21.250 --> 00:08:24.060 align:start position:0% ideas right so you know maybe you know - maybe<00:08:21.580> you<00:08:21.760> recognize<00:08:21.909> Paul<00:08:22.450> Dirac<00:08:22.950> maybe<00:08:23.950> you 00:08:24.060 --> 00:08:24.070 align:start position:0% maybe you recognize Paul Dirac maybe you 00:08:24.070 --> 00:08:24.860 align:start position:0% maybe you recognize Paul Dirac maybe you recognize<00:08:24.250> er 00:08:24.860 --> 00:08:24.870 align:start position:0% recognize er 00:08:24.870 --> 00:08:27.110 align:start position:0% recognize er intro<00:08:25.260> dinger<00:08:25.650> but<00:08:26.010> quantum<00:08:26.370> mechanics<00:08:26.880> as 00:08:27.110 --> 00:08:27.120 align:start position:0% intro dinger but quantum mechanics as 00:08:27.120 --> 00:08:28.910 align:start position:0% intro dinger but quantum mechanics as formulated<00:08:27.690> in<00:08:28.170> those<00:08:28.350> days<00:08:28.590> was<00:08:28.890> not 00:08:28.910 --> 00:08:28.920 align:start position:0% formulated in those days was not 00:08:28.920 --> 00:08:31.370 align:start position:0% formulated in those days was not compositional<00:08:29.910> and<00:08:30.600> it's<00:08:30.750> only<00:08:30.930> been<00:08:31.140> in<00:08:31.290> the 00:08:31.370 --> 00:08:31.380 align:start position:0% compositional and it's only been in the 00:08:31.380 --> 00:08:33.160 align:start position:0% compositional and it's only been in the last<00:08:31.410> five<00:08:31.950> years<00:08:32.010> that<00:08:32.490> we've<00:08:32.640> had<00:08:32.670> a 00:08:33.160 --> 00:08:33.170 align:start position:0% last five years that we've had a 00:08:33.170 --> 00:08:34.940 align:start position:0% last five years that we've had a compositional<00:08:34.170> formulation<00:08:34.830> or 00:08:34.940 --> 00:08:34.950 align:start position:0% compositional formulation or 00:08:34.950 --> 00:08:37.160 align:start position:0% compositional formulation or presentation<00:08:35.580> of<00:08:35.730> quantum<00:08:36.420> mechanics<00:08:36.840> via 00:08:37.160 --> 00:08:37.170 align:start position:0% presentation of quantum mechanics via 00:08:37.170 --> 00:08:39.530 align:start position:0% presentation of quantum mechanics via Simpson<00:08:37.680> of<00:08:37.770> RAM<00:08:37.950> ski-in<00:08:38.250> Bob<00:08:38.520> Kocher<00:08:38.760> a 00:08:39.530 --> 00:08:39.540 align:start position:0% Simpson of RAM ski-in Bob Kocher a 00:08:39.540 --> 00:08:42.920 align:start position:0% Simpson of RAM ski-in Bob Kocher a similar<00:08:40.290> thing<00:08:40.470> has<00:08:40.680> happened<00:08:41.750> in<00:08:42.750> the 00:08:42.920 --> 00:08:42.930 align:start position:0% similar thing has happened in the 00:08:42.930 --> 00:08:45.080 align:start position:0% similar thing has happened in the physics<00:08:43.260> of<00:08:43.350> the<00:08:43.440> large<00:08:43.970> gravitation<00:08:44.970> and 00:08:45.080 --> 00:08:45.090 align:start position:0% physics of the large gravitation and 00:08:45.090 --> 00:08:47.840 align:start position:0% physics of the large gravitation and cosmology<00:08:45.120> and<00:08:45.810> because<00:08:46.320> we<00:08:46.500> don't<00:08:46.800> have<00:08:47.550> good 00:08:47.840 --> 00:08:47.850 align:start position:0% cosmology and because we don't have good 00:08:47.850 --> 00:08:50.660 align:start position:0% cosmology and because we don't have good compositional<00:08:48.540> accounts<00:08:48.990> physics<00:08:49.770> fails<00:08:50.280> to 00:08:50.660 --> 00:08:50.670 align:start position:0% compositional accounts physics fails to 00:08:50.670 --> 00:08:53.090 align:start position:0% compositional accounts physics fails to scale<00:08:50.940> we<00:08:51.780> don't<00:08:51.960> have<00:08:52.170> a<00:08:52.200> nice<00:08:52.470> way<00:08:52.710> to<00:08:52.770> marry 00:08:53.090 --> 00:08:53.100 align:start position:0% scale we don't have a nice way to marry 00:08:53.100 --> 00:08:55.520 align:start position:0% scale we don't have a nice way to marry those<00:08:53.310> two<00:08:53.520> ideas<00:08:53.700> so<00:08:54.660> if<00:08:54.900> you're<00:08:55.110> feeling 00:08:55.520 --> 00:08:55.530 align:start position:0% those two ideas so if you're feeling 00:08:55.530 --> 00:08:57.050 align:start position:0% those two ideas so if you're feeling like<00:08:55.680> hey<00:08:56.010> I'm<00:08:56.160> not<00:08:56.340> quite<00:08:56.670> sure<00:08:56.700> what 00:08:57.050 --> 00:08:57.060 align:start position:0% like hey I'm not quite sure what 00:08:57.060 --> 00:08:58.910 align:start position:0% like hey I'm not quite sure what compositionality<00:08:57.690> is<00:08:57.990> I'm<00:08:58.170> not<00:08:58.320> sure<00:08:58.470> not 00:08:58.910 --> 00:08:58.920 align:start position:0% compositionality is I'm not sure not 00:08:58.920 --> 00:09:01.190 align:start position:0% compositionality is I'm not sure not sure<00:08:58.950> well<00:08:59.580> these<00:08:59.880> guys<00:09:00.180> didn't<00:09:00.600> either 00:09:01.190 --> 00:09:01.200 align:start position:0% sure well these guys didn't either 00:09:01.200 --> 00:09:05.960 align:start position:0% sure well these guys didn't either so<00:09:02.190> it's<00:09:02.610> kind<00:09:02.910> of<00:09:03.000> okay<00:09:04.280> but<00:09:05.280> what<00:09:05.460> I<00:09:05.490> can<00:09:05.730> say 00:09:05.960 --> 00:09:05.970 align:start position:0% so it's kind of okay but what I can say 00:09:05.970 --> 00:09:09.260 align:start position:0% so it's kind of okay but what I can say is<00:09:06.240> that<00:09:06.750> the<00:09:06.900> notion<00:09:07.170> of<00:09:07.470> composition<00:09:08.270> has 00:09:09.260 --> 00:09:09.270 align:start position:0% is that the notion of composition has 00:09:09.270 --> 00:09:13.970 align:start position:0% is that the notion of composition has has<00:09:10.110> nice<00:09:11.240> formalizations<00:09:12.240> so<00:09:12.870> in<00:09:13.230> the<00:09:13.500> since 00:09:13.970 --> 00:09:13.980 align:start position:0% has nice formalizations so in the since 00:09:13.980 --> 00:09:16.670 align:start position:0% has nice formalizations so in the since about<00:09:14.340> the<00:09:14.640> 1950s<00:09:15.330> there's<00:09:16.320> been<00:09:16.560> an 00:09:16.670 --> 00:09:16.680 align:start position:0% about the 1950s there's been an 00:09:16.680 --> 00:09:18.950 align:start position:0% about the 1950s there's been an appropriately<00:09:17.640> parametric<00:09:18.450> notion<00:09:18.870> of 00:09:18.950 --> 00:09:18.960 align:start position:0% appropriately parametric notion of 00:09:18.960 --> 00:09:21.830 align:start position:0% appropriately parametric notion of composition<00:09:19.590> that<00:09:19.770> was<00:09:20.190> formulated<00:09:20.880> first<00:09:21.660> in 00:09:21.830 --> 00:09:21.840 align:start position:0% composition that was formulated first in 00:09:21.840 --> 00:09:23.900 align:start position:0% composition that was formulated first in category<00:09:22.320> theory<00:09:22.710> and<00:09:23.220> it<00:09:23.400> was<00:09:23.490> given<00:09:23.760> this 00:09:23.900 --> 00:09:23.910 align:start position:0% category theory and it was given this 00:09:23.910 --> 00:09:27.920 align:start position:0% category theory and it was given this weird<00:09:24.240> crazy<00:09:24.750> name<00:09:25.380> of<00:09:25.680> a<00:09:25.800> monad<00:09:26.420> if<00:09:27.420> you<00:09:27.660> if 00:09:27.920 --> 00:09:27.930 align:start position:0% weird crazy name of a monad if you if 00:09:27.930 --> 00:09:30.070 align:start position:0% weird crazy name of a monad if you if you<00:09:28.080> pair<00:09:28.500> monads<00:09:29.100> with<00:09:29.340> their<00:09:29.520> dual 00:09:30.070 --> 00:09:30.080 align:start position:0% you pair monads with their dual 00:09:30.080 --> 00:09:33.800 align:start position:0% you pair monads with their dual mathematical<00:09:31.080> widget<00:09:31.440> the<00:09:31.950> comonad<00:09:32.810> you 00:09:33.800 --> 00:09:33.810 align:start position:0% mathematical widget the comonad you 00:09:33.810 --> 00:09:35.840 align:start position:0% mathematical widget the comonad you couldn't<00:09:34.110> think<00:09:34.230> of<00:09:34.440> them<00:09:34.620> so<00:09:35.100> composition<00:09:35.730> is 00:09:35.840 --> 00:09:35.850 align:start position:0% couldn't think of them so composition is 00:09:35.850 --> 00:09:37.370 align:start position:0% couldn't think of them so composition is kind<00:09:36.030> of<00:09:36.090> like<00:09:36.270> nesting<00:09:36.750> right<00:09:36.930> it's<00:09:37.170> like<00:09:37.320> the 00:09:37.370 --> 00:09:37.380 align:start position:0% kind of like nesting right it's like the 00:09:37.380 --> 00:09:39.950 align:start position:0% kind of like nesting right it's like the Russian<00:09:37.830> dolls<00:09:38.040> you<00:09:38.340> you<00:09:38.820> nest<00:09:39.120> you<00:09:39.600> you<00:09:39.840> know 00:09:39.950 --> 00:09:39.960 align:start position:0% Russian dolls you you nest you you know 00:09:39.960 --> 00:09:42.710 align:start position:0% Russian dolls you you nest you you know it's<00:09:40.110> like<00:09:40.230> the<00:09:40.650> the<00:09:41.130> the<00:09:41.490> the<00:09:41.910> tree<00:09:42.360> inside 00:09:42.710 --> 00:09:42.720 align:start position:0% it's like the the the the tree inside 00:09:42.720 --> 00:09:44.990 align:start position:0% it's like the the the the tree inside the<00:09:42.900> leaf<00:09:43.110> and<00:09:43.440> the<00:09:43.800> leaf<00:09:44.010> inside<00:09:44.460> that<00:09:44.670> tree 00:09:44.990 --> 00:09:45.000 align:start position:0% the leaf and the leaf inside that tree 00:09:45.000 --> 00:09:46.520 align:start position:0% the leaf and the leaf inside that tree and<00:09:45.270> the<00:09:45.390> tree<00:09:45.570> inside<00:09:45.870> the<00:09:46.020> leaf<00:09:46.200> right<00:09:46.410> so 00:09:46.520 --> 00:09:46.530 align:start position:0% and the tree inside the leaf right so 00:09:46.530 --> 00:09:48.920 align:start position:0% and the tree inside the leaf right so it's<00:09:46.650> about<00:09:46.800> nesting<00:09:47.340> and<00:09:47.520> and<00:09:48.240> what<00:09:48.570> what 00:09:48.920 --> 00:09:48.930 align:start position:0% it's about nesting and and what what 00:09:48.930 --> 00:09:51.380 align:start position:0% it's about nesting and and what what monads<00:09:49.290> and<00:09:49.500> Co<00:09:49.860> monads<00:09:50.250> give<00:09:50.460> you<00:09:50.610> monads 00:09:51.380 --> 00:09:51.390 align:start position:0% monads and Co monads give you monads 00:09:51.390 --> 00:09:53.480 align:start position:0% monads and Co monads give you monads give<00:09:51.600> you<00:09:51.660> a<00:09:51.720> way<00:09:51.840> to<00:09:51.900> zoom<00:09:52.230> out<00:09:52.500> and<00:09:52.890> comb 00:09:53.480 --> 00:09:53.490 align:start position:0% give you a way to zoom out and comb 00:09:53.490 --> 00:09:55.580 align:start position:0% give you a way to zoom out and comb monads<00:09:53.850> give<00:09:54.060> you<00:09:54.120> a<00:09:54.180> way<00:09:54.270> to<00:09:54.300> zoom<00:09:54.660> in<00:09:54.900> on<00:09:55.140> this 00:09:55.580 --> 00:09:55.590 align:start position:0% monads give you a way to zoom in on this 00:09:55.590 --> 00:09:57.770 align:start position:0% monads give you a way to zoom in on this nesting<00:09:56.190> phenomena<00:09:56.790> or<00:09:56.940> this<00:09:57.090> composing 00:09:57.770 --> 00:09:57.780 align:start position:0% nesting phenomena or this composing 00:09:57.780 --> 00:10:01.310 align:start position:0% nesting phenomena or this composing phenomenon<00:09:58.700> and<00:09:59.810> lest<00:10:00.810> you<00:10:00.930> think<00:10:01.200> I'm 00:10:01.310 --> 00:10:01.320 align:start position:0% phenomenon and lest you think I'm 00:10:01.320 --> 00:10:04.030 align:start position:0% phenomenon and lest you think I'm talking<00:10:01.680> about<00:10:01.920> abstract<00:10:02.280> airy-fairy<00:10:02.760> stuff 00:10:04.030 --> 00:10:04.040 align:start position:0% talking about abstract airy-fairy stuff 00:10:04.040 --> 00:10:06.800 align:start position:0% talking about abstract airy-fairy stuff again<00:10:05.040> I'm<00:10:05.280> sure<00:10:05.430> all<00:10:05.640> I<00:10:05.730> can<00:10:06.000> do<00:10:06.180> in<00:10:06.390> 25 00:10:06.800 --> 00:10:06.810 align:start position:0% again I'm sure all I can do in 25 00:10:06.810 --> 00:10:08.000 align:start position:0% again I'm sure all I can do in 25 minutes<00:10:06.990> is<00:10:07.170> give<00:10:07.320> you<00:10:07.440> a<00:10:07.470> few<00:10:07.530> impressions 00:10:08.000 --> 00:10:08.010 align:start position:0% minutes is give you a few impressions 00:10:08.010 --> 00:10:13.690 align:start position:0% minutes is give you a few impressions right<00:10:08.490> so<00:10:08.910> so<00:10:09.330> here<00:10:09.900> are<00:10:10.110> effective<00:10:12.560> api's 00:10:13.690 --> 00:10:13.700 align:start position:0% right so so here are effective api's 00:10:13.700 --> 00:10:16.100 align:start position:0% right so so here are effective api's expressed<00:10:14.700> in<00:10:14.880> the<00:10:14.940> language<00:10:15.060> Scala<00:10:15.630> you<00:10:15.960> can 00:10:16.100 --> 00:10:16.110 align:start position:0% expressed in the language Scala you can 00:10:16.110 --> 00:10:18.110 align:start position:0% expressed in the language Scala you can find<00:10:16.380> similar<00:10:16.860> expressions<00:10:17.820> in<00:10:18.030> the<00:10:18.090> language 00:10:18.110 --> 00:10:18.120 align:start position:0% find similar expressions in the language 00:10:18.120 --> 00:10:20.180 align:start position:0% find similar expressions in the language Haskell<00:10:18.870> just<00:10:19.080> out<00:10:19.170> of<00:10:19.200> curiosity<00:10:19.560> how<00:10:20.100> many 00:10:20.180 --> 00:10:20.190 align:start position:0% Haskell just out of curiosity how many 00:10:20.190 --> 00:10:23.590 align:start position:0% Haskell just out of curiosity how many people<00:10:20.340> code<00:10:21.270> in<00:10:21.480> functional<00:10:21.930> languages<00:10:22.400> here 00:10:23.590 --> 00:10:23.600 align:start position:0% people code in functional languages here 00:10:23.600 --> 00:10:26.330 align:start position:0% people code in functional languages here awesome<00:10:24.630> how<00:10:24.930> many<00:10:25.080> people<00:10:25.380> use<00:10:25.620> monads<00:10:26.100> in 00:10:26.330 --> 00:10:26.340 align:start position:0% awesome how many people use monads in 00:10:26.340 --> 00:10:29.390 align:start position:0% awesome how many people use monads in their<00:10:26.520> daily<00:10:26.820> practice<00:10:27.290> you<00:10:28.290> know<00:10:28.380> quite<00:10:29.370> a 00:10:29.390 --> 00:10:29.400 align:start position:0% their daily practice you know quite a 00:10:29.400 --> 00:10:32.310 align:start position:0% their daily practice you know quite a few<00:10:30.030> less<00:10:30.510> yeah<00:10:30.930> okay 00:10:32.310 --> 00:10:32.320 align:start position:0% few less yeah okay 00:10:32.320 --> 00:10:35.100 align:start position:0% few less yeah okay but<00:10:33.190> but<00:10:33.370> the<00:10:33.670> point<00:10:34.210> is<00:10:34.480> that<00:10:34.660> they<00:10:34.750> are<00:10:34.960> an 00:10:35.100 --> 00:10:35.110 align:start position:0% but but the point is that they are an 00:10:35.110 --> 00:10:36.900 align:start position:0% but but the point is that they are an effective<00:10:35.230> notion<00:10:35.980> and<00:10:36.160> they're<00:10:36.280> a<00:10:36.310> great<00:10:36.730> way 00:10:36.900 --> 00:10:36.910 align:start position:0% effective notion and they're a great way 00:10:36.910 --> 00:10:38.760 align:start position:0% effective notion and they're a great way to<00:10:36.940> structure<00:10:37.360> a<00:10:37.570> code<00:10:37.870> even<00:10:38.320> if<00:10:38.530> you're<00:10:38.650> not 00:10:38.760 --> 00:10:38.770 align:start position:0% to structure a code even if you're not 00:10:38.770 --> 00:10:41.760 align:start position:0% to structure a code even if you're not thinking<00:10:39.160> about<00:10:40.080> scaling<00:10:41.080> blockchains 00:10:41.760 --> 00:10:41.770 align:start position:0% thinking about scaling blockchains 00:10:41.770 --> 00:10:43.260 align:start position:0% thinking about scaling blockchains they're<00:10:42.250> they're<00:10:42.490> a<00:10:42.520> great<00:10:42.670> way<00:10:42.730> to<00:10:42.880> structure 00:10:43.260 --> 00:10:43.270 align:start position:0% they're they're a great way to structure 00:10:43.270 --> 00:10:45.060 align:start position:0% they're they're a great way to structure container<00:10:43.870> code<00:10:44.200> they're<00:10:44.500> a<00:10:44.530> great<00:10:44.770> rate<00:10:44.980> of 00:10:45.060 --> 00:10:45.070 align:start position:0% container code they're a great rate of 00:10:45.070 --> 00:10:47.480 align:start position:0% container code they're a great rate of constructor<00:10:45.580> to<00:10:46.270> structure<00:10:46.750> control<00:10:47.140> flow 00:10:47.480 --> 00:10:47.490 align:start position:0% constructor to structure control flow 00:10:47.490 --> 00:10:49.770 align:start position:0% constructor to structure control flow but<00:10:48.490> it<00:10:48.580> turns<00:10:48.790> out<00:10:49.030> that<00:10:49.210> that<00:10:49.330> we<00:10:49.480> can<00:10:49.630> do 00:10:49.770 --> 00:10:49.780 align:start position:0% but it turns out that that we can do 00:10:49.780 --> 00:10:50.990 align:start position:0% but it turns out that that we can do better<00:10:49.990> than<00:10:50.260> that 00:10:50.990 --> 00:10:51.000 align:start position:0% better than that 00:10:51.000 --> 00:10:55.730 align:start position:0% better than that so<00:10:52.000> in<00:10:52.330> particular<00:10:52.510> Special<00:10:53.410> K<00:10:53.820> kbdb 00:10:55.730 --> 00:10:55.740 align:start position:0% so in particular Special K kbdb 00:10:55.740 --> 00:10:59.820 align:start position:0% so in particular Special K kbdb looks<00:10:56.740> at<00:10:56.980> a<00:10:57.010> duality<00:10:57.480> between<00:10:58.830> continuation 00:10:59.820 --> 00:10:59.830 align:start position:0% looks at a duality between continuation 00:10:59.830 --> 00:11:01.770 align:start position:0% looks at a duality between continuation which<00:11:00.070> is<00:11:00.280> the<00:11:00.550> rest<00:11:00.820> of<00:11:01.000> your<00:11:01.120> program<00:11:01.540> so 00:11:01.770 --> 00:11:01.780 align:start position:0% which is the rest of your program so 00:11:01.780 --> 00:11:03.180 align:start position:0% which is the rest of your program so let's<00:11:01.810> say<00:11:02.050> your<00:11:02.200> program<00:11:02.560> walks<00:11:02.830> up<00:11:02.980> to<00:11:03.010> the 00:11:03.180 --> 00:11:03.190 align:start position:0% let's say your program walks up to the 00:11:03.190 --> 00:11:04.440 align:start position:0% let's say your program walks up to the block<00:11:03.400> tier<00:11:03.580> and<00:11:03.640> says<00:11:03.790> I'm<00:11:03.910> looking<00:11:04.270> for 00:11:04.440 --> 00:11:04.450 align:start position:0% block tier and says I'm looking for 00:11:04.450 --> 00:11:06.000 align:start position:0% block tier and says I'm looking for something<00:11:04.660> right<00:11:05.500> and<00:11:05.710> what<00:11:05.830> if<00:11:05.920> that 00:11:06.000 --> 00:11:06.010 align:start position:0% something right and what if that 00:11:06.010 --> 00:11:08.400 align:start position:0% something right and what if that something<00:11:06.430> isn't<00:11:06.610> there<00:11:07.000> yet<00:11:07.300> what<00:11:08.050> do<00:11:08.110> you<00:11:08.200> do 00:11:08.400 --> 00:11:08.410 align:start position:0% something isn't there yet what do you do 00:11:08.410 --> 00:11:10.650 align:start position:0% something isn't there yet what do you do with<00:11:08.590> that<00:11:08.620> program<00:11:08.980> that<00:11:09.640> is<00:11:10.150> waiting<00:11:10.630> for 00:11:10.650 --> 00:11:10.660 align:start position:0% with that program that is waiting for 00:11:10.660 --> 00:11:13.140 align:start position:0% with that program that is waiting for data<00:11:10.960> and<00:11:11.140> can't<00:11:11.320> go<00:11:11.440> further<00:11:11.710> right<00:11:12.100> so<00:11:13.000> in 00:11:13.140 --> 00:11:13.150 align:start position:0% data and can't go further right so in 00:11:13.150 --> 00:11:15.210 align:start position:0% data and can't go further right so in Special<00:11:13.570> K<00:11:13.750> what<00:11:13.990> happens<00:11:14.440> is<00:11:14.650> the<00:11:14.860> rest<00:11:15.100> of 00:11:15.210 --> 00:11:15.220 align:start position:0% Special K what happens is the rest of 00:11:15.220 --> 00:11:17.910 align:start position:0% Special K what happens is the rest of that<00:11:15.370> program<00:11:15.880> is<00:11:16.140> packaged<00:11:17.140> up<00:11:17.410> as<00:11:17.620> a<00:11:17.650> piece 00:11:17.910 --> 00:11:17.920 align:start position:0% that program is packaged up as a piece 00:11:17.920 --> 00:11:20.820 align:start position:0% that program is packaged up as a piece of<00:11:18.070> data<00:11:18.220> and<00:11:18.580> stored<00:11:19.050> at<00:11:20.050> the<00:11:20.170> place<00:11:20.590> where 00:11:20.820 --> 00:11:20.830 align:start position:0% of data and stored at the place where 00:11:20.830 --> 00:11:22.310 align:start position:0% of data and stored at the place where you<00:11:20.980> were<00:11:21.220> it<00:11:21.370> was<00:11:21.460> looking<00:11:21.880> for<00:11:21.940> something 00:11:22.310 --> 00:11:22.320 align:start position:0% you were it was looking for something 00:11:22.320 --> 00:11:24.960 align:start position:0% you were it was looking for something right<00:11:23.320> so<00:11:23.500> that's<00:11:23.620> the<00:11:23.860> continuation<00:11:24.370> and 00:11:24.960 --> 00:11:24.970 align:start position:0% right so that's the continuation and 00:11:24.970 --> 00:11:27.570 align:start position:0% right so that's the continuation and then<00:11:25.480> data<00:11:25.720> is<00:11:25.990> dual<00:11:26.230> to<00:11:26.440> that<00:11:26.650> and<00:11:27.220> in<00:11:27.370> fact 00:11:27.570 --> 00:11:27.580 align:start position:0% then data is dual to that and in fact 00:11:27.580 --> 00:11:29.220 align:start position:0% then data is dual to that and in fact you<00:11:27.670> can<00:11:27.820> have<00:11:27.940> a<00:11:28.000> notion<00:11:28.360> of<00:11:28.690> data<00:11:28.870> integrity 00:11:29.220 --> 00:11:29.230 align:start position:0% you can have a notion of data integrity 00:11:29.230 --> 00:11:32.460 align:start position:0% you can have a notion of data integrity that<00:11:30.010> that<00:11:30.760> goes<00:11:31.150> all<00:11:31.510> the<00:11:31.540> way<00:11:31.750> back<00:11:31.870> to<00:11:32.350> the 00:11:32.460 --> 00:11:32.470 align:start position:0% that that goes all the way back to the 00:11:32.470 --> 00:11:34.580 align:start position:0% that that goes all the way back to the law<00:11:32.650> of<00:11:32.680> excluded<00:11:33.070> middle<00:11:33.400> right<00:11:33.910> a<00:11:33.940> or<00:11:34.270> not<00:11:34.450> a 00:11:34.580 --> 00:11:34.590 align:start position:0% law of excluded middle right a or not a 00:11:34.590 --> 00:11:38.550 align:start position:0% law of excluded middle right a or not a right<00:11:35.590> that<00:11:35.920> has<00:11:35.980> to<00:11:36.520> do<00:11:36.730> with<00:11:37.320> this<00:11:38.320> duality 00:11:38.550 --> 00:11:38.560 align:start position:0% right that has to do with this duality 00:11:38.560 --> 00:11:41.130 align:start position:0% right that has to do with this duality between<00:11:39.100> continuation<00:11:39.970> and<00:11:40.090> data<00:11:40.270> so<00:11:40.630> at<00:11:40.900> this 00:11:41.130 --> 00:11:41.140 align:start position:0% between continuation and data so at this 00:11:41.140 --> 00:11:42.810 align:start position:0% between continuation and data so at this location<00:11:41.350> that<00:11:41.950> you're<00:11:42.070> looking<00:11:42.370> for<00:11:42.550> this 00:11:42.810 --> 00:11:42.820 align:start position:0% location that you're looking for this 00:11:42.820 --> 00:11:44.910 align:start position:0% location that you're looking for this address<00:11:43.090> on<00:11:43.510> the<00:11:43.600> blockchain<00:11:43.810> or<00:11:44.560> in<00:11:44.650> the<00:11:44.740> case 00:11:44.910 --> 00:11:44.920 align:start position:0% address on the blockchain or in the case 00:11:44.920 --> 00:11:46.620 align:start position:0% address on the blockchain or in the case of<00:11:45.070> Special<00:11:45.430> K<00:11:45.580> it's<00:11:45.730> a<00:11:45.850> it's<00:11:46.270> a<00:11:46.450> more 00:11:46.620 --> 00:11:46.630 align:start position:0% of Special K it's a it's a more 00:11:46.630 --> 00:11:48.810 align:start position:0% of Special K it's a it's a more sophisticated<00:11:47.260> kind<00:11:47.440> of<00:11:47.740> key<00:11:47.980> but<00:11:48.490> if<00:11:48.610> it's 00:11:48.810 --> 00:11:48.820 align:start position:0% sophisticated kind of key but if it's 00:11:48.820 --> 00:11:51.960 align:start position:0% sophisticated kind of key but if it's location<00:11:49.680> you<00:11:50.680> will<00:11:50.800> either<00:11:51.070> have<00:11:51.280> a 00:11:51.960 --> 00:11:51.970 align:start position:0% location you will either have a 00:11:51.970 --> 00:11:55.800 align:start position:0% location you will either have a continuation<00:11:52.810> or<00:11:53.350> some<00:11:53.860> data<00:11:54.040> and<00:11:54.490> if<00:11:55.360> if<00:11:55.630> a 00:11:55.800 --> 00:11:55.810 align:start position:0% continuation or some data and if if a 00:11:55.810 --> 00:11:58.080 align:start position:0% continuation or some data and if if a program<00:11:56.200> is<00:11:56.380> looking<00:11:56.500> for<00:11:56.860> for<00:11:57.490> data<00:11:57.670> and<00:11:57.970> it's 00:11:58.080 --> 00:11:58.090 align:start position:0% program is looking for for data and it's 00:11:58.090 --> 00:11:59.970 align:start position:0% program is looking for for data and it's not<00:11:58.240> there<00:11:58.450> the<00:11:58.600> continuation<00:11:59.050> will<00:11:59.860> be 00:11:59.970 --> 00:11:59.980 align:start position:0% not there the continuation will be 00:11:59.980 --> 00:12:02.460 align:start position:0% not there the continuation will be stored<00:12:00.310> there<00:12:00.400> if<00:12:00.790> a<00:12:01.270> program<00:12:01.630> is<00:12:01.780> depositing 00:12:02.460 --> 00:12:02.470 align:start position:0% stored there if a program is depositing 00:12:02.470 --> 00:12:04.230 align:start position:0% stored there if a program is depositing data<00:12:02.680> if<00:12:02.920> there<00:12:03.070> is<00:12:03.220> a<00:12:03.250> continuation<00:12:03.700> there 00:12:04.230 --> 00:12:04.240 align:start position:0% data if there is a continuation there 00:12:04.240 --> 00:12:06.180 align:start position:0% data if there is a continuation there that<00:12:04.690> continuation<00:12:05.170> will<00:12:05.470> be<00:12:05.590> woken<00:12:05.920> up<00:12:06.040> and 00:12:06.180 --> 00:12:06.190 align:start position:0% that continuation will be woken up and 00:12:06.190 --> 00:12:08.610 align:start position:0% that continuation will be woken up and handed<00:12:06.520> the<00:12:06.610> data<00:12:06.820> okay<00:12:07.630> that's<00:12:07.810> the<00:12:07.990> basic 00:12:08.610 --> 00:12:08.620 align:start position:0% handed the data okay that's the basic 00:12:08.620 --> 00:12:11.610 align:start position:0% handed the data okay that's the basic set<00:12:08.890> up<00:12:09.040> right<00:12:09.910> now<00:12:10.180> you<00:12:10.480> can<00:12:10.870> ask<00:12:11.140> some 00:12:11.610 --> 00:12:11.620 align:start position:0% set up right now you can ask some 00:12:11.620 --> 00:12:13.860 align:start position:0% set up right now you can ask some questions<00:12:12.190> about<00:12:12.490> that<00:12:12.700> set<00:12:12.970> up<00:12:13.120> you<00:12:13.360> can<00:12:13.570> say 00:12:13.860 --> 00:12:13.870 align:start position:0% questions about that set up you can say 00:12:13.870 --> 00:12:18.210 align:start position:0% questions about that set up you can say well<00:12:15.150> after<00:12:16.150> the<00:12:16.720> data<00:12:16.990> and<00:12:17.380> the<00:12:17.500> program<00:12:18.010> the 00:12:18.210 --> 00:12:18.220 align:start position:0% well after the data and the program the 00:12:18.220 --> 00:12:20.640 align:start position:0% well after the data and the program the continuation<00:12:18.640> meet<00:12:19.420> each<00:12:19.600> other<00:12:19.900> what 00:12:20.640 --> 00:12:20.650 align:start position:0% continuation meet each other what 00:12:20.650 --> 00:12:23.520 align:start position:0% continuation meet each other what happens<00:12:21.100> and<00:12:21.690> there<00:12:22.690> are<00:12:22.810> there<00:12:23.050> are<00:12:23.080> only<00:12:23.380> a 00:12:23.520 --> 00:12:23.530 align:start position:0% happens and there are there are only a 00:12:23.530 --> 00:12:27.230 align:start position:0% happens and there are there are only a handful<00:12:24.010> of<00:12:24.130> possibilities<00:12:24.790> one<00:12:25.660> is<00:12:25.900> the<00:12:26.680> data 00:12:27.230 --> 00:12:27.240 align:start position:0% handful of possibilities one is the data 00:12:27.240 --> 00:12:29.820 align:start position:0% handful of possibilities one is the data disappears<00:12:28.330> and<00:12:28.540> the<00:12:29.380> continuation 00:12:29.820 --> 00:12:29.830 align:start position:0% disappears and the continuation 00:12:29.830 --> 00:12:32.280 align:start position:0% disappears and the continuation disappears<00:12:30.730> so<00:12:31.090> they<00:12:31.540> meet<00:12:31.810> each<00:12:31.840> other<00:12:32.200> in 00:12:32.280 --> 00:12:32.290 align:start position:0% disappears so they meet each other in 00:12:32.290 --> 00:12:34.590 align:start position:0% disappears so they meet each other in this<00:12:32.530> abstract<00:12:33.160> space<00:12:33.490> this<00:12:33.820> this<00:12:34.090> address 00:12:34.590 --> 00:12:34.600 align:start position:0% this abstract space this this address 00:12:34.600 --> 00:12:37.500 align:start position:0% this abstract space this this address and<00:12:34.840> they<00:12:35.410> go<00:12:35.560> poof<00:12:35.940> all<00:12:36.940> right<00:12:37.090> another 00:12:37.500 --> 00:12:37.510 align:start position:0% and they go poof all right another 00:12:37.510 --> 00:12:39.900 align:start position:0% and they go poof all right another possibility<00:12:38.110> is<00:12:38.470> that<00:12:38.800> the<00:12:39.310> continuation 00:12:39.900 --> 00:12:39.910 align:start position:0% possibility is that the continuation 00:12:39.910 --> 00:12:42.660 align:start position:0% possibility is that the continuation remains<00:12:40.510> and<00:12:40.750> the<00:12:40.810> data<00:12:40.990> goes<00:12:41.230> poof<00:12:41.670> another 00:12:42.660 --> 00:12:42.670 align:start position:0% remains and the data goes poof another 00:12:42.670 --> 00:12:44.610 align:start position:0% remains and the data goes poof another possibility<00:12:43.180> is<00:12:43.390> that<00:12:43.510> the<00:12:43.870> continuation 00:12:44.610 --> 00:12:44.620 align:start position:0% possibility is that the continuation 00:12:44.620 --> 00:12:45.480 align:start position:0% possibility is that the continuation goes<00:12:45.040> poof 00:12:45.480 --> 00:12:45.490 align:start position:0% goes poof 00:12:45.490 --> 00:12:47.220 align:start position:0% goes poof the<00:12:45.610> data<00:12:45.790> remains<00:12:46.029> and<00:12:46.540> the<00:12:47.020> last 00:12:47.220 --> 00:12:47.230 align:start position:0% the data remains and the last 00:12:47.230 --> 00:12:49.170 align:start position:0% the data remains and the last possibility<00:12:47.860> of<00:12:47.950> course<00:12:48.220> is<00:12:48.490> that<00:12:48.730> they<00:12:48.880> they 00:12:49.170 --> 00:12:49.180 align:start position:0% possibility of course is that they they 00:12:49.180 --> 00:12:52.380 align:start position:0% possibility of course is that they they both<00:12:49.360> persist<00:12:49.899> right<00:12:50.800> so<00:12:51.100> so<00:12:51.520> what<00:12:51.940> is<00:12:52.060> what 00:12:52.380 --> 00:12:52.390 align:start position:0% both persist right so so what is what 00:12:52.390 --> 00:12:58.400 align:start position:0% both persist right so so what is what does<00:12:52.480> that<00:12:52.540> have<00:12:52.899> to<00:12:52.959> do<00:12:53.290> with<00:12:56.430> traditional 00:12:58.400 --> 00:12:58.410 align:start position:0% does that have to do with traditional 00:12:58.410 --> 00:13:00.930 align:start position:0% does that have to do with traditional approaches<00:12:59.410> to<00:12:59.440> distributed<00:13:00.310> applications 00:13:00.930 --> 00:13:00.940 align:start position:0% approaches to distributed applications 00:13:00.940 --> 00:13:04.050 align:start position:0% approaches to distributed applications well<00:13:01.660> if<00:13:01.779> it<00:13:01.899> well<00:13:02.260> if<00:13:02.560> the<00:13:02.830> data<00:13:03.100> persists<00:13:03.880> and 00:13:04.050 --> 00:13:04.060 align:start position:0% well if it well if the data persists and 00:13:04.060 --> 00:13:05.820 align:start position:0% well if it well if the data persists and the<00:13:04.240> continuation<00:13:04.720> evaporates 00:13:05.820 --> 00:13:05.830 align:start position:0% the continuation evaporates 00:13:05.830 --> 00:13:07.889 align:start position:0% the continuation evaporates that's<00:13:06.279> just<00:13:06.640> traditional<00:13:07.089> deep<00:13:07.270> database 00:13:07.889 --> 00:13:07.899 align:start position:0% that's just traditional deep database 00:13:07.899 --> 00:13:11.250 align:start position:0% that's just traditional deep database operations<00:13:08.500> think<00:13:09.190> about<00:13:09.430> a<00:13:09.459> read/write<00:13:10.260> my 00:13:11.250 --> 00:13:11.260 align:start position:0% operations think about a read/write my 00:13:11.260 --> 00:13:13.170 align:start position:0% operations think about a read/write my program<00:13:11.649> once<00:13:11.890> the<00:13:12.070> data<00:13:12.250> I<00:13:12.490> read<00:13:12.790> it<00:13:12.910> but<00:13:13.120> I 00:13:13.170 --> 00:13:13.180 align:start position:0% program once the data I read it but I 00:13:13.180 --> 00:13:14.490 align:start position:0% program once the data I read it but I don't<00:13:13.450> get<00:13:13.600> rid<00:13:13.750> of<00:13:13.779> it<00:13:13.959> out<00:13:14.050> of<00:13:14.080> the<00:13:14.230> database 00:13:14.490 --> 00:13:14.500 align:start position:0% don't get rid of it out of the database 00:13:14.500 --> 00:13:16.620 align:start position:0% don't get rid of it out of the database just<00:13:14.860> from<00:13:15.070> the<00:13:15.160> read<00:13:15.279> operation<00:13:15.630> right 00:13:16.620 --> 00:13:16.630 align:start position:0% just from the read operation right 00:13:16.630 --> 00:13:18.300 align:start position:0% just from the read operation right that's<00:13:17.080> that's<00:13:17.410> traditional<00:13:17.980> database 00:13:18.300 --> 00:13:18.310 align:start position:0% that's that's traditional database 00:13:18.310 --> 00:13:24.600 align:start position:0% that's that's traditional database operations<00:13:19.020> if<00:13:20.020> I<00:13:21.149> publish<00:13:22.149> and<00:13:22.510> and<00:13:23.080> and<00:13:24.040> the 00:13:24.600 --> 00:13:24.610 align:start position:0% operations if I publish and and and the 00:13:24.610 --> 00:13:27.180 align:start position:0% operations if I publish and and and the the<00:13:24.910> the<00:13:25.300> publishing<00:13:25.870> data<00:13:26.080> is<00:13:26.320> ephemeral<00:13:26.709> but 00:13:27.180 --> 00:13:27.190 align:start position:0% the the publishing data is ephemeral but 00:13:27.190 --> 00:13:29.579 align:start position:0% the the publishing data is ephemeral but the<00:13:27.670> continuation<00:13:28.089> persists<00:13:28.990> that's 00:13:29.579 --> 00:13:29.589 align:start position:0% the continuation persists that's 00:13:29.589 --> 00:13:31.850 align:start position:0% the continuation persists that's ordinary<00:13:30.130> published<00:13:30.790> and<00:13:30.940> subscribed 00:13:31.850 --> 00:13:31.860 align:start position:0% ordinary published and subscribed 00:13:31.860 --> 00:13:34.139 align:start position:0% ordinary published and subscribed that's<00:13:32.860> ordinary<00:13:33.190> publish<00:13:33.610> and<00:13:33.760> subscribing 00:13:34.139 --> 00:13:34.149 align:start position:0% that's ordinary publish and subscribing 00:13:34.149 --> 00:13:36.600 align:start position:0% that's ordinary publish and subscribing if<00:13:34.360> they<00:13:34.480> if<00:13:34.959> both<00:13:35.290> of<00:13:35.320> them<00:13:35.589> persist<00:13:35.980> its 00:13:36.600 --> 00:13:36.610 align:start position:0% if they if both of them persist its 00:13:36.610 --> 00:13:38.760 align:start position:0% if they if both of them persist its published<00:13:37.149> and<00:13:37.300> subscribe<00:13:37.779> with<00:13:38.290> a<00:13:38.320> history 00:13:38.760 --> 00:13:38.770 align:start position:0% published and subscribe with a history 00:13:38.770 --> 00:13:42.769 align:start position:0% published and subscribe with a history with<00:13:39.220> a<00:13:39.250> backlog<00:13:39.850> of<00:13:40.060> what<00:13:40.660> you<00:13:40.779> published<00:13:41.230> and 00:13:42.769 --> 00:13:42.779 align:start position:0% with a backlog of what you published and 00:13:42.779 --> 00:13:45.120 align:start position:0% with a backlog of what you published and finally<00:13:43.779> this<00:13:44.020> is<00:13:44.080> quite<00:13:44.410> interesting<00:13:44.980> if 00:13:45.120 --> 00:13:45.130 align:start position:0% finally this is quite interesting if 00:13:45.130 --> 00:13:48.510 align:start position:0% finally this is quite interesting if they<00:13:45.310> if<00:13:45.550> they<00:13:45.760> both<00:13:46.080> disappear<00:13:47.160> then<00:13:48.160> you<00:13:48.190> get 00:13:48.510 --> 00:13:48.520 align:start position:0% they if they both disappear then you get 00:13:48.520 --> 00:13:51.360 align:start position:0% they if they both disappear then you get item<00:13:49.000> level<00:13:49.360> locking<00:13:49.810> in<00:13:50.290> a<00:13:50.920> distributed 00:13:51.360 --> 00:13:51.370 align:start position:0% item level locking in a distributed 00:13:51.370 --> 00:13:56.760 align:start position:0% item level locking in a distributed transactional<00:13:52.329> semantics<00:13:52.870> so<00:13:53.880> one<00:13:54.880> API<00:13:55.770> which 00:13:56.760 --> 00:13:56.770 align:start position:0% transactional semantics so one API which 00:13:56.770 --> 00:14:02.130 align:start position:0% transactional semantics so one API which I<00:13:57.959> showed<00:13:58.959> you<00:13:59.160> nothing<00:14:00.160> up<00:14:00.250> my<00:14:00.279> sleeves<00:14:01.140> right 00:14:02.130 --> 00:14:02.140 align:start position:0% I showed you nothing up my sleeves right 00:14:02.140 --> 00:14:06.960 align:start position:0% I showed you nothing up my sleeves right one<00:14:02.680> API<00:14:03.180> the<00:14:04.180> the<00:14:04.450> monadic<00:14:04.779> api<00:14:05.200> covers<00:14:05.980> all 00:14:06.960 --> 00:14:06.970 align:start position:0% one API the the monadic api covers all 00:14:06.970 --> 00:14:10.740 align:start position:0% one API the the monadic api covers all of<00:14:07.510> those<00:14:08.200> distributed<00:14:09.750> programming 00:14:10.740 --> 00:14:10.750 align:start position:0% of those distributed programming 00:14:10.750 --> 00:14:15.540 align:start position:0% of those distributed programming paradigms<00:14:12.089> so<00:14:13.410> now<00:14:14.410> how<00:14:14.920> does<00:14:14.980> this<00:14:15.160> apply<00:14:15.430> to 00:14:15.540 --> 00:14:15.550 align:start position:0% paradigms so now how does this apply to 00:14:15.550 --> 00:14:20.430 align:start position:0% paradigms so now how does this apply to the<00:14:15.760> blockchain<00:14:17.670> well<00:14:18.670> that<00:14:18.850> that<00:14:19.149> that<00:14:19.480> how 00:14:20.430 --> 00:14:20.440 align:start position:0% the blockchain well that that that how 00:14:20.440 --> 00:14:22.650 align:start position:0% the blockchain well that that that how we<00:14:20.500> provide<00:14:21.279> that<00:14:21.550> is<00:14:21.820> that<00:14:22.029> the<00:14:22.149> continuation 00:14:22.650 --> 00:14:22.660 align:start position:0% we provide that is that the continuation 00:14:22.660 --> 00:14:25.800 align:start position:0% we provide that is that the continuation monad<00:14:23.020> is<00:14:23.620> the<00:14:24.220> is<00:14:24.430> the<00:14:24.640> monad<00:14:25.089> underlying 00:14:25.800 --> 00:14:25.810 align:start position:0% monad is the is the monad underlying 00:14:25.810 --> 00:14:28.319 align:start position:0% monad is the is the monad underlying being<00:14:26.470> able<00:14:26.620> to<00:14:26.770> bring<00:14:27.160> those<00:14:27.339> those<00:14:27.790> patterns 00:14:28.319 --> 00:14:28.329 align:start position:0% being able to bring those those patterns 00:14:28.329 --> 00:14:30.449 align:start position:0% being able to bring those those patterns together<00:14:28.540> right<00:14:29.500> so<00:14:29.649> we<00:14:29.770> talked<00:14:30.010> about<00:14:30.160> this 00:14:30.449 --> 00:14:30.459 align:start position:0% together right so we talked about this 00:14:30.459 --> 00:14:32.760 align:start position:0% together right so we talked about this duality<00:14:31.029> between<00:14:31.440> continuation<00:14:32.440> and<00:14:32.560> data 00:14:32.760 --> 00:14:32.770 align:start position:0% duality between continuation and data 00:14:32.770 --> 00:14:35.100 align:start position:0% duality between continuation and data well<00:14:33.399> it's<00:14:33.550> the<00:14:33.670> it's<00:14:34.120> the<00:14:34.270> structuring<00:14:34.839> of 00:14:35.100 --> 00:14:35.110 align:start position:0% well it's the it's the structuring of 00:14:35.110 --> 00:14:37.050 align:start position:0% well it's the it's the structuring of the<00:14:35.370> continuations<00:14:36.370> and<00:14:36.490> the<00:14:36.550> way<00:14:36.640> we<00:14:36.820> store 00:14:37.050 --> 00:14:37.060 align:start position:0% the continuations and the way we store 00:14:37.060 --> 00:14:40.440 align:start position:0% the continuations and the way we store them<00:14:37.360> that<00:14:37.720> uses<00:14:38.320> the<00:14:38.470> continuation<00:14:38.890> monad<00:14:39.450> to 00:14:40.440 --> 00:14:40.450 align:start position:0% them that uses the continuation monad to 00:14:40.450 --> 00:14:42.600 align:start position:0% them that uses the continuation monad to provide<00:14:40.810> to<00:14:41.290> provide<00:14:41.589> that<00:14:41.740> unification<00:14:42.490> of 00:14:42.600 --> 00:14:42.610 align:start position:0% provide to provide that unification of 00:14:42.610 --> 00:14:45.680 align:start position:0% provide to provide that unification of all<00:14:42.730> those<00:14:42.910> programming<00:14:43.390> paradigms<00:14:43.810> and<00:14:44.079> and 00:14:45.680 --> 00:14:45.690 align:start position:0% all those programming paradigms and and 00:14:45.690 --> 00:14:48.600 align:start position:0% all those programming paradigms and and so<00:14:46.690> we<00:14:46.810> looked<00:14:47.079> at<00:14:47.170> that<00:14:47.290> API<00:14:47.620> it<00:14:48.040> turns<00:14:48.339> out 00:14:48.600 --> 00:14:48.610 align:start position:0% so we looked at that API it turns out 00:14:48.610 --> 00:14:51.690 align:start position:0% so we looked at that API it turns out that<00:14:49.270> if<00:14:49.450> you<00:14:49.570> just<00:14:50.020> tilt<00:14:50.470> that<00:14:50.649> API<00:14:51.070> on<00:14:51.459> its 00:14:51.690 --> 00:14:51.700 align:start position:0% that if you just tilt that API on its 00:14:51.700 --> 00:14:54.000 align:start position:0% that if you just tilt that API on its side<00:14:51.970> a<00:14:52.000> little<00:14:52.540> bit<00:14:52.660> what<00:14:53.560> you<00:14:53.709> end<00:14:53.860> up 00:14:54.000 --> 00:14:54.010 align:start position:0% side a little bit what you end up 00:14:54.010 --> 00:14:56.130 align:start position:0% side a little bit what you end up getting<00:14:54.160> is<00:14:54.520> the<00:14:54.850> applied<00:14:55.120> PI<00:14:55.390> calculus<00:14:55.930> and 00:14:56.130 --> 00:14:56.140 align:start position:0% getting is the applied PI calculus and 00:14:56.140 --> 00:14:58.300 align:start position:0% getting is the applied PI calculus and that's<00:14:56.829> exactly<00:14:57.459> how<00:14:57.579> Special<00:14:58.029> K 00:14:58.300 --> 00:14:58.310 align:start position:0% that's exactly how Special K 00:14:58.310 --> 00:15:00.850 align:start position:0% that's exactly how Special K is<00:14:58.370> organized<00:14:58.880> so<00:14:59.240> if<00:14:59.900> you<00:14:59.990> look<00:15:00.170> at<00:15:00.290> Special<00:15:00.650> K 00:15:00.850 --> 00:15:00.860 align:start position:0% is organized so if you look at Special K 00:15:00.860 --> 00:15:03.040 align:start position:0% is organized so if you look at Special K if<00:15:01.400> you<00:15:01.550> go<00:15:01.670> to<00:15:01.730> github<00:15:01.940> right<00:15:02.420> now<00:15:02.630> and<00:15:02.960> you 00:15:03.040 --> 00:15:03.050 align:start position:0% if you go to github right now and you 00:15:03.050 --> 00:15:04.720 align:start position:0% if you go to github right now and you look<00:15:03.200> at<00:15:03.320> Special<00:15:03.650> K<00:15:03.800> what<00:15:03.980> you'll<00:15:04.130> find<00:15:04.430> is<00:15:04.670> a 00:15:04.720 --> 00:15:04.730 align:start position:0% look at Special K what you'll find is a 00:15:04.730 --> 00:15:08.590 align:start position:0% look at Special K what you'll find is a little<00:15:05.630> DSL<00:15:06.350> that<00:15:07.250> provides<00:15:08.120> an 00:15:08.590 --> 00:15:08.600 align:start position:0% little DSL that provides an 00:15:08.600 --> 00:15:10.330 align:start position:0% little DSL that provides an implementation<00:15:08.870> of<00:15:09.710> the<00:15:09.830> applied<00:15:10.130> PI 00:15:10.330 --> 00:15:10.340 align:start position:0% implementation of the applied PI 00:15:10.340 --> 00:15:14.110 align:start position:0% implementation of the applied PI calculus<00:15:11.050> so<00:15:12.279> but<00:15:13.279> here's<00:15:13.520> a<00:15:13.580> little<00:15:13.880> preview 00:15:14.110 --> 00:15:14.120 align:start position:0% calculus so but here's a little preview 00:15:14.120 --> 00:15:20.610 align:start position:0% calculus so but here's a little preview of<00:15:14.680> applying<00:15:15.680> that<00:15:16.160> API<00:15:16.580> to<00:15:17.089> Casper<00:15:19.240> so<00:15:20.240> I 00:15:20.610 --> 00:15:20.620 align:start position:0% of applying that API to Casper so I 00:15:20.620 --> 00:15:23.350 align:start position:0% of applying that API to Casper so I spent<00:15:21.620> last<00:15:21.800> night<00:15:22.100> and<00:15:22.279> refactored<00:15:22.940> this<00:15:23.120> I 00:15:23.350 --> 00:15:23.360 align:start position:0% spent last night and refactored this I 00:15:23.360 --> 00:15:27.610 align:start position:0% spent last night and refactored this I had<00:15:23.510> good<00:15:23.720> fun<00:15:25.240> so<00:15:26.240> let's<00:15:26.480> see<00:15:26.630> if<00:15:26.750> I<00:15:26.870> can<00:15:27.050> can 00:15:27.610 --> 00:15:27.620 align:start position:0% had good fun so let's see if I can can 00:15:27.620 --> 00:15:29.950 align:start position:0% had good fun so let's see if I can can you<00:15:27.710> see<00:15:27.890> that<00:15:28.330> well<00:15:29.330> that's<00:15:29.450> that's<00:15:29.720> all 00:15:29.950 --> 00:15:29.960 align:start position:0% you see that well that's that's all 00:15:29.960 --> 00:15:31.990 align:start position:0% you see that well that's that's all right<00:15:30.110> so<00:15:30.740> I'm<00:15:30.830> just<00:15:30.860> gonna<00:15:31.100> again<00:15:31.580> I<00:15:31.610> only 00:15:31.990 --> 00:15:32.000 align:start position:0% right so I'm just gonna again I only 00:15:32.000 --> 00:15:40.480 align:start position:0% right so I'm just gonna again I only have<00:15:32.240> time<00:15:32.480> to<00:15:32.630> give<00:15:32.779> you<00:15:32.870> a<00:15:32.930> flavor<00:15:38.950> so<00:15:39.950> here 00:15:40.480 --> 00:15:40.490 align:start position:0% have time to give you a flavor so here 00:15:40.490 --> 00:15:43.540 align:start position:0% have time to give you a flavor so here are<00:15:40.700> the<00:15:41.180> files<00:15:41.600> in<00:15:42.050> the<00:15:42.170> spec<00:15:42.529> and<00:15:43.130> let's<00:15:43.339> take 00:15:43.540 --> 00:15:43.550 align:start position:0% are the files in the spec and let's take 00:15:43.550 --> 00:15:49.900 align:start position:0% are the files in the spec and let's take a<00:15:43.610> look<00:15:43.820> briefly<00:15:44.270> at<00:15:44.510> just<00:15:44.839> some<00:15:45.410> of<00:15:45.560> them<00:15:48.910> so 00:15:49.900 --> 00:15:49.910 align:start position:0% a look briefly at just some of them so 00:15:49.910 --> 00:15:52.780 align:start position:0% a look briefly at just some of them so in<00:15:50.330> in<00:15:50.750> Casper<00:15:51.350> the<00:15:51.560> consensus<00:15:52.100> protocol<00:15:52.610> is 00:15:52.780 --> 00:15:52.790 align:start position:0% in in Casper the consensus protocol is 00:15:52.790 --> 00:15:54.700 align:start position:0% in in Casper the consensus protocol is organized<00:15:53.330> around<00:15:53.510> nodes<00:15:53.900> which<00:15:54.230> we<00:15:54.380> think<00:15:54.529> of 00:15:54.700 --> 00:15:54.710 align:start position:0% organized around nodes which we think of 00:15:54.710 --> 00:15:58.090 align:start position:0% organized around nodes which we think of as<00:15:54.880> validators<00:15:55.880> and<00:15:56.180> what<00:15:57.050> a<00:15:57.080> validator<00:15:57.650> wants 00:15:58.090 --> 00:15:58.100 align:start position:0% as validators and what a validator wants 00:15:58.100 --> 00:16:01.360 align:start position:0% as validators and what a validator wants to<00:15:58.190> do<00:15:58.339> is<00:15:58.490> essentially<00:15:59.200> receive<00:16:00.200> blocks<00:16:00.950> and 00:16:01.360 --> 00:16:01.370 align:start position:0% to do is essentially receive blocks and 00:16:01.370 --> 00:16:04.270 align:start position:0% to do is essentially receive blocks and then<00:16:01.490> make<00:16:01.880> bets<00:16:02.300> on<00:16:02.660> whether<00:16:03.560> or<00:16:03.740> not<00:16:03.800> a<00:16:03.890> block 00:16:04.270 --> 00:16:04.280 align:start position:0% then make bets on whether or not a block 00:16:04.280 --> 00:16:07.870 align:start position:0% then make bets on whether or not a block should<00:16:04.550> be<00:16:04.610> published<00:16:05.120> to<00:16:05.360> the<00:16:05.510> to<00:16:06.050> the<00:16:06.760> to<00:16:07.760> the 00:16:07.870 --> 00:16:07.880 align:start position:0% should be published to the to the to the 00:16:07.880 --> 00:16:10.210 align:start position:0% should be published to the to the to the to<00:16:08.150> the<00:16:08.270> blockchain<00:16:08.750> and<00:16:09.200> here's<00:16:09.710> here's 00:16:10.210 --> 00:16:10.220 align:start position:0% to the blockchain and here's here's 00:16:10.220 --> 00:16:13.030 align:start position:0% to the blockchain and here's here's basically<00:16:10.880> just<00:16:11.270> an<00:16:11.570> applied<00:16:12.170> PI<00:16:12.440> calculus 00:16:13.030 --> 00:16:13.040 align:start position:0% basically just an applied PI calculus 00:16:13.040 --> 00:16:15.700 align:start position:0% basically just an applied PI calculus spec<00:16:13.400> of<00:16:13.670> the<00:16:14.420> bedding<00:16:14.720> and<00:16:15.080> the<00:16:15.440> the 00:16:15.700 --> 00:16:15.710 align:start position:0% spec of the bedding and the the 00:16:15.710 --> 00:16:18.850 align:start position:0% spec of the bedding and the the convergence<00:16:16.460> around<00:16:16.640> bedding<00:16:17.180> spec<00:16:18.170> for<00:16:18.800> the 00:16:18.850 --> 00:16:18.860 align:start position:0% convergence around bedding spec for the 00:16:18.860 --> 00:16:20.800 align:start position:0% convergence around bedding spec for the validator<00:16:19.430> we<00:16:20.270> can 00:16:20.800 --> 00:16:20.810 align:start position:0% validator we can 00:16:20.810 --> 00:16:22.720 align:start position:0% validator we can there<00:16:21.290> are<00:16:21.470> similar<00:16:22.070> and<00:16:22.250> you<00:16:22.339> can<00:16:22.490> see<00:16:22.640> how 00:16:22.720 --> 00:16:22.730 align:start position:0% there are similar and you can see how 00:16:22.730 --> 00:16:26.530 align:start position:0% there are similar and you can see how tiny<00:16:23.030> it<00:16:23.240> is<00:16:23.360> it's<00:16:23.630> it's<00:16:23.900> teeny<00:16:24.200> tiny<00:16:25.540> this 00:16:26.530 --> 00:16:26.540 align:start position:0% tiny it is it's it's teeny tiny this 00:16:26.540 --> 00:16:29.260 align:start position:0% tiny it is it's it's teeny tiny this this<00:16:27.080> Wow<00:16:27.650> we<00:16:28.040> are<00:16:28.370> already<00:16:28.640> at<00:16:28.820> two<00:16:28.970> minutes 00:16:29.260 --> 00:16:29.270 align:start position:0% this Wow we are already at two minutes 00:16:29.270 --> 00:16:31.840 align:start position:0% this Wow we are already at two minutes okay<00:16:29.620> come<00:16:30.620> see<00:16:30.920> me<00:16:31.100> afterwards<00:16:31.430> and<00:16:31.760> I'll 00:16:31.840 --> 00:16:31.850 align:start position:0% okay come see me afterwards and I'll 00:16:31.850 --> 00:16:33.579 align:start position:0% okay come see me afterwards and I'll show<00:16:32.089> you<00:16:32.120> probing<00:16:32.930> this<00:16:33.110> spec<00:16:33.380> for 00:16:33.579 --> 00:16:33.589 align:start position:0% show you probing this spec for 00:16:33.589 --> 00:16:37.450 align:start position:0% show you probing this spec for properties<00:16:34.130> okay<00:16:34.790> so<00:16:35.000> well<00:16:35.300> I'll<00:16:35.720> I'll<00:16:36.280> cut<00:16:37.280> to 00:16:37.450 --> 00:16:37.460 align:start position:0% properties okay so well I'll I'll cut to 00:16:37.460 --> 00:16:46.710 align:start position:0% properties okay so well I'll I'll cut to the<00:16:37.660> cut<00:16:38.660> to<00:16:38.780> the<00:16:38.900> chase 00:16:46.710 --> 00:16:46.720 align:start position:0% 00:16:46.720 --> 00:16:49.360 align:start position:0% so<00:16:47.720> I<00:16:47.750> was<00:16:47.930> gonna<00:16:48.080> give<00:16:48.290> you<00:16:48.410> a<00:16:48.440> demo<00:16:48.830> but<00:16:49.310> I 00:16:49.360 --> 00:16:49.370 align:start position:0% so I was gonna give you a demo but I 00:16:49.370 --> 00:16:52.390 align:start position:0% so I was gonna give you a demo but I would<00:16:49.610> like<00:16:49.760> to<00:16:49.940> just<00:16:50.120> take<00:16:50.330> take<00:16:50.630> a<00:16:51.220> just<00:16:52.220> come 00:16:52.390 --> 00:16:52.400 align:start position:0% would like to just take take a just come 00:16:52.400 --> 00:16:53.950 align:start position:0% would like to just take take a just come to<00:16:52.520> come<00:16:52.670> see<00:16:52.820> me<00:16:52.970> afterwards<00:16:53.270> and<00:16:53.480> I'll<00:16:53.570> give 00:16:53.950 --> 00:16:53.960 align:start position:0% to come see me afterwards and I'll give 00:16:53.960 --> 00:16:56.260 align:start position:0% to come see me afterwards and I'll give you<00:16:54.050> a<00:16:54.110> lot<00:16:54.680> more<00:16:54.950> of<00:16:55.100> the<00:16:55.220> flavor<00:16:55.700> of<00:16:55.820> the<00:16:56.030> spec 00:16:56.260 --> 00:16:56.270 align:start position:0% you a lot more of the flavor of the spec 00:16:56.270 --> 00:16:57.670 align:start position:0% you a lot more of the flavor of the spec and<00:16:56.300> how<00:16:56.570> how<00:16:56.960> we<00:16:57.020> can<00:16:57.260> probe<00:16:57.500> it 00:16:57.670 --> 00:16:57.680 align:start position:0% and how how we can probe it 00:16:57.680 --> 00:16:59.080 align:start position:0% and how how we can probe it automatically<00:16:58.280> with<00:16:58.400> the<00:16:58.490> spatial<00:16:58.850> logic 00:16:59.080 --> 00:16:59.090 align:start position:0% automatically with the spatial logic 00:16:59.090 --> 00:17:00.520 align:start position:0% automatically with the spatial logic model<00:16:59.360> checker<00:16:59.570> but<00:17:00.110> I<00:17:00.140> would<00:17:00.320> like<00:17:00.470> to 00:17:00.520 --> 00:17:00.530 align:start position:0% model checker but I would like to 00:17:00.530 --> 00:17:02.890 align:start position:0% model checker but I would like to conclude<00:17:00.830> by<00:17:01.460> just<00:17:01.730> taking<00:17:02.120> you<00:17:02.420> through<00:17:02.450> a 00:17:02.890 --> 00:17:02.900 align:start position:0% conclude by just taking you through a 00:17:02.900 --> 00:17:05.650 align:start position:0% conclude by just taking you through a little<00:17:03.290> bit<00:17:03.670> taking<00:17:04.670> these<00:17:04.820> same<00:17:05.180> kind<00:17:05.540> of 00:17:05.650 --> 00:17:05.660 align:start position:0% little bit taking these same kind of 00:17:05.660 --> 00:17:07.780 align:start position:0% little bit taking these same kind of specs<00:17:06.020> and<00:17:06.350> using<00:17:06.980> the<00:17:07.100> compositional 00:17:07.780 --> 00:17:07.790 align:start position:0% specs and using the compositional 00:17:07.790 --> 00:17:11.650 align:start position:0% specs and using the compositional structure<00:17:08.390> we<00:17:08.930> can<00:17:09.080> walk<00:17:09.620> this<00:17:10.370> structure<00:17:11.090> we 00:17:11.650 --> 00:17:11.660 align:start position:0% structure we can walk this structure we 00:17:11.660 --> 00:17:13.990 align:start position:0% structure we can walk this structure we can<00:17:11.810> essentially<00:17:12.410> build<00:17:12.710> up<00:17:12.950> a<00:17:13.070> new<00:17:13.310> semantics 00:17:13.990 --> 00:17:14.000 align:start position:0% can essentially build up a new semantics 00:17:14.000 --> 00:17:16.630 align:start position:0% can essentially build up a new semantics from<00:17:14.810> the<00:17:14.930> existing<00:17:15.470> semantics<00:17:16.040> in<00:17:16.250> a<00:17:16.400> nice 00:17:16.630 --> 00:17:16.640 align:start position:0% from the existing semantics in a nice 00:17:16.640 --> 00:17:22.360 align:start position:0% from the existing semantics in a nice clean<00:17:17.270> careful<00:17:17.870> way<00:17:18.430> so<00:17:19.430> I<00:17:19.960> took<00:17:20.960> the<00:17:21.620> I<00:17:21.920> took 00:17:22.360 --> 00:17:22.370 align:start position:0% clean careful way so I took the I took 00:17:22.370 --> 00:17:24.790 align:start position:0% clean careful way so I took the I took the<00:17:22.660> essentially<00:17:23.660> a<00:17:23.690> variant<00:17:24.260> of<00:17:24.350> the<00:17:24.500> applied 00:17:24.790 --> 00:17:24.800 align:start position:0% the essentially a variant of the applied 00:17:24.800 --> 00:17:28.240 align:start position:0% the essentially a variant of the applied PI<00:17:25.040> calculus<00:17:25.640> and<00:17:25.850> I<00:17:26.330> added<00:17:26.630> to<00:17:27.200> it<00:17:27.440> metering 00:17:28.240 --> 00:17:28.250 align:start position:0% PI calculus and I added to it metering 00:17:28.250 --> 00:17:31.840 align:start position:0% PI calculus and I added to it metering and<00:17:28.760> this<00:17:29.570> metering<00:17:30.080> basically<00:17:30.920> uses<00:17:31.340> three 00:17:31.840 --> 00:17:31.850 align:start position:0% and this metering basically uses three 00:17:31.850 --> 00:17:34.870 align:start position:0% and this metering basically uses three elements<00:17:32.390> so<00:17:32.810> there's<00:17:32.990> a<00:17:33.050> resource<00:17:33.760> there's<00:17:34.760> a 00:17:34.870 --> 00:17:34.880 align:start position:0% elements so there's a resource there's a 00:17:34.880 --> 00:17:37.450 align:start position:0% elements so there's a resource there's a there's<00:17:35.690> an<00:17:35.990> a<00:17:36.170> channel<00:17:36.590> for<00:17:36.770> the<00:17:36.800> exchange<00:17:37.280> of 00:17:37.450 --> 00:17:37.460 align:start position:0% there's an a channel for the exchange of 00:17:37.460 --> 00:17:39.370 align:start position:0% there's an a channel for the exchange of the<00:17:37.580> resource<00:17:38.000> and<00:17:38.210> there's<00:17:38.600> a<00:17:38.690> channel<00:17:39.050> for 00:17:39.370 --> 00:17:39.380 align:start position:0% the resource and there's a channel for 00:17:39.380 --> 00:17:42.040 align:start position:0% the resource and there's a channel for the<00:17:39.470> next<00:17:39.830> step<00:17:40.100> that<00:17:40.400> next<00:17:41.120> step<00:17:41.300> is<00:17:41.450> again<00:17:41.780> an 00:17:42.040 --> 00:17:42.050 align:start position:0% the next step that next step is again an 00:17:42.050 --> 00:17:45.490 align:start position:0% the next step that next step is again an encoding<00:17:42.860> of<00:17:42.920> a<00:17:43.040> continuation<00:17:43.490> and<00:17:44.350> what<00:17:45.350> we 00:17:45.490 --> 00:17:45.500 align:start position:0% encoding of a continuation and what we 00:17:45.500 --> 00:17:49.390 align:start position:0% encoding of a continuation and what we see<00:17:45.680> here<00:17:45.710> is<00:17:46.390> essentially<00:17:47.390> just<00:17:47.540> just<00:17:48.440> a<00:17:48.530> tiny 00:17:49.390 --> 00:17:49.400 align:start position:0% see here is essentially just just a tiny 00:17:49.400 --> 00:17:53.230 align:start position:0% see here is essentially just just a tiny little<00:17:49.820> harness<00:17:50.450> for<00:17:51.020> for<00:17:51.500> running<00:17:51.950> a<00:17:52.430> metered 00:17:53.230 --> 00:17:53.240 align:start position:0% little harness for for running a metered 00:17:53.240 --> 00:17:58.060 align:start position:0% little harness for for running a metered VM<00:17:55.240> we<00:17:56.240> run<00:17:56.510> inside<00:17:57.110> that<00:17:57.380> harness<00:17:57.830> the 00:17:58.060 --> 00:17:58.070 align:start position:0% VM we run inside that harness the 00:17:58.070 --> 00:18:00.760 align:start position:0% VM we run inside that harness the translation<00:17:58.910> of<00:17:59.090> our<00:17:59.660> of<00:17:59.930> our<00:18:00.140> little<00:18:00.500> tiny 00:18:00.760 --> 00:18:00.770 align:start position:0% translation of our of our little tiny 00:18:00.770 --> 00:18:05.050 align:start position:0% translation of our of our little tiny API<00:18:01.370> for<00:18:02.210> for<00:18:02.770> contracts<00:18:03.770> right<00:18:04.670> but<00:18:04.910> this 00:18:05.050 --> 00:18:05.060 align:start position:0% API for for contracts right but this 00:18:05.060 --> 00:18:07.090 align:start position:0% API for for contracts right but this this<00:18:05.330> API<00:18:05.690> and<00:18:06.080> this<00:18:06.230> contract<00:18:06.650> language<00:18:06.950> is<00:18:07.070> a 00:18:07.090 --> 00:18:07.100 align:start position:0% this API and this contract language is a 00:18:07.100 --> 00:18:08.920 align:start position:0% this API and this contract language is a little<00:18:07.280> different<00:18:07.820> and<00:18:08.210> the<00:18:08.480> reason<00:18:08.630> it's 00:18:08.920 --> 00:18:08.930 align:start position:0% little different and the reason it's 00:18:08.930 --> 00:18:11.310 align:start position:0% little different and the reason it's different<00:18:08.990> is<00:18:09.380> because<00:18:09.530> contracts<00:18:10.250> can<00:18:10.460> be 00:18:11.310 --> 00:18:11.320 align:start position:0% different is because contracts can be 00:18:11.320 --> 00:18:15.790 align:start position:0% different is because contracts can be executed<00:18:12.320> in<00:18:12.650> parallel<00:18:13.390> contracts<00:18:14.390> have<00:18:15.170> have 00:18:15.790 --> 00:18:15.800 align:start position:0% executed in parallel contracts have have 00:18:15.800 --> 00:18:17.830 align:start position:0% executed in parallel contracts have have other<00:18:16.430> interesting<00:18:17.000> properties<00:18:17.480> in<00:18:17.690> that 00:18:17.830 --> 00:18:17.840 align:start position:0% other interesting properties in that 00:18:17.840 --> 00:18:19.810 align:start position:0% other interesting properties in that contracts<00:18:18.410> themselves<00:18:18.590> can<00:18:19.070> be<00:18:19.100> reified<00:18:19.640> in 00:18:19.810 --> 00:18:19.820 align:start position:0% contracts themselves can be reified in 00:18:19.820 --> 00:18:26.170 align:start position:0% contracts themselves can be reified in exchanged<00:18:23.350> the<00:18:24.350> important<00:18:25.070> point<00:18:25.310> here<00:18:25.730> again 00:18:26.170 --> 00:18:26.180 align:start position:0% exchanged the important point here again 00:18:26.180 --> 00:18:27.700 align:start position:0% exchanged the important point here again I'm<00:18:26.330> happy<00:18:26.690> to<00:18:26.780> go<00:18:26.870> through<00:18:26.900> all<00:18:27.200> the<00:18:27.320> details 00:18:27.700 --> 00:18:27.710 align:start position:0% I'm happy to go through all the details 00:18:27.710 --> 00:18:29.800 align:start position:0% I'm happy to go through all the details with<00:18:27.920> you<00:18:28.070> offline<00:18:28.580> but<00:18:29.060> the<00:18:29.180> important<00:18:29.630> point 00:18:29.800 --> 00:18:29.810 align:start position:0% with you offline but the important point 00:18:29.810 --> 00:18:33.880 align:start position:0% with you offline but the important point here<00:18:30.080> is<00:18:30.230> the<00:18:30.620> size<00:18:30.950> of<00:18:31.220> this<00:18:31.370> spec<00:18:31.730> and<00:18:32.890> not 00:18:33.880 --> 00:18:33.890 align:start position:0% here is the size of this spec and not 00:18:33.890 --> 00:18:35.950 align:start position:0% here is the size of this spec and not only<00:18:34.250> the<00:18:34.400> size<00:18:34.670> of<00:18:34.850> this<00:18:35.060> spec<00:18:35.360> but<00:18:35.780> the 00:18:35.950 --> 00:18:35.960 align:start position:0% only the size of this spec but the 00:18:35.960 --> 00:18:37.960 align:start position:0% only the size of this spec but the correctness<00:18:36.440> properties<00:18:37.130> of<00:18:37.340> this<00:18:37.550> virtual 00:18:37.960 --> 00:18:37.970 align:start position:0% correctness properties of this virtual 00:18:37.970 --> 00:18:40.180 align:start position:0% correctness properties of this virtual machine<00:18:38.030> can<00:18:38.570> be<00:18:38.750> stated<00:18:39.110> and<00:18:39.440> proved<00:18:39.860> in 00:18:40.180 --> 00:18:40.190 align:start position:0% machine can be stated and proved in 00:18:40.190 --> 00:18:44.530 align:start position:0% machine can be stated and proved in about<00:18:40.670> 1/2<00:18:40.910> a<00:18:41.120> page<00:18:41.770> right<00:18:42.770> so<00:18:43.390> even<00:18:44.390> more 00:18:44.530 --> 00:18:44.540 align:start position:0% about 1/2 a page right so even more 00:18:44.540 --> 00:18:47.020 align:start position:0% about 1/2 a page right so even more interestingly<00:18:44.870> you<00:18:45.590> can<00:18:45.800> take<00:18:46.040> this<00:18:46.490> kind<00:18:46.850> of 00:18:47.020 --> 00:18:47.030 align:start position:0% interestingly you can take this kind of 00:18:47.030 --> 00:18:49.960 align:start position:0% interestingly you can take this kind of virtual<00:18:47.360> machine<00:18:47.720> and<00:18:47.900> bootstrap<00:18:48.640> so<00:18:49.640> you<00:18:49.730> can 00:18:49.960 --> 00:18:49.970 align:start position:0% virtual machine and bootstrap so you can 00:18:49.970 --> 00:18:52.390 align:start position:0% virtual machine and bootstrap so you can build<00:18:50.570> this<00:18:50.870> virtual<00:18:51.290> machine<00:18:51.590> on<00:18:51.770> top<00:18:52.130> of 00:18:52.390 --> 00:18:52.400 align:start position:0% build this virtual machine on top of 00:18:52.400 --> 00:18:54.340 align:start position:0% build this virtual machine on top of this<00:18:52.520> virtual<00:18:52.910> machine<00:18:53.080> and<00:18:54.080> it<00:18:54.140> would<00:18:54.230> be 00:18:54.340 --> 00:18:54.350 align:start position:0% this virtual machine and it would be 00:18:54.350 --> 00:18:56.350 align:start position:0% this virtual machine and it would be interesting<00:18:54.950> to<00:18:54.980> look<00:18:55.310> at<00:18:55.490> look<00:18:55.910> at<00:18:56.060> doing 00:18:56.350 --> 00:18:56.360 align:start position:0% interesting to look at look at doing 00:18:56.360 --> 00:18:58.330 align:start position:0% interesting to look at look at doing that<00:18:56.540> with<00:18:57.020> the<00:18:57.200> existing<00:18:57.530> VM 00:18:58.330 --> 00:18:58.340 align:start position:0% that with the existing VM 00:18:58.340 --> 00:18:59.380 align:start position:0% that with the existing VM that<00:18:58.610> would<00:18:58.730> be<00:18:58.820> an<00:18:58.909> interesting<00:18:59.179> question 00:18:59.380 --> 00:18:59.390 align:start position:0% that would be an interesting question 00:18:59.390 --> 00:19:03.490 align:start position:0% that would be an interesting question could<00:19:00.380> we<00:19:00.590> build<00:19:00.919> the<00:19:01.789> etherium<00:19:02.500> blockchain 00:19:03.490 --> 00:19:03.500 align:start position:0% could we build the etherium blockchain 00:19:03.500 --> 00:19:06.070 align:start position:0% could we build the etherium blockchain on<00:19:03.710> top<00:19:04.100> of<00:19:04.279> the<00:19:04.400> existing<00:19:04.490> vm<00:19:05.120> does<00:19:05.900> it 00:19:06.070 --> 00:19:06.080 align:start position:0% on top of the existing vm does it 00:19:06.080 --> 00:19:09.159 align:start position:0% on top of the existing vm does it bootstrap<00:19:06.590> and<00:19:06.830> that<00:19:07.580> that<00:19:07.940> that<00:19:08.659> brings<00:19:08.929> us 00:19:09.159 --> 00:19:09.169 align:start position:0% bootstrap and that that that brings us 00:19:09.169 --> 00:19:10.570 align:start position:0% bootstrap and that that that brings us that<00:19:09.409> to<00:19:09.620> the<00:19:09.740> point<00:19:09.950> I<00:19:10.010> was<00:19:10.130> trying<00:19:10.250> to<00:19:10.429> make 00:19:10.570 --> 00:19:10.580 align:start position:0% that to the point I was trying to make 00:19:10.580 --> 00:19:12.760 align:start position:0% that to the point I was trying to make at<00:19:10.700> the<00:19:10.760> very<00:19:10.970> beginning<00:19:11.419> do<00:19:12.140> we<00:19:12.320> have<00:19:12.590> this 00:19:12.760 --> 00:19:12.770 align:start position:0% at the very beginning do we have this 00:19:12.770 --> 00:19:14.919 align:start position:0% at the very beginning do we have this self<00:19:13.130> loop<00:19:13.429> right<00:19:14.150> because<00:19:14.390> that's<00:19:14.630> your 00:19:14.919 --> 00:19:14.929 align:start position:0% self loop right because that's your 00:19:14.929 --> 00:19:18.720 align:start position:0% self loop right because that's your first<00:19:15.320> and<00:19:15.740> best<00:19:16.130> test<00:19:16.640> that<00:19:17.240> you<00:19:17.390> can<00:19:17.570> scale 00:19:18.720 --> 00:19:18.730 align:start position:0% first and best test that you can scale 00:19:18.730 --> 00:19:22.000 align:start position:0% first and best test that you can scale so<00:19:19.730> the<00:19:20.539> big<00:19:20.809> picture<00:19:21.049> that<00:19:21.529> I<00:19:21.559> want<00:19:21.770> to<00:19:21.860> leave 00:19:22.000 --> 00:19:22.010 align:start position:0% so the big picture that I want to leave 00:19:22.010 --> 00:19:23.380 align:start position:0% so the big picture that I want to leave you<00:19:22.159> with<00:19:22.340> is<00:19:22.490> that<00:19:22.580> is<00:19:23.000> that 00:19:23.380 --> 00:19:23.390 align:start position:0% you with is that is that 00:19:23.390 --> 00:19:25.990 align:start position:0% you with is that is that compositionality<00:19:24.350> this<00:19:25.130> this<00:19:25.429> kind<00:19:25.850> of 00:19:25.990 --> 00:19:26.000 align:start position:0% compositionality this this kind of 00:19:26.000 --> 00:19:28.120 align:start position:0% compositionality this this kind of finding<00:19:26.929> the<00:19:27.049> small<00:19:27.380> and<00:19:27.590> the<00:19:27.710> large<00:19:27.740> the 00:19:28.120 --> 00:19:28.130 align:start position:0% finding the small and the large the 00:19:28.130 --> 00:19:30.279 align:start position:0% finding the small and the large the large<00:19:28.549> and<00:19:28.789> the<00:19:28.820> small<00:19:28.880> is<00:19:29.360> the<00:19:29.720> key<00:19:30.110> to 00:19:30.279 --> 00:19:30.289 align:start position:0% large and the small is the key to 00:19:30.289 --> 00:19:35.500 align:start position:0% large and the small is the key to scaling<00:19:30.620> any<00:19:30.890> system<00:19:31.690> so<00:19:32.690> thank<00:19:33.380> you