WEBVTT Kind: captions Language: en 00:00:04.840 --> 00:00:07.770 align:start position:0% hi<00:00:05.170> everyone<00:00:05.440> good<00:00:06.130> morning<00:00:06.490> my<00:00:07.300> name<00:00:07.450> is<00:00:07.480> Sean 00:00:07.770 --> 00:00:07.780 align:start position:0% hi everyone good morning my name is Sean 00:00:07.780 --> 00:00:09.629 align:start position:0% hi everyone good morning my name is Sean and<00:00:07.810> I'm<00:00:08.140> working<00:00:08.320> on<00:00:08.560> the<00:00:08.620> formality<00:00:09.430> proof 00:00:09.629 --> 00:00:09.639 align:start position:0% and I'm working on the formality proof 00:00:09.639 --> 00:00:12.320 align:start position:0% and I'm working on the formality proof language<00:00:10.030> with<00:00:10.690> my<00:00:10.809> co-founder<00:00:10.990> Victor<00:00:11.559> Maya 00:00:12.320 --> 00:00:12.330 align:start position:0% language with my co-founder Victor Maya 00:00:12.330 --> 00:00:15.539 align:start position:0% language with my co-founder Victor Maya what's<00:00:13.330> a<00:00:13.389> proof<00:00:13.570> language<00:00:14.250> so<00:00:15.250> let's<00:00:15.400> do<00:00:15.520> a 00:00:15.539 --> 00:00:15.549 align:start position:0% what's a proof language so let's do a 00:00:15.549 --> 00:00:18.870 align:start position:0% what's a proof language so let's do a quick<00:00:15.760> refresher<00:00:16.090> on<00:00:16.209> type<00:00:16.539> systems<00:00:17.880> here's 00:00:18.870 --> 00:00:18.880 align:start position:0% quick refresher on type systems here's 00:00:18.880 --> 00:00:20.310 align:start position:0% quick refresher on type systems here's some<00:00:19.030> pseudocode<00:00:19.300> representing<00:00:19.990> an<00:00:20.080> array 00:00:20.310 --> 00:00:20.320 align:start position:0% some pseudocode representing an array 00:00:20.320 --> 00:00:22.620 align:start position:0% some pseudocode representing an array indexing<00:00:20.950> function<00:00:21.130> in<00:00:21.610> an<00:00:21.790> untyped<00:00:22.180> language 00:00:22.620 --> 00:00:22.630 align:start position:0% indexing function in an untyped language 00:00:22.630 --> 00:00:25.500 align:start position:0% indexing function in an untyped language I<00:00:22.870> take<00:00:23.500> an<00:00:23.590> index<00:00:23.980> and<00:00:24.190> an<00:00:24.550> array<00:00:24.820> and<00:00:25.120> I<00:00:25.270> try 00:00:25.500 --> 00:00:25.510 align:start position:0% I take an index and an array and I try 00:00:25.510 --> 00:00:27.090 align:start position:0% I take an index and an array and I try to<00:00:25.540> get<00:00:25.780> whatever's<00:00:26.140> inside<00:00:26.320> the<00:00:26.590> array<00:00:26.830> at 00:00:27.090 --> 00:00:27.100 align:start position:0% to get whatever's inside the array at 00:00:27.100 --> 00:00:30.990 align:start position:0% to get whatever's inside the array at that<00:00:27.340> index<00:00:28.110> get<00:00:29.110> 1<00:00:29.380> is<00:00:29.680> bar<00:00:30.250> because<00:00:30.760> array 00:00:30.990 --> 00:00:31.000 align:start position:0% that index get 1 is bar because array 00:00:31.000 --> 00:00:34.940 align:start position:0% that index get 1 is bar because array indices<00:00:31.270> start<00:00:31.690> at<00:00:31.750> 0<00:00:31.960> and<00:00:32.259> get<00:00:33.250> 2<00:00:33.460> is<00:00:33.760> bats 00:00:34.940 --> 00:00:34.950 align:start position:0% indices start at 0 and get 2 is bats 00:00:34.950 --> 00:00:36.360 align:start position:0% indices start at 0 and get 2 is bats here's<00:00:35.950> a<00:00:36.040> riddle 00:00:36.360 --> 00:00:36.370 align:start position:0% here's a riddle 00:00:36.370 --> 00:00:39.060 align:start position:0% here's a riddle if<00:00:36.489> get<00:00:36.760> 1<00:00:36.940> is<00:00:37.089> bar<00:00:37.329> and<00:00:37.600> get<00:00:37.719> 2<00:00:37.899> is<00:00:38.050> baz<00:00:38.289> what's 00:00:39.060 --> 00:00:39.070 align:start position:0% if get 1 is bar and get 2 is baz what's 00:00:39.070 --> 00:00:43.319 align:start position:0% if get 1 is bar and get 2 is baz what's get<00:00:39.309> 1.5<00:00:40.410> better<00:00:41.410> question<00:00:41.769> what<00:00:42.370> should<00:00:42.789> get 00:00:43.319 --> 00:00:43.329 align:start position:0% get 1.5 better question what should get 00:00:43.329 --> 00:00:47.880 align:start position:0% get 1.5 better question what should get 1.5<00:00:43.899> be<00:00:44.109> a<00:00:45.089> runtime<00:00:46.089> error<00:00:46.620> indexing<00:00:47.620> an<00:00:47.710> array 00:00:47.880 --> 00:00:47.890 align:start position:0% 1.5 be a runtime error indexing an array 00:00:47.890 --> 00:00:49.439 align:start position:0% 1.5 be a runtime error indexing an array with<00:00:48.070> a<00:00:48.100> non<00:00:48.309> integer<00:00:48.609> makes<00:00:48.999> no<00:00:49.149> sense 00:00:49.439 --> 00:00:49.449 align:start position:0% with a non integer makes no sense 00:00:49.449 --> 00:00:51.750 align:start position:0% with a non integer makes no sense because<00:00:49.989> an<00:00:50.230> untyped<00:00:50.589> language<00:00:51.010> but<00:00:51.609> a<00:00:51.640> none 00:00:51.750 --> 00:00:51.760 align:start position:0% because an untyped language but a none 00:00:51.760 --> 00:00:53.279 align:start position:0% because an untyped language but a none type<00:00:51.909> language<00:00:52.239> lets<00:00:52.600> you<00:00:52.690> shoot<00:00:52.870> yourself<00:00:52.960> in 00:00:53.279 --> 00:00:53.289 align:start position:0% type language lets you shoot yourself in 00:00:53.289 --> 00:00:55.049 align:start position:0% type language lets you shoot yourself in the<00:00:53.350> foot<00:00:53.589> and<00:00:53.769> make<00:00:54.280> a<00:00:54.309> bad<00:00:54.489> function<00:00:54.879> call 00:00:55.049 --> 00:00:55.059 align:start position:0% the foot and make a bad function call 00:00:55.059 --> 00:00:58.169 align:start position:0% the foot and make a bad function call and<00:00:55.300> this<00:00:55.690> only<00:00:55.929> fails<00:00:56.109> during<00:00:56.319> execution<00:00:57.179> ie 00:00:58.169 --> 00:00:58.179 align:start position:0% and this only fails during execution ie 00:00:58.179 --> 00:00:59.969 align:start position:0% and this only fails during execution ie when<00:00:58.600> your<00:00:58.749> codes<00:00:59.019> running<00:00:59.379> and<00:00:59.559> can<00:00:59.739> affect 00:00:59.969 --> 00:00:59.979 align:start position:0% when your codes running and can affect 00:00:59.979 --> 00:01:02.700 align:start position:0% when your codes running and can affect the<00:01:00.069> world<00:01:00.190> around<00:01:00.460> it<00:01:01.350> runtime<00:01:02.350> errors<00:01:02.589> are 00:01:02.700 --> 00:01:02.710 align:start position:0% the world around it runtime errors are 00:01:02.710 --> 00:01:04.229 align:start position:0% the world around it runtime errors are tough<00:01:02.920> because<00:01:03.129> sometimes<00:01:03.609> they<00:01:03.729> do<00:01:03.789> nothing 00:01:04.229 --> 00:01:04.239 align:start position:0% tough because sometimes they do nothing 00:01:04.239 --> 00:01:05.969 align:start position:0% tough because sometimes they do nothing and<00:01:04.420> sometimes<00:01:05.050> they<00:01:05.350> cause<00:01:05.530> your<00:01:05.710> spacecraft 00:01:05.969 --> 00:01:05.979 align:start position:0% and sometimes they cause your spacecraft 00:01:05.979 --> 00:01:08.310 align:start position:0% and sometimes they cause your spacecraft to<00:01:06.430> perform<00:01:06.820> a<00:01:07.030> rapid<00:01:07.690> unscheduled 00:01:08.310 --> 00:01:08.320 align:start position:0% to perform a rapid unscheduled 00:01:08.320 --> 00:01:10.740 align:start position:0% to perform a rapid unscheduled disassembly<00:01:08.950> your<00:01:09.850> codes<00:01:10.030> runtime<00:01:10.360> could<00:01:10.600> be 00:01:10.740 --> 00:01:10.750 align:start position:0% disassembly your codes runtime could be 00:01:10.750 --> 00:01:12.510 align:start position:0% disassembly your codes runtime could be in<00:01:10.899> five<00:01:11.110> minutes<00:01:11.469> on<00:01:11.619> your<00:01:11.770> laptop<00:01:12.159> or<00:01:12.460> it 00:01:12.510 --> 00:01:12.520 align:start position:0% in five minutes on your laptop or it 00:01:12.520 --> 00:01:14.130 align:start position:0% in five minutes on your laptop or it could<00:01:12.610> be<00:01:12.700> 30<00:01:12.939> years<00:01:13.240> for<00:01:13.450> now<00:01:13.570> on<00:01:13.780> devices 00:01:14.130 --> 00:01:14.140 align:start position:0% could be 30 years for now on devices 00:01:14.140 --> 00:01:16.020 align:start position:0% could be 30 years for now on devices that<00:01:14.320> don't<00:01:14.530> even<00:01:14.770> exist<00:01:14.890> yet<00:01:15.100> you<00:01:15.759> don't<00:01:15.880> know 00:01:16.020 --> 00:01:16.030 align:start position:0% that don't even exist yet you don't know 00:01:16.030 --> 00:01:19.109 align:start position:0% that don't even exist yet you don't know its<00:01:16.329> runtime<00:01:17.219> by<00:01:18.219> adding<00:01:18.460> some<00:01:18.610> types<00:01:18.820> we<00:01:19.000> can 00:01:19.109 --> 00:01:19.119 align:start position:0% its runtime by adding some types we can 00:01:19.119 --> 00:01:21.389 align:start position:0% its runtime by adding some types we can get<00:01:19.240> the<00:01:19.329> compiler<00:01:19.780> to<00:01:19.810> complain<00:01:20.229> hey<00:01:20.680> fix 00:01:21.389 --> 00:01:21.399 align:start position:0% get the compiler to complain hey fix 00:01:21.399 --> 00:01:23.160 align:start position:0% get the compiler to complain hey fix your<00:01:21.579> code<00:01:21.729> you<00:01:22.329> can't<00:01:22.509> have<00:01:22.659> an<00:01:22.750> index<00:01:23.049> that's 00:01:23.160 --> 00:01:23.170 align:start position:0% your code you can't have an index that's 00:01:23.170 --> 00:01:25.889 align:start position:0% your code you can't have an index that's not<00:01:23.350> an<00:01:23.469> integer<00:01:23.789> this<00:01:24.789> error<00:01:25.210> might<00:01:25.719> look 00:01:25.889 --> 00:01:25.899 align:start position:0% not an integer this error might look 00:01:25.899 --> 00:01:27.630 align:start position:0% not an integer this error might look deceptively<00:01:26.170> similar<00:01:26.710> the<00:01:26.950> previous<00:01:27.280> one<00:01:27.460> but 00:01:27.630 --> 00:01:27.640 align:start position:0% deceptively similar the previous one but 00:01:27.640 --> 00:01:30.359 align:start position:0% deceptively similar the previous one but there's<00:01:27.820> one<00:01:28.060> crucial<00:01:28.689> difference<00:01:29.039> it<00:01:30.039> occurs 00:01:30.359 --> 00:01:30.369 align:start position:0% there's one crucial difference it occurs 00:01:30.369 --> 00:01:33.599 align:start position:0% there's one crucial difference it occurs before<00:01:30.670> your<00:01:31.240> code<00:01:31.479> runs<00:01:31.840> that<00:01:32.770> is<00:01:32.979> before<00:01:33.520> it 00:01:33.599 --> 00:01:33.609 align:start position:0% before your code runs that is before it 00:01:33.609 --> 00:01:36.660 align:start position:0% before your code runs that is before it can<00:01:33.759> do<00:01:34.030> any<00:01:34.270> damage<00:01:34.770> but<00:01:35.770> simple<00:01:36.100> types<00:01:36.310> are 00:01:36.660 --> 00:01:36.670 align:start position:0% can do any damage but simple types are 00:01:36.670 --> 00:01:38.910 align:start position:0% can do any damage but simple types are kind<00:01:36.969> of<00:01:37.030> inflexible<00:01:37.600> this<00:01:38.229> function<00:01:38.619> only 00:01:38.910 --> 00:01:38.920 align:start position:0% kind of inflexible this function only 00:01:38.920 --> 00:01:40.469 align:start position:0% kind of inflexible this function only works<00:01:39.250> for<00:01:39.430> arrays<00:01:39.670> that<00:01:39.700> contain<00:01:39.880> integers 00:01:40.469 --> 00:01:40.479 align:start position:0% works for arrays that contain integers 00:01:40.479 --> 00:01:42.990 align:start position:0% works for arrays that contain integers if<00:01:41.320> we<00:01:41.590> want<00:01:41.740> different<00:01:41.890> array<00:01:42.219> contents<00:01:42.789> in<00:01:42.939> a 00:01:42.990 --> 00:01:43.000 align:start position:0% if we want different array contents in a 00:01:43.000 --> 00:01:44.219 align:start position:0% if we want different array contents in a simply<00:01:43.329> type<00:01:43.509> language<00:01:43.899> we<00:01:44.079> need<00:01:44.170> a 00:01:44.219 --> 00:01:44.229 align:start position:0% simply type language we need a 00:01:44.229 --> 00:01:46.709 align:start position:0% simply type language we need a copy/paste<00:01:44.799> lots<00:01:45.070> of<00:01:45.189> boilerplate<00:01:45.630> lots<00:01:46.630> of 00:01:46.709 --> 00:01:46.719 align:start position:0% copy/paste lots of boilerplate lots of 00:01:46.719 --> 00:01:47.999 align:start position:0% copy/paste lots of boilerplate lots of languages<00:01:47.079> try<00:01:47.229> to<00:01:47.289> solve<00:01:47.530> this<00:01:47.679> with<00:01:47.859> things 00:01:47.999 --> 00:01:48.009 align:start position:0% languages try to solve this with things 00:01:48.009 --> 00:01:50.870 align:start position:0% languages try to solve this with things like<00:01:48.130> interfaces<00:01:48.729> but<00:01:49.149> there's<00:01:49.329> a<00:01:49.390> better<00:01:49.509> way 00:01:50.870 --> 00:01:50.880 align:start position:0% like interfaces but there's a better way 00:01:50.880 --> 00:01:53.069 align:start position:0% like interfaces but there's a better way polymorphism<00:01:51.880> allows<00:01:52.060> us<00:01:52.570> to<00:01:52.689> have<00:01:52.810> a<00:01:52.840> type 00:01:53.069 --> 00:01:53.079 align:start position:0% polymorphism allows us to have a type 00:01:53.079 --> 00:01:55.380 align:start position:0% polymorphism allows us to have a type parameter<00:01:53.259> a<00:01:53.740> that<00:01:54.340> can<00:01:54.460> get<00:01:54.609> filled<00:01:54.880> with<00:01:55.090> int 00:01:55.380 --> 00:01:55.390 align:start position:0% parameter a that can get filled with int 00:01:55.390 --> 00:01:58.380 align:start position:0% parameter a that can get filled with int or<00:01:55.539> string<00:01:55.600> or<00:01:56.409> any<00:01:56.740> type<00:01:56.979> that<00:01:57.009> we<00:01:57.189> like<00:01:57.390> this 00:01:58.380 --> 00:01:58.390 align:start position:0% or string or any type that we like this 00:01:58.390 --> 00:02:00.359 align:start position:0% or string or any type that we like this is<00:01:58.509> really<00:01:58.869> useful<00:01:59.320> and<00:01:59.500> most<00:01:59.799> type<00:01:59.979> languages 00:02:00.359 --> 00:02:00.369 align:start position:0% is really useful and most type languages 00:02:00.369 --> 00:02:01.859 align:start position:0% is really useful and most type languages stop<00:02:00.579> there<00:02:00.820> but<00:02:01.539> this<00:02:01.630> still<00:02:01.810> doesn't 00:02:01.859 --> 00:02:01.869 align:start position:0% stop there but this still doesn't 00:02:01.869 --> 00:02:05.580 align:start position:0% stop there but this still doesn't prevent<00:02:02.350> all<00:02:02.560> runtime<00:02:03.219> errors<00:02:04.259> we<00:02:05.259> could<00:02:05.409> call 00:02:05.580 --> 00:02:05.590 align:start position:0% prevent all runtime errors we could call 00:02:05.590 --> 00:02:07.620 align:start position:0% prevent all runtime errors we could call get<00:02:05.799> with<00:02:05.920> a<00:02:05.950> really<00:02:06.340> large<00:02:06.490> index<00:02:07.090> and<00:02:07.329> cause 00:02:07.620 --> 00:02:07.630 align:start position:0% get with a really large index and cause 00:02:07.630 --> 00:02:09.960 align:start position:0% get with a really large index and cause an<00:02:07.810> out-of-bounds<00:02:08.200> runtime<00:02:08.679> error<00:02:08.970> some 00:02:09.960 --> 00:02:09.970 align:start position:0% an out-of-bounds runtime error some 00:02:09.970 --> 00:02:11.370 align:start position:0% an out-of-bounds runtime error some languages<00:02:10.420> don't<00:02:10.539> even<00:02:10.780> error<00:02:10.990> they<00:02:11.200> just 00:02:11.370 --> 00:02:11.380 align:start position:0% languages don't even error they just 00:02:11.380 --> 00:02:12.899 align:start position:0% languages don't even error they just dump<00:02:11.680> the<00:02:11.920> contents<00:02:12.100> of<00:02:12.370> memory<00:02:12.670> and<00:02:12.819> that's 00:02:12.899 --> 00:02:12.909 align:start position:0% dump the contents of memory and that's 00:02:12.909 --> 00:02:15.960 align:start position:0% dump the contents of memory and that's probably<00:02:13.180> worse<00:02:14.280> but<00:02:15.280> for<00:02:15.430> what<00:02:15.550> the<00:02:15.610> compiler 00:02:15.960 --> 00:02:15.970 align:start position:0% probably worse but for what the compiler 00:02:15.970 --> 00:02:17.940 align:start position:0% probably worse but for what the compiler to<00:02:16.000> warn<00:02:16.300> us<00:02:16.450> if<00:02:16.659> our<00:02:16.810> index<00:02:17.440> is<00:02:17.590> bigger<00:02:17.769> than 00:02:17.940 --> 00:02:17.950 align:start position:0% to warn us if our index is bigger than 00:02:17.950 --> 00:02:18.720 align:start position:0% to warn us if our index is bigger than our 00:02:18.720 --> 00:02:18.730 align:start position:0% our 00:02:18.730 --> 00:02:20.040 align:start position:0% our we're<00:02:18.910> gonna<00:02:19.000> need<00:02:19.240> types<00:02:19.540> that<00:02:19.660> depend<00:02:19.990> not 00:02:20.040 --> 00:02:20.050 align:start position:0% we're gonna need types that depend not 00:02:20.050 --> 00:02:23.660 align:start position:0% we're gonna need types that depend not only<00:02:20.170> on<00:02:20.470> other<00:02:20.590> types<00:02:20.950> but<00:02:21.580> on<00:02:21.670> normal<00:02:22.030> values 00:02:23.660 --> 00:02:23.670 align:start position:0% only on other types but on normal values 00:02:23.670 --> 00:02:26.580 align:start position:0% only on other types but on normal values here<00:02:24.670> we<00:02:24.819> have<00:02:25.000> a<00:02:25.030> type<00:02:25.390> type<00:02:25.930> level<00:02:26.110> number<00:02:26.440> n 00:02:26.580 --> 00:02:26.590 align:start position:0% here we have a type type level number n 00:02:26.590 --> 00:02:28.710 align:start position:0% here we have a type type level number n that<00:02:27.370> tells<00:02:27.580> the<00:02:27.700> compiler<00:02:27.970> how<00:02:28.330> long<00:02:28.569> the 00:02:28.710 --> 00:02:28.720 align:start position:0% that tells the compiler how long the 00:02:28.720 --> 00:02:30.870 align:start position:0% that tells the compiler how long the array<00:02:28.930> is<00:02:29.110> just<00:02:29.370> like<00:02:30.370> we<00:02:30.490> have<00:02:30.610> a<00:02:30.640> type 00:02:30.870 --> 00:02:30.880 align:start position:0% array is just like we have a type 00:02:30.880 --> 00:02:32.520 align:start position:0% array is just like we have a type parameter<00:02:31.030> a<00:02:31.450> that<00:02:31.750> tells<00:02:31.930> us<00:02:32.050> what's<00:02:32.230> in<00:02:32.410> the 00:02:32.520 --> 00:02:32.530 align:start position:0% parameter a that tells us what's in the 00:02:32.530 --> 00:02:35.640 align:start position:0% parameter a that tells us what's in the array<00:02:32.770> n<00:02:33.010> is<00:02:33.730> a<00:02:33.760> type<00:02:34.090> level<00:02:34.270> value<00:02:34.810> that<00:02:35.470> lets 00:02:35.640 --> 00:02:35.650 align:start position:0% array n is a type level value that lets 00:02:35.650 --> 00:02:37.020 align:start position:0% array n is a type level value that lets us<00:02:35.770> enforce<00:02:36.130> that<00:02:36.250> our<00:02:36.340> index<00:02:36.670> has<00:02:36.850> to<00:02:36.880> be 00:02:37.020 --> 00:02:37.030 align:start position:0% us enforce that our index has to be 00:02:37.030 --> 00:02:40.680 align:start position:0% us enforce that our index has to be between<00:02:37.239> 0<00:02:37.450> and<00:02:38.050> n<00:02:38.170> minus<00:02:38.200> 1<00:02:39.330> the<00:02:40.330> values 00:02:40.680 --> 00:02:40.690 align:start position:0% between 0 and n minus 1 the values 00:02:40.690 --> 00:02:42.690 align:start position:0% between 0 and n minus 1 the values independent<00:02:41.260> types<00:02:41.470> don't<00:02:42.370> have<00:02:42.489> to<00:02:42.610> be 00:02:42.690 --> 00:02:42.700 align:start position:0% independent types don't have to be 00:02:42.700 --> 00:02:44.160 align:start position:0% independent types don't have to be constants<00:02:43.180> they<00:02:43.450> can<00:02:43.600> be<00:02:43.690> the<00:02:43.780> results<00:02:44.080> of 00:02:44.160 --> 00:02:44.170 align:start position:0% constants they can be the results of 00:02:44.170 --> 00:02:46.590 align:start position:0% constants they can be the results of computations<00:02:44.790> this<00:02:45.790> lets<00:02:46.000> us<00:02:46.060> constrain<00:02:46.480> the 00:02:46.590 --> 00:02:46.600 align:start position:0% computations this lets us constrain the 00:02:46.600 --> 00:02:48.720 align:start position:0% computations this lets us constrain the function<00:02:46.930> so<00:02:47.170> much<00:02:47.380> that<00:02:48.040> we<00:02:48.130> can<00:02:48.250> often<00:02:48.520> guess 00:02:48.720 --> 00:02:48.730 align:start position:0% function so much that we can often guess 00:02:48.730 --> 00:02:50.400 align:start position:0% function so much that we can often guess what<00:02:48.940> the<00:02:49.030> implementation<00:02:49.660> has<00:02:49.840> to<00:02:49.989> be<00:02:50.110> just 00:02:50.400 --> 00:02:50.410 align:start position:0% what the implementation has to be just 00:02:50.410 --> 00:02:52.259 align:start position:0% what the implementation has to be just from<00:02:50.560> its<00:02:50.650> shape<00:02:50.920> kind<00:02:51.820> of<00:02:51.880> like<00:02:52.000> a<00:02:52.030> game<00:02:52.239> of 00:02:52.259 --> 00:02:52.269 align:start position:0% from its shape kind of like a game of 00:02:52.269 --> 00:02:54.240 align:start position:0% from its shape kind of like a game of who's<00:02:52.510> that<00:02:52.540> Pokemon<00:02:53.170> but<00:02:53.440> with<00:02:53.590> types<00:02:53.830> in 00:02:54.240 --> 00:02:54.250 align:start position:0% who's that Pokemon but with types in 00:02:54.250 --> 00:02:55.860 align:start position:0% who's that Pokemon but with types in this<00:02:55.120> case<00:02:55.300> we<00:02:55.420> have<00:02:55.510> a<00:02:55.570> function<00:02:55.840> that 00:02:55.860 --> 00:02:55.870 align:start position:0% this case we have a function that 00:02:55.870 --> 00:02:57.780 align:start position:0% this case we have a function that receives<00:02:56.200> a<00:02:56.290> number<00:02:56.560> n<00:02:56.709> and<00:02:56.980> returns<00:02:57.610> an<00:02:57.730> array 00:02:57.780 --> 00:02:57.790 align:start position:0% receives a number n and returns an array 00:02:57.790 --> 00:02:59.400 align:start position:0% receives a number n and returns an array of<00:02:57.940> prime<00:02:58.300> numbers<00:02:58.660> that<00:02:58.840> have<00:02:59.050> multiplied 00:02:59.400 --> 00:02:59.410 align:start position:0% of prime numbers that have multiplied 00:02:59.410 --> 00:03:02.009 align:start position:0% of prime numbers that have multiplied together<00:02:59.560> equal<00:03:00.310> n<00:03:00.540> Karen<00:03:01.540> can<00:03:01.690> anyone<00:03:01.870> guess 00:03:02.009 --> 00:03:02.019 align:start position:0% together equal n Karen can anyone guess 00:03:02.019 --> 00:03:05.070 align:start position:0% together equal n Karen can anyone guess what<00:03:02.140> this<00:03:02.290> has<00:03:02.410> to<00:03:02.440> be<00:03:02.880> it's<00:03:03.880> factorize<00:03:04.330> the 00:03:05.070 --> 00:03:05.080 align:start position:0% what this has to be it's factorize the 00:03:05.080 --> 00:03:06.330 align:start position:0% what this has to be it's factorize the cool<00:03:05.290> thing<00:03:05.440> is<00:03:05.470> nothing<00:03:05.860> other<00:03:06.040> than<00:03:06.160> the 00:03:06.330 --> 00:03:06.340 align:start position:0% cool thing is nothing other than the 00:03:06.340 --> 00:03:07.979 align:start position:0% cool thing is nothing other than the correct<00:03:06.550> factorization<00:03:06.989> implementation 00:03:07.979 --> 00:03:07.989 align:start position:0% correct factorization implementation 00:03:07.989 --> 00:03:09.870 align:start position:0% correct factorization implementation will<00:03:08.350> pass<00:03:08.530> the<00:03:08.680> type<00:03:08.830> checker<00:03:09.069> that<00:03:09.730> the 00:03:09.870 --> 00:03:09.880 align:start position:0% will pass the type checker that the 00:03:09.880 --> 00:03:11.430 align:start position:0% will pass the type checker that the Fibonacci<00:03:10.269> sequence<00:03:10.600> would<00:03:10.930> be<00:03:11.019> a<00:03:11.050> type<00:03:11.260> error 00:03:11.430 --> 00:03:11.440 align:start position:0% Fibonacci sequence would be a type error 00:03:11.440 --> 00:03:13.259 align:start position:0% Fibonacci sequence would be a type error because<00:03:11.950> the<00:03:12.130> products<00:03:12.489> wouldn't<00:03:12.760> sum<00:03:12.970> to<00:03:13.120> it 00:03:13.259 --> 00:03:13.269 align:start position:0% because the products wouldn't sum to it 00:03:13.269 --> 00:03:16.949 align:start position:0% because the products wouldn't sum to it to<00:03:13.480> the<00:03:13.630> number<00:03:13.870> let's<00:03:14.709> play<00:03:14.830> again<00:03:15.840> given<00:03:16.840> an 00:03:16.949 --> 00:03:16.959 align:start position:0% to the number let's play again given an 00:03:16.959 --> 00:03:19.979 align:start position:0% to the number let's play again given an array<00:03:17.080> X's<00:03:17.880> return<00:03:18.880> an<00:03:19.000> array<00:03:19.269> wise<00:03:19.510> with<00:03:19.900> the 00:03:19.979 --> 00:03:19.989 align:start position:0% array X's return an array wise with the 00:03:19.989 --> 00:03:21.750 align:start position:0% array X's return an array wise with the same<00:03:20.200> elements<00:03:20.440> but<00:03:20.830> in<00:03:21.190> ascending<00:03:21.489> order 00:03:21.750 --> 00:03:21.760 align:start position:0% same elements but in ascending order 00:03:21.760 --> 00:03:24.979 align:start position:0% same elements but in ascending order what<00:03:22.450> does<00:03:22.540> this<00:03:22.600> function<00:03:22.930> have<00:03:23.049> to<00:03:23.079> be<00:03:23.940> sort 00:03:24.979 --> 00:03:24.989 align:start position:0% what does this function have to be sort 00:03:24.989 --> 00:03:27.750 align:start position:0% what does this function have to be sort anything<00:03:25.989> else<00:03:26.110> is<00:03:26.260> a<00:03:26.290> type<00:03:26.500> error<00:03:26.650> those<00:03:27.519> such 00:03:27.750 --> 00:03:27.760 align:start position:0% anything else is a type error those such 00:03:27.760 --> 00:03:29.520 align:start position:0% anything else is a type error those such that<00:03:27.970> to<00:03:28.120> check<00:03:28.299> statically<00:03:28.840> which<00:03:29.290> means 00:03:29.520 --> 00:03:29.530 align:start position:0% that to check statically which means 00:03:29.530 --> 00:03:31.259 align:start position:0% that to check statically which means that<00:03:29.950> you<00:03:30.400> will<00:03:30.549> not<00:03:30.640> go<00:03:30.790> to<00:03:30.820> space<00:03:31.120> today 00:03:31.259 --> 00:03:31.269 align:start position:0% that you will not go to space today 00:03:31.269 --> 00:03:33.449 align:start position:0% that you will not go to space today becomes<00:03:32.079> my<00:03:32.530> code<00:03:32.739> is<00:03:32.890> broken<00:03:33.010> and<00:03:33.370> I<00:03:33.400> don't 00:03:33.449 --> 00:03:33.459 align:start position:0% becomes my code is broken and I don't 00:03:33.459 --> 00:03:35.670 align:start position:0% becomes my code is broken and I don't know<00:03:33.730> why<00:03:33.910> which<00:03:34.690> is<00:03:34.720> great<00:03:34.989> because<00:03:35.200> compile 00:03:35.670 --> 00:03:35.680 align:start position:0% know why which is great because compile 00:03:35.680 --> 00:03:37.680 align:start position:0% know why which is great because compile time<00:03:35.980> is<00:03:36.190> when<00:03:36.370> you<00:03:36.549> the<00:03:36.700> programmer<00:03:37.150> are<00:03:37.420> in 00:03:37.680 --> 00:03:37.690 align:start position:0% time is when you the programmer are in 00:03:37.690 --> 00:03:40.140 align:start position:0% time is when you the programmer are in the<00:03:37.750> process<00:03:37.930> of<00:03:38.200> fixing<00:03:38.350> your<00:03:38.560> code<00:03:38.970> this<00:03:39.970> is 00:03:40.140 --> 00:03:40.150 align:start position:0% the process of fixing your code this is 00:03:40.150 --> 00:03:41.789 align:start position:0% the process of fixing your code this is really<00:03:40.480> nice<00:03:40.630> for<00:03:40.690> immutable<00:03:41.350> block<00:03:41.530> chains 00:03:41.789 --> 00:03:41.799 align:start position:0% really nice for immutable block chains 00:03:41.799 --> 00:03:44.160 align:start position:0% really nice for immutable block chains where<00:03:42.340> a<00:03:42.519> runtime<00:03:42.910> error<00:03:42.970> means<00:03:43.510> my<00:03:43.840> code<00:03:44.049> is 00:03:44.160 --> 00:03:44.170 align:start position:0% where a runtime error means my code is 00:03:44.170 --> 00:03:45.870 align:start position:0% where a runtime error means my code is broken<00:03:44.440> no<00:03:45.100> one<00:03:45.220> can<00:03:45.370> get<00:03:45.489> their<00:03:45.610> money<00:03:45.790> out 00:03:45.870 --> 00:03:45.880 align:start position:0% broken no one can get their money out 00:03:45.880 --> 00:03:48.090 align:start position:0% broken no one can get their money out and<00:03:46.150> I<00:03:46.450> can't<00:03:46.690> fix<00:03:46.870> it<00:03:47.079> because<00:03:47.620> I<00:03:47.650> deployed<00:03:48.070> my 00:03:48.090 --> 00:03:48.100 align:start position:0% and I can't fix it because I deployed my 00:03:48.100 --> 00:03:51.870 align:start position:0% and I can't fix it because I deployed my code<00:03:48.459> to<00:03:48.489> an<00:03:48.760> immutable<00:03:49.180> platform<00:03:50.880> but 00:03:51.870 --> 00:03:51.880 align:start position:0% code to an immutable platform but 00:03:51.880 --> 00:03:53.520 align:start position:0% code to an immutable platform but dependent<00:03:52.239> types<00:03:52.329> are<00:03:52.540> useful<00:03:52.840> for<00:03:52.870> so<00:03:53.350> much 00:03:53.520 --> 00:03:53.530 align:start position:0% dependent types are useful for so much 00:03:53.530 --> 00:03:55.590 align:start position:0% dependent types are useful for so much more<00:03:53.799> if<00:03:54.040> we<00:03:54.310> can<00:03:54.370> do<00:03:54.489> arbitrary<00:03:55.120> type<00:03:55.420> level 00:03:55.590 --> 00:03:55.600 align:start position:0% more if we can do arbitrary type level 00:03:55.600 --> 00:03:57.360 align:start position:0% more if we can do arbitrary type level computation<00:03:56.320> we<00:03:56.739> can<00:03:56.890> use<00:03:57.010> our<00:03:57.130> type<00:03:57.340> system 00:03:57.360 --> 00:03:57.370 align:start position:0% computation we can use our type system 00:03:57.370 --> 00:04:00.060 align:start position:0% computation we can use our type system to<00:03:58.090> declare<00:03:58.390> any<00:03:58.600> number<00:03:58.900> of<00:03:58.989> any<00:03:59.470> combination 00:04:00.060 --> 00:04:00.070 align:start position:0% to declare any number of any combination 00:04:00.070 --> 00:04:02.130 align:start position:0% to declare any number of any combination of<00:04:00.130> properties<00:04:00.340> we<00:04:00.670> want<00:04:00.820> and<00:04:01.120> then<00:04:01.959> if<00:04:02.049> we 00:04:02.130 --> 00:04:02.140 align:start position:0% of properties we want and then if we 00:04:02.140 --> 00:04:03.599 align:start position:0% of properties we want and then if we write<00:04:02.290> code<00:04:02.500> that<00:04:02.530> validly<00:04:03.010> checks<00:04:03.310> as<00:04:03.459> those 00:04:03.599 --> 00:04:03.609 align:start position:0% write code that validly checks as those 00:04:03.609 --> 00:04:05.340 align:start position:0% write code that validly checks as those properties<00:04:04.030> we've<00:04:04.540> built<00:04:04.720> a<00:04:04.810> constructive 00:04:05.340 --> 00:04:05.350 align:start position:0% properties we've built a constructive 00:04:05.350 --> 00:04:07.050 align:start position:0% properties we've built a constructive executable<00:04:05.980> proof<00:04:06.280> of<00:04:06.489> the<00:04:06.670> theorem<00:04:06.850> that 00:04:07.050 --> 00:04:07.060 align:start position:0% executable proof of the theorem that 00:04:07.060 --> 00:04:09.300 align:start position:0% executable proof of the theorem that type<00:04:07.209> represents<00:04:07.560> this<00:04:08.560> is<00:04:08.709> the<00:04:08.799> curry<00:04:08.980> Howard 00:04:09.300 --> 00:04:09.310 align:start position:0% type represents this is the curry Howard 00:04:09.310 --> 00:04:11.729 align:start position:0% type represents this is the curry Howard isomorphism<00:04:10.000> and<00:04:10.299> by<00:04:10.450> favorite<00:04:10.900> isomorphism 00:04:11.729 --> 00:04:11.739 align:start position:0% isomorphism and by favorite isomorphism 00:04:11.739 --> 00:04:13.620 align:start position:0% isomorphism and by favorite isomorphism formal<00:04:12.670> logic<00:04:12.940> and<00:04:13.060> software<00:04:13.299> development 00:04:13.620 --> 00:04:13.630 align:start position:0% formal logic and software development 00:04:13.630 --> 00:04:15.300 align:start position:0% formal logic and software development are<00:04:13.810> actually<00:04:14.079> the<00:04:14.170> same<00:04:14.200> activity<00:04:14.859> it's<00:04:15.100> just 00:04:15.300 --> 00:04:15.310 align:start position:0% are actually the same activity it's just 00:04:15.310 --> 00:04:16.979 align:start position:0% are actually the same activity it's just not<00:04:15.430> obvious<00:04:15.609> because<00:04:16.090> the<00:04:16.180> usual<00:04:16.299> syntax<00:04:16.840> is 00:04:16.979 --> 00:04:16.989 align:start position:0% not obvious because the usual syntax is 00:04:16.989 --> 00:04:19.500 align:start position:0% not obvious because the usual syntax is very<00:04:17.169> different<00:04:17.590> most<00:04:18.400> math<00:04:18.609> syntax<00:04:19.060> forces 00:04:19.500 --> 00:04:19.510 align:start position:0% very different most math syntax forces 00:04:19.510 --> 00:04:21.029 align:start position:0% very different most math syntax forces you<00:04:19.600> to<00:04:19.630> do<00:04:19.810> the<00:04:19.900> execution<00:04:20.440> manually<00:04:20.859> and 00:04:21.029 --> 00:04:21.039 align:start position:0% you to do the execution manually and 00:04:21.039 --> 00:04:22.950 align:start position:0% you to do the execution manually and most<00:04:21.609> code<00:04:21.820> syntax<00:04:22.090> forces<00:04:22.630> you<00:04:22.690> to<00:04:22.720> keep 00:04:22.950 --> 00:04:22.960 align:start position:0% most code syntax forces you to keep 00:04:22.960 --> 00:04:26.159 align:start position:0% most code syntax forces you to keep track<00:04:23.200> of<00:04:23.350> type<00:04:23.530> information<00:04:23.860> manually<00:04:25.169> our 00:04:26.159 --> 00:04:26.169 align:start position:0% track of type information manually our 00:04:26.169 --> 00:04:27.390 align:start position:0% track of type information manually our goal<00:04:26.409> with<00:04:26.560> formality<00:04:27.010> is<00:04:27.099> to<00:04:27.220> have<00:04:27.370> a 00:04:27.390 --> 00:04:27.400 align:start position:0% goal with formality is to have a 00:04:27.400 --> 00:04:29.100 align:start position:0% goal with formality is to have a language<00:04:27.640> that's<00:04:27.970> really<00:04:28.360> really<00:04:28.599> good<00:04:28.900> for 00:04:29.100 --> 00:04:29.110 align:start position:0% language that's really really good for 00:04:29.110 --> 00:04:30.960 align:start position:0% language that's really really good for both<00:04:29.289> software<00:04:29.770> development<00:04:30.220> and<00:04:30.340> for 00:04:30.960 --> 00:04:30.970 align:start position:0% both software development and for 00:04:30.970 --> 00:04:31.920 align:start position:0% both software development and for exploring<00:04:31.360> mathematics 00:04:31.920 --> 00:04:31.930 align:start position:0% exploring mathematics 00:04:31.930 --> 00:04:33.600 align:start position:0% exploring mathematics we<00:04:32.500> want<00:04:32.680> to<00:04:32.740> make<00:04:32.860> a<00:04:32.889> programming<00:04:33.370> language 00:04:33.600 --> 00:04:33.610 align:start position:0% we want to make a programming language 00:04:33.610 --> 00:04:35.189 align:start position:0% we want to make a programming language as<00:04:33.699> accessible<00:04:34.300> as<00:04:34.419> Python<00:04:34.630> and<00:04:34.960> a<00:04:34.990> proof 00:04:35.189 --> 00:04:35.199 align:start position:0% as accessible as Python and a proof 00:04:35.199 --> 00:04:37.230 align:start position:0% as accessible as Python and a proof language<00:04:35.560> as<00:04:35.680> powerful<00:04:36.130> as<00:04:36.220> Agda<00:04:36.639> one<00:04:37.030> that's 00:04:37.230 --> 00:04:37.240 align:start position:0% language as powerful as Agda one that's 00:04:37.240 --> 00:04:40.680 align:start position:0% language as powerful as Agda one that's safe<00:04:37.509> fast<00:04:38.199> simple<00:04:38.889> and<00:04:39.100> portable<00:04:39.790> we<00:04:40.509> still 00:04:40.680 --> 00:04:40.690 align:start position:0% safe fast simple and portable we still 00:04:40.690 --> 00:04:41.999 align:start position:0% safe fast simple and portable we still have<00:04:40.780> a<00:04:40.810> long<00:04:40.930> way<00:04:41.080> to<00:04:41.139> meet<00:04:41.289> that<00:04:41.320> goal<00:04:41.650> but 00:04:41.999 --> 00:04:42.009 align:start position:0% have a long way to meet that goal but 00:04:42.009 --> 00:04:43.230 align:start position:0% have a long way to meet that goal but we've<00:04:42.130> made<00:04:42.220> great<00:04:42.430> progress<00:04:42.639> in<00:04:43.000> the<00:04:43.060> past 00:04:43.230 --> 00:04:43.240 align:start position:0% we've made great progress in the past 00:04:43.240 --> 00:04:45.629 align:start position:0% we've made great progress in the past year<00:04:43.770> here's<00:04:44.770> all<00:04:44.889> the<00:04:44.979> type<00:04:45.130> signatures<00:04:45.520> we 00:04:45.629 --> 00:04:45.639 align:start position:0% year here's all the type signatures we 00:04:45.639 --> 00:04:47.520 align:start position:0% year here's all the type signatures we just<00:04:45.820> went<00:04:45.940> over<00:04:46.240> but<00:04:46.570> informality<00:04:46.960> syntax 00:04:47.520 --> 00:04:47.530 align:start position:0% just went over but informality syntax 00:04:47.530 --> 00:04:51.689 align:start position:0% just went over but informality syntax instead<00:04:47.800> instead<00:04:48.190> of<00:04:48.430> pseudocode<00:04:49.229> and<00:04:50.699> here's 00:04:51.689 --> 00:04:51.699 align:start position:0% instead instead of pseudocode and here's 00:04:51.699 --> 00:04:53.370 align:start position:0% instead instead of pseudocode and here's how<00:04:51.820> we<00:04:51.910> declare<00:04:52.180> datatypes<00:04:52.690> and<00:04:52.900> how<00:04:53.110> we<00:04:53.169> take 00:04:53.370 --> 00:04:53.380 align:start position:0% how we declare datatypes and how we take 00:04:53.380 --> 00:04:55.409 align:start position:0% how we declare datatypes and how we take the<00:04:53.500> tail<00:04:53.680> of<00:04:53.830> a<00:04:53.889> list<00:04:54.070> the<00:04:55.000> cool<00:04:55.210> thing<00:04:55.389> here 00:04:55.409 --> 00:04:55.419 align:start position:0% the tail of a list the cool thing here 00:04:55.419 --> 00:04:57.060 align:start position:0% the tail of a list the cool thing here is<00:04:55.810> that<00:04:55.840> unlike<00:04:56.080> other<00:04:56.320> proof<00:04:56.620> languages 00:04:57.060 --> 00:04:57.070 align:start position:0% is that unlike other proof languages 00:04:57.070 --> 00:05:00.689 align:start position:0% is that unlike other proof languages like<00:04:57.520> or<00:04:57.759> Agda<00:04:58.500> our<00:04:59.500> data<00:04:59.949> types<00:05:00.250> aren't 00:05:00.689 --> 00:05:00.699 align:start position:0% like or Agda our data types aren't 00:05:00.699 --> 00:05:02.670 align:start position:0% like or Agda our data types aren't built<00:05:00.970> in<00:05:01.240> to<00:05:01.509> the<00:05:01.600> theory<00:05:01.840> they're<00:05:02.350> actually 00:05:02.670 --> 00:05:02.680 align:start position:0% built in to the theory they're actually 00:05:02.680 --> 00:05:05.420 align:start position:0% built in to the theory they're actually just<00:05:02.830> a<00:05:02.889> syntax<00:05:03.280> sugar<00:05:03.490> for<00:05:04.120> lambda<00:05:04.750> functions 00:05:05.420 --> 00:05:05.430 align:start position:0% just a syntax sugar for lambda functions 00:05:05.430 --> 00:05:07.710 align:start position:0% just a syntax sugar for lambda functions this<00:05:06.430> this<00:05:06.760> code<00:05:06.940> looks<00:05:07.060> a<00:05:07.180> little<00:05:07.270> scary<00:05:07.570> from 00:05:07.710 --> 00:05:07.720 align:start position:0% this this code looks a little scary from 00:05:07.720 --> 00:05:09.180 align:start position:0% this this code looks a little scary from a<00:05:07.810> user<00:05:07.960> perspective<00:05:08.139> which<00:05:08.560> is<00:05:08.680> why<00:05:08.800> we<00:05:08.979> built 00:05:09.180 --> 00:05:09.190 align:start position:0% a user perspective which is why we built 00:05:09.190 --> 00:05:10.650 align:start position:0% a user perspective which is why we built the<00:05:09.280> syntax<00:05:09.639> trigger<00:05:09.940> over<00:05:10.060> the<00:05:10.240> past<00:05:10.449> year 00:05:10.650 --> 00:05:10.660 align:start position:0% the syntax trigger over the past year 00:05:10.660 --> 00:05:12.689 align:start position:0% the syntax trigger over the past year but<00:05:11.650> it's<00:05:11.800> actually<00:05:12.039> a<00:05:12.070> lot<00:05:12.190> simpler<00:05:12.550> to 00:05:12.689 --> 00:05:12.699 align:start position:0% but it's actually a lot simpler to 00:05:12.699 --> 00:05:14.730 align:start position:0% but it's actually a lot simpler to implement<00:05:12.729> and<00:05:13.270> our<00:05:13.780> runtime<00:05:13.990> is<00:05:14.350> only<00:05:14.530> about 00:05:14.730 --> 00:05:14.740 align:start position:0% implement and our runtime is only about 00:05:14.740 --> 00:05:16.500 align:start position:0% implement and our runtime is only about 400<00:05:15.190> lines<00:05:15.370> long<00:05:15.610> and<00:05:15.850> our<00:05:15.910> core<00:05:16.180> language 00:05:16.500 --> 00:05:16.510 align:start position:0% 400 lines long and our core language 00:05:16.510 --> 00:05:18.659 align:start position:0% 400 lines long and our core language theory<00:05:16.780> is<00:05:16.840> only<00:05:16.990> about<00:05:17.139> 1500<00:05:17.770> we<00:05:18.430> think<00:05:18.580> it's 00:05:18.659 --> 00:05:18.669 align:start position:0% theory is only about 1500 we think it's 00:05:18.669 --> 00:05:20.010 align:start position:0% theory is only about 1500 we think it's really<00:05:18.789> important<00:05:19.240> for<00:05:19.270> portability<00:05:19.930> and 00:05:20.010 --> 00:05:20.020 align:start position:0% really important for portability and 00:05:20.020 --> 00:05:22.529 align:start position:0% really important for portability and decentralization<00:05:20.850> to<00:05:21.850> have<00:05:22.030> a<00:05:22.060> language 00:05:22.529 --> 00:05:22.539 align:start position:0% decentralization to have a language 00:05:22.539 --> 00:05:23.909 align:start position:0% decentralization to have a language that's<00:05:22.720> small<00:05:23.050> enough<00:05:23.080> that<00:05:23.410> people<00:05:23.560> can 00:05:23.909 --> 00:05:23.919 align:start position:0% that's small enough that people can 00:05:23.919 --> 00:05:25.860 align:start position:0% that's small enough that people can implement<00:05:24.639> it<00:05:24.880> or<00:05:24.970> at<00:05:25.060> least<00:05:25.090> understand<00:05:25.690> it 00:05:25.860 --> 00:05:25.870 align:start position:0% implement it or at least understand it 00:05:25.870 --> 00:05:29.100 align:start position:0% implement it or at least understand it themselves<00:05:27.180> here's<00:05:28.180> the<00:05:28.300> clean<00:05:28.449> syntax<00:05:28.840> again 00:05:29.100 --> 00:05:29.110 align:start position:0% themselves here's the clean syntax again 00:05:29.110 --> 00:05:30.390 align:start position:0% themselves here's the clean syntax again you<00:05:29.410> know<00:05:29.500> now<00:05:29.650> that<00:05:29.680> you<00:05:29.860> know<00:05:29.949> the<00:05:30.070> laminin 00:05:30.390 --> 00:05:30.400 align:start position:0% you know now that you know the laminin 00:05:30.400 --> 00:05:33.120 align:start position:0% you know now that you know the laminin codings<00:05:30.699> look<00:05:30.820> like<00:05:31.949> let's<00:05:32.949> talk<00:05:33.039> about 00:05:33.120 --> 00:05:33.130 align:start position:0% codings look like let's talk about 00:05:33.130 --> 00:05:35.100 align:start position:0% codings look like let's talk about performance<00:05:33.639> a<00:05:33.849> language<00:05:34.599> is<00:05:34.720> great<00:05:34.840> for 00:05:35.100 --> 00:05:35.110 align:start position:0% performance a language is great for 00:05:35.110 --> 00:05:36.570 align:start position:0% performance a language is great for writing<00:05:35.169> practical<00:05:35.680> software<00:05:36.039> has<00:05:36.310> to<00:05:36.340> be 00:05:36.570 --> 00:05:36.580 align:start position:0% writing practical software has to be 00:05:36.580 --> 00:05:39.180 align:start position:0% writing practical software has to be fast<00:05:37.080> while<00:05:38.080> formalities<00:05:38.530> runtime<00:05:38.889> is<00:05:39.010> still 00:05:39.180 --> 00:05:39.190 align:start position:0% fast while formalities runtime is still 00:05:39.190 --> 00:05:40.710 align:start position:0% fast while formalities runtime is still immature<00:05:39.430> the<00:05:39.880> language<00:05:40.330> has<00:05:40.449> a<00:05:40.479> lot<00:05:40.690> of 00:05:40.710 --> 00:05:40.720 align:start position:0% immature the language has a lot of 00:05:40.720 --> 00:05:41.850 align:start position:0% immature the language has a lot of features<00:05:40.930> that<00:05:41.110> we<00:05:41.320> think<00:05:41.349> will<00:05:41.560> make<00:05:41.680> it<00:05:41.740> very 00:05:41.850 --> 00:05:41.860 align:start position:0% features that we think will make it very 00:05:41.860 --> 00:05:44.430 align:start position:0% features that we think will make it very fast<00:05:42.340> in<00:05:42.520> the<00:05:42.610> long<00:05:42.760> term<00:05:43.289> interaction<00:05:44.289> that's 00:05:44.430 --> 00:05:44.440 align:start position:0% fast in the long term interaction that's 00:05:44.440 --> 00:05:46.379 align:start position:0% fast in the long term interaction that's is<00:05:44.740> a<00:05:45.099> runtime<00:05:45.520> model<00:05:45.820> and<00:05:46.000> I<00:05:46.120> think<00:05:46.300> it 00:05:46.379 --> 00:05:46.389 align:start position:0% is a runtime model and I think it 00:05:46.389 --> 00:05:47.879 align:start position:0% is a runtime model and I think it deserves<00:05:46.449> its<00:05:46.750> own<00:05:46.810> talk<00:05:47.139> since<00:05:47.590> they<00:05:47.710> allow 00:05:47.879 --> 00:05:47.889 align:start position:0% deserves its own talk since they allow 00:05:47.889 --> 00:05:49.500 align:start position:0% deserves its own talk since they allow some<00:05:48.070> really<00:05:48.430> crazy<00:05:48.610> optimizations<00:05:49.419> like 00:05:49.500 --> 00:05:49.510 align:start position:0% some really crazy optimizations like 00:05:49.510 --> 00:05:51.870 align:start position:0% some really crazy optimizations like optimal<00:05:50.349> sharing<00:05:50.800> runtime<00:05:51.250> Fusion<00:05:51.669> and 00:05:51.870 --> 00:05:51.880 align:start position:0% optimal sharing runtime Fusion and 00:05:51.880 --> 00:05:55.290 align:start position:0% optimal sharing runtime Fusion and here's<00:05:52.449> our<00:05:52.630> nice<00:05:54.060> illustration<00:05:55.060> of<00:05:55.150> what 00:05:55.290 --> 00:05:55.300 align:start position:0% here's our nice illustration of what 00:05:55.300 --> 00:05:56.580 align:start position:0% here's our nice illustration of what like<00:05:55.479> the<00:05:55.599> reduction<00:05:56.020> actually<00:05:56.289> looks<00:05:56.470> like 00:05:56.580 --> 00:05:56.590 align:start position:0% like the reduction actually looks like 00:05:56.590 --> 00:05:58.020 align:start position:0% like the reduction actually looks like and<00:05:56.770> you<00:05:56.830> can<00:05:56.860> see<00:05:57.099> the<00:05:57.190> conversion<00:05:57.639> from<00:05:57.820> a 00:05:58.020 --> 00:05:58.030 align:start position:0% and you can see the conversion from a 00:05:58.030 --> 00:06:05.750 align:start position:0% and you can see the conversion from a lambda<00:05:58.419> X<00:05:58.539> term<00:05:58.930> to<00:05:59.229> a<00:05:59.500> graph<00:05:59.770> and<00:06:00.010> then<00:06:00.130> back 00:06:05.750 --> 00:06:05.760 align:start position:0% 00:06:05.760 --> 00:06:07.980 align:start position:0% for<00:06:06.760> code<00:06:06.909> with<00:06:07.090> higher-order<00:06:07.330> lots<00:06:07.900> of 00:06:07.980 --> 00:06:07.990 align:start position:0% for code with higher-order lots of 00:06:07.990 --> 00:06:09.149 align:start position:0% for code with higher-order lots of higher-order<00:06:08.229> functions<00:06:08.680> formalities 00:06:09.149 --> 00:06:09.159 align:start position:0% higher-order functions formalities 00:06:09.159 --> 00:06:11.100 align:start position:0% higher-order functions formalities extremely<00:06:09.610> fast<00:06:09.820> right<00:06:10.090> now<00:06:10.120> but<00:06:10.930> there's 00:06:11.100 --> 00:06:11.110 align:start position:0% extremely fast right now but there's 00:06:11.110 --> 00:06:12.990 align:start position:0% extremely fast right now but there's still<00:06:11.260> substantial<00:06:11.830> overhead<00:06:12.280> which<00:06:12.820> makes 00:06:12.990 --> 00:06:13.000 align:start position:0% still substantial overhead which makes 00:06:13.000 --> 00:06:15.330 align:start position:0% still substantial overhead which makes us<00:06:13.120> only<00:06:13.270> moderately<00:06:13.930> fast<00:06:14.110> on<00:06:14.380> average<00:06:14.800> at 00:06:15.330 --> 00:06:15.340 align:start position:0% us only moderately fast on average at 00:06:15.340 --> 00:06:17.189 align:start position:0% us only moderately fast on average at the<00:06:15.490> moment<00:06:15.849> we<00:06:16.510> think<00:06:16.690> in<00:06:16.780> future<00:06:16.900> our 00:06:17.189 --> 00:06:17.199 align:start position:0% the moment we think in future our 00:06:17.199 --> 00:06:18.540 align:start position:0% the moment we think in future our interaction<00:06:17.710> that<00:06:17.830> model<00:06:18.099> will<00:06:18.190> pay<00:06:18.310> a<00:06:18.340> lot<00:06:18.520> of 00:06:18.540 --> 00:06:18.550 align:start position:0% interaction that model will pay a lot of 00:06:18.550 --> 00:06:20.310 align:start position:0% interaction that model will pay a lot of dividends<00:06:19.030> here<00:06:19.210> performance<00:06:19.990> is<00:06:20.080> really 00:06:20.310 --> 00:06:20.320 align:start position:0% dividends here performance is really 00:06:20.320 --> 00:06:22.350 align:start position:0% dividends here performance is really critical<00:06:20.889> to<00:06:21.010> us<00:06:21.159> for<00:06:21.909> getting<00:06:22.000> people<00:06:22.180> to 00:06:22.350 --> 00:06:22.360 align:start position:0% critical to us for getting people to 00:06:22.360 --> 00:06:24.270 align:start position:0% critical to us for getting people to adopt<00:06:22.539> formality<00:06:23.110> and<00:06:23.260> using<00:06:23.590> it<00:06:23.680> to<00:06:23.710> build 00:06:24.270 --> 00:06:24.280 align:start position:0% adopt formality and using it to build 00:06:24.280 --> 00:06:27.390 align:start position:0% adopt formality and using it to build lots<00:06:24.430> of<00:06:24.639> great<00:06:25.240> software<00:06:26.039> one<00:06:27.039> interesting 00:06:27.390 --> 00:06:27.400 align:start position:0% lots of great software one interesting 00:06:27.400 --> 00:06:28.860 align:start position:0% lots of great software one interesting thing<00:06:27.520> about<00:06:27.550> these<00:06:27.820> benchmarks<00:06:28.270> is<00:06:28.389> that<00:06:28.690> if 00:06:28.860 --> 00:06:28.870 align:start position:0% thing about these benchmarks is that if 00:06:28.870 --> 00:06:31.320 align:start position:0% thing about these benchmarks is that if instead<00:06:29.830> I<00:06:30.039> call<00:06:30.250> the<00:06:30.370> function<00:06:30.550> not<00:06:30.940> ten<00:06:31.240> to 00:06:31.320 --> 00:06:31.330 align:start position:0% instead I call the function not ten to 00:06:31.330 --> 00:06:33.240 align:start position:0% instead I call the function not ten to the<00:06:31.360> hundred<00:06:31.690> times<00:06:31.900> but<00:06:32.139> ten<00:06:32.380> to<00:06:32.710> the<00:06:32.830> hundred 00:06:33.240 --> 00:06:33.250 align:start position:0% the hundred times but ten to the hundred 00:06:33.250 --> 00:06:35.219 align:start position:0% the hundred times but ten to the hundred thousand<00:06:33.669> it<00:06:33.880> still<00:06:34.270> only<00:06:34.449> takes<00:06:34.840> like<00:06:35.020> 12 00:06:35.219 --> 00:06:35.229 align:start position:0% thousand it still only takes like 12 00:06:35.229 --> 00:06:37.800 align:start position:0% thousand it still only takes like 12 seconds<00:06:35.560> which<00:06:35.949> is<00:06:36.099> you<00:06:36.699> know<00:06:36.789> way<00:06:37.570> better 00:06:37.800 --> 00:06:37.810 align:start position:0% seconds which is you know way better 00:06:37.810 --> 00:06:39.450 align:start position:0% seconds which is you know way better than<00:06:38.139> I<00:06:38.380> think<00:06:38.590> pretty<00:06:39.010> much<00:06:39.130> any<00:06:39.280> other 00:06:39.450 --> 00:06:39.460 align:start position:0% than I think pretty much any other 00:06:39.460 --> 00:06:40.680 align:start position:0% than I think pretty much any other language<00:06:39.729> that<00:06:39.849> I've<00:06:39.940> used<00:06:40.120> unless<00:06:40.419> you<00:06:40.570> do 00:06:40.680 --> 00:06:40.690 align:start position:0% language that I've used unless you do 00:06:40.690 --> 00:06:42.580 align:start position:0% language that I've used unless you do like<00:06:40.840> crazy<00:06:41.080> optimizations 00:06:42.580 --> 00:06:42.590 align:start position:0% like crazy optimizations 00:06:42.590 --> 00:06:46.490 align:start position:0% like crazy optimizations here's<00:06:43.590> why<00:06:43.710> proofs<00:06:43.950> matter<00:06:45.140> here's<00:06:46.140> a<00:06:46.230> sample 00:06:46.490 --> 00:06:46.500 align:start position:0% here's why proofs matter here's a sample 00:06:46.500 --> 00:06:47.900 align:start position:0% here's why proofs matter here's a sample of<00:06:46.530> some<00:06:46.680> costly<00:06:47.070> issues<00:06:47.490> that<00:06:47.700> have<00:06:47.790> happened 00:06:47.900 --> 00:06:47.910 align:start position:0% of some costly issues that have happened 00:06:47.910 --> 00:06:49.070 align:start position:0% of some costly issues that have happened at<00:06:48.120> different<00:06:48.420> parts<00:06:48.630> of<00:06:48.690> the<00:06:48.810> stack<00:06:49.050> that 00:06:49.070 --> 00:06:49.080 align:start position:0% at different parts of the stack that 00:06:49.080 --> 00:06:50.750 align:start position:0% at different parts of the stack that perhaps<00:06:49.440> could<00:06:49.770> have<00:06:49.830> benefited<00:06:50.370> from<00:06:50.400> proofs 00:06:50.750 --> 00:06:50.760 align:start position:0% perhaps could have benefited from proofs 00:06:50.760 --> 00:06:53.120 align:start position:0% perhaps could have benefited from proofs and<00:06:50.910> type<00:06:51.060> safety<00:06:51.350> heartbleed<00:06:52.350> that's<00:06:52.890> just 00:06:53.120 --> 00:06:53.130 align:start position:0% and type safety heartbleed that's just 00:06:53.130 --> 00:06:55.970 align:start position:0% and type safety heartbleed that's just an<00:06:53.250> out<00:06:53.400> of<00:06:53.430> bounds<00:06:53.670> indexing<00:06:54.360> error<00:06:54.980> now 00:06:55.970 --> 00:06:55.980 align:start position:0% an out of bounds indexing error now 00:06:55.980 --> 00:06:57.950 align:start position:0% an out of bounds indexing error now proofs<00:06:56.640> aren't<00:06:56.850> a<00:06:56.880> silver<00:06:57.210> bullet<00:06:57.420> because 00:06:57.950 --> 00:06:57.960 align:start position:0% proofs aren't a silver bullet because 00:06:57.960 --> 00:06:59.090 align:start position:0% proofs aren't a silver bullet because all<00:06:58.080> these<00:06:58.170> issues<00:06:58.440> are<00:06:58.590> really<00:06:58.710> complicated 00:06:59.090 --> 00:06:59.100 align:start position:0% all these issues are really complicated 00:06:59.100 --> 00:07:01.910 align:start position:0% all these issues are really complicated but<00:06:59.850> if<00:07:00.030> proofs<00:07:00.540> can<00:07:00.690> reduce<00:07:01.230> the<00:07:01.410> severity<00:07:01.770> or 00:07:01.910 --> 00:07:01.920 align:start position:0% but if proofs can reduce the severity or 00:07:01.920 --> 00:07:03.590 align:start position:0% but if proofs can reduce the severity or incidence<00:07:02.430> of<00:07:02.520> these<00:07:02.670> kinds<00:07:03.030> of<00:07:03.090> errors<00:07:03.420> even 00:07:03.590 --> 00:07:03.600 align:start position:0% incidence of these kinds of errors even 00:07:03.600 --> 00:07:05.420 align:start position:0% incidence of these kinds of errors even just<00:07:03.900> a<00:07:03.960> little<00:07:04.170> bit<00:07:04.260> at<00:07:04.350> the<00:07:04.440> margin<00:07:04.800> I<00:07:04.950> think 00:07:05.420 --> 00:07:05.430 align:start position:0% just a little bit at the margin I think 00:07:05.430 --> 00:07:08.390 align:start position:0% just a little bit at the margin I think it's<00:07:05.550> worth<00:07:05.760> exploring<00:07:06.120> and<00:07:07.010> in<00:07:08.010> black<00:07:08.190> Shang 00:07:08.390 --> 00:07:08.400 align:start position:0% it's worth exploring and in black Shang 00:07:08.400 --> 00:07:09.680 align:start position:0% it's worth exploring and in black Shang I<00:07:08.490> think<00:07:08.670> it's<00:07:08.760> especially<00:07:08.970> especially 00:07:09.680 --> 00:07:09.690 align:start position:0% I think it's especially especially 00:07:09.690 --> 00:07:11.570 align:start position:0% I think it's especially especially relevant<00:07:09.960> because<00:07:10.590> the<00:07:10.710> ratio<00:07:10.860> between<00:07:11.160> code 00:07:11.570 --> 00:07:11.580 align:start position:0% relevant because the ratio between code 00:07:11.580 --> 00:07:14.600 align:start position:0% relevant because the ratio between code complexity<00:07:12.060> and<00:07:12.270> code<00:07:12.420> value<00:07:12.900> is<00:07:13.530> so<00:07:14.070> extreme 00:07:14.600 --> 00:07:14.610 align:start position:0% complexity and code value is so extreme 00:07:14.610 --> 00:07:17.240 align:start position:0% complexity and code value is so extreme here<00:07:15.360> I<00:07:15.390> just<00:07:15.750> counted<00:07:16.410> the<00:07:16.440> lines<00:07:16.650> in<00:07:17.010> you 00:07:17.240 --> 00:07:17.250 align:start position:0% here I just counted the lines in you 00:07:17.250 --> 00:07:20.780 align:start position:0% here I just counted the lines in you know<00:07:17.340> some<00:07:17.960> popular<00:07:18.960> projects<00:07:19.950> you<00:07:20.070> know<00:07:20.190> ba 00:07:20.780 --> 00:07:20.790 align:start position:0% know some popular projects you know ba 00:07:20.790 --> 00:07:24.170 align:start position:0% know some popular projects you know ba tu<00:07:21.120> SDC<00:07:21.870> and<00:07:22.080> you<00:07:22.740> know<00:07:22.830> a<00:07:23.280> lot<00:07:23.670> of<00:07:23.700> projects 00:07:24.170 --> 00:07:24.180 align:start position:0% tu SDC and you know a lot of projects 00:07:24.180 --> 00:07:25.910 align:start position:0% tu SDC and you know a lot of projects are<00:07:24.330> running<00:07:24.930> at<00:07:25.020> about<00:07:25.110> a<00:07:25.230> million<00:07:25.560> line<00:07:25.890> a 00:07:25.910 --> 00:07:25.920 align:start position:0% are running at about a million line a 00:07:25.920 --> 00:07:27.860 align:start position:0% are running at about a million line a million<00:07:26.400> dollars<00:07:26.760> of<00:07:26.970> capital<00:07:27.150> per<00:07:27.510> lines<00:07:27.690> of 00:07:27.860 --> 00:07:27.870 align:start position:0% million dollars of capital per lines of 00:07:27.870 --> 00:07:29.660 align:start position:0% million dollars of capital per lines of code<00:07:28.050> so<00:07:28.560> I<00:07:28.590> think<00:07:28.740> it's<00:07:28.920> really<00:07:29.160> important 00:07:29.660 --> 00:07:29.670 align:start position:0% code so I think it's really important 00:07:29.670 --> 00:07:31.370 align:start position:0% code so I think it's really important that<00:07:30.030> if<00:07:30.240> you're<00:07:30.390> writing<00:07:30.750> projects<00:07:31.230> like 00:07:31.370 --> 00:07:31.380 align:start position:0% that if you're writing projects like 00:07:31.380 --> 00:07:32.960 align:start position:0% that if you're writing projects like that<00:07:31.560> it's<00:07:31.800> you<00:07:32.190> should<00:07:32.370> put<00:07:32.520> a<00:07:32.550> little<00:07:32.700> extra 00:07:32.960 --> 00:07:32.970 align:start position:0% that it's you should put a little extra 00:07:32.970 --> 00:07:34.460 align:start position:0% that it's you should put a little extra effort<00:07:33.330> in<00:07:33.480> trying<00:07:33.780> to<00:07:33.930> make<00:07:34.050> sure<00:07:34.170> that<00:07:34.320> the 00:07:34.460 --> 00:07:34.470 align:start position:0% effort in trying to make sure that the 00:07:34.470 --> 00:07:35.930 align:start position:0% effort in trying to make sure that the lines<00:07:34.620> of<00:07:34.770> code<00:07:34.920> are<00:07:35.100> actually<00:07:35.640> the<00:07:35.730> correct 00:07:35.930 --> 00:07:35.940 align:start position:0% lines of code are actually the correct 00:07:35.940 --> 00:07:40.010 align:start position:0% lines of code are actually the correct lines<00:07:36.210> of<00:07:36.360> code<00:07:37.970> one<00:07:38.970> criticism<00:07:39.360> of<00:07:39.630> proofs<00:07:39.870> is 00:07:40.010 --> 00:07:40.020 align:start position:0% lines of code one criticism of proofs is 00:07:40.020 --> 00:07:41.360 align:start position:0% lines of code one criticism of proofs is that<00:07:40.230> they<00:07:40.350> pass<00:07:40.530> responsibility<00:07:41.220> for 00:07:41.360 --> 00:07:41.370 align:start position:0% that they pass responsibility for 00:07:41.370 --> 00:07:43.250 align:start position:0% that they pass responsibility for correctness<00:07:41.670> to<00:07:41.910> the<00:07:42.000> specification<00:07:42.720> rather 00:07:43.250 --> 00:07:43.260 align:start position:0% correctness to the specification rather 00:07:43.260 --> 00:07:44.570 align:start position:0% correctness to the specification rather than<00:07:43.500> the<00:07:43.590> implementation<00:07:44.160> and<00:07:44.280> you<00:07:44.370> still 00:07:44.570 --> 00:07:44.580 align:start position:0% than the implementation and you still 00:07:44.580 --> 00:07:45.950 align:start position:0% than the implementation and you still have<00:07:44.700> to<00:07:44.790> audit<00:07:44.970> it<00:07:45.180> and<00:07:45.330> that's<00:07:45.660> completely 00:07:45.950 --> 00:07:45.960 align:start position:0% have to audit it and that's completely 00:07:45.960 --> 00:07:47.660 align:start position:0% have to audit it and that's completely true<00:07:46.320> like<00:07:46.560> it<00:07:46.680> doesn't<00:07:46.950> this<00:07:47.130> proofs<00:07:47.490> don't 00:07:47.660 --> 00:07:47.670 align:start position:0% true like it doesn't this proofs don't 00:07:47.670 --> 00:07:49.460 align:start position:0% true like it doesn't this proofs don't solve<00:07:47.880> having<00:07:48.240> to<00:07:48.330> actually<00:07:48.480> think<00:07:49.260> about 00:07:49.460 --> 00:07:49.470 align:start position:0% solve having to actually think about 00:07:49.470 --> 00:07:51.080 align:start position:0% solve having to actually think about your<00:07:49.590> code<00:07:49.740> and<00:07:49.920> reason<00:07:50.220> reason<00:07:50.760> that<00:07:51.000> is 00:07:51.080 --> 00:07:51.090 align:start position:0% your code and reason reason that is 00:07:51.090 --> 00:07:53.300 align:start position:0% your code and reason reason that is correct<00:07:51.450> and<00:07:52.350> if<00:07:52.470> you're<00:07:52.590> type<00:07:52.770> spec<00:07:52.980> is<00:07:53.100> bad 00:07:53.300 --> 00:07:53.310 align:start position:0% correct and if you're type spec is bad 00:07:53.310 --> 00:07:55.550 align:start position:0% correct and if you're type spec is bad then<00:07:53.580> you'd<00:07:53.730> proofs<00:07:53.970> don't<00:07:54.240> help<00:07:54.420> you<00:07:54.560> but 00:07:55.550 --> 00:07:55.560 align:start position:0% then you'd proofs don't help you but 00:07:55.560 --> 00:07:57.980 align:start position:0% then you'd proofs don't help you but type<00:07:56.220> specifications<00:07:56.970> can<00:07:57.150> be<00:07:57.270> much<00:07:57.630> simpler 00:07:57.980 --> 00:07:57.990 align:start position:0% type specifications can be much simpler 00:07:57.990 --> 00:07:59.780 align:start position:0% type specifications can be much simpler than<00:07:58.140> the<00:07:58.260> code<00:07:58.410> they're<00:07:58.560> typing<00:07:58.920> and<00:07:59.640> at 00:07:59.780 --> 00:07:59.790 align:start position:0% than the code they're typing and at 00:07:59.790 --> 00:08:01.250 align:start position:0% than the code they're typing and at worst<00:08:00.030> act<00:08:00.300> like<00:08:00.450> a<00:08:00.480> compiler<00:08:01.080> check 00:08:01.250 --> 00:08:01.260 align:start position:0% worst act like a compiler check 00:08:01.260 --> 00:08:03.020 align:start position:0% worst act like a compiler check documentation<00:08:01.950> here's<00:08:02.520> a<00:08:02.580> little<00:08:02.820> snippet 00:08:03.020 --> 00:08:03.030 align:start position:0% documentation here's a little snippet 00:08:03.030 --> 00:08:08.120 align:start position:0% documentation here's a little snippet from<00:08:03.780> our<00:08:04.080> er<00:08:04.800> C<00:08:04.950> 20<00:08:05.300> implementation<00:08:06.300> and<00:08:07.130> you 00:08:08.120 --> 00:08:08.130 align:start position:0% from our er C 20 implementation and you 00:08:08.130 --> 00:08:09.680 align:start position:0% from our er C 20 implementation and you can<00:08:08.280> see<00:08:08.430> that<00:08:08.640> like<00:08:08.790> if<00:08:09.090> we<00:08:09.330> that<00:08:09.540> we<00:08:09.660> have 00:08:09.680 --> 00:08:09.690 align:start position:0% can see that like if we that we have 00:08:09.690 --> 00:08:11.330 align:start position:0% can see that like if we that we have this<00:08:10.020> type<00:08:10.260> specification<00:08:10.920> that<00:08:11.040> says<00:08:11.160> I<00:08:11.220> have 00:08:11.330 --> 00:08:11.340 align:start position:0% this type specification that says I have 00:08:11.340 --> 00:08:13.220 align:start position:0% this type specification that says I have a<00:08:11.400> transfer<00:08:11.790> function<00:08:11.820> I<00:08:12.330> have<00:08:12.540> the<00:08:12.810> approvals 00:08:13.220 --> 00:08:13.230 align:start position:0% a transfer function I have the approvals 00:08:13.230 --> 00:08:14.630 align:start position:0% a transfer function I have the approvals have<00:08:13.380> to<00:08:13.470> be<00:08:13.560> in<00:08:13.650> an<00:08:13.770> old<00:08:13.920> state<00:08:14.190> that<00:08:14.340> has<00:08:14.520> to 00:08:14.630 --> 00:08:14.640 align:start position:0% have to be in an old state that has to 00:08:14.640 --> 00:08:16.820 align:start position:0% have to be in an old state that has to be<00:08:14.730> removed<00:08:14.940> from<00:08:15.090> a<00:08:15.210> new<00:08:15.330> state<00:08:15.540> and<00:08:15.750> it<00:08:16.680> has 00:08:16.820 --> 00:08:16.830 align:start position:0% be removed from a new state and it has 00:08:16.830 --> 00:08:17.840 align:start position:0% be removed from a new state and it has to<00:08:16.950> obey<00:08:17.040> a<00:08:17.160> double<00:08:17.460> entry<00:08:17.610> bookkeeping 00:08:17.840 --> 00:08:17.850 align:start position:0% to obey a double entry bookkeeping 00:08:17.850 --> 00:08:19.730 align:start position:0% to obey a double entry bookkeeping environment<00:08:18.570> you<00:08:18.960> don't<00:08:19.110> even<00:08:19.230> need<00:08:19.440> to<00:08:19.500> see 00:08:19.730 --> 00:08:19.740 align:start position:0% environment you don't even need to see 00:08:19.740 --> 00:08:21.140 align:start position:0% environment you don't even need to see the<00:08:19.860> implementation<00:08:20.070> to<00:08:20.610> know<00:08:20.760> that<00:08:20.970> if<00:08:21.060> it 00:08:21.140 --> 00:08:21.150 align:start position:0% the implementation to know that if it 00:08:21.150 --> 00:08:22.670 align:start position:0% the implementation to know that if it type<00:08:21.360> checks<00:08:21.660> those<00:08:21.840> properties<00:08:22.410> that<00:08:22.530> it's 00:08:22.670 --> 00:08:22.680 align:start position:0% type checks those properties that it's 00:08:22.680 --> 00:08:24.860 align:start position:0% type checks those properties that it's going<00:08:22.890> to<00:08:23.010> long<00:08:23.820> as<00:08:23.940> the<00:08:24.030> compilers<00:08:24.480> valid 00:08:24.860 --> 00:08:24.870 align:start position:0% going to long as the compilers valid 00:08:24.870 --> 00:08:26.750 align:start position:0% going to long as the compilers valid that<00:08:25.290> it's<00:08:25.440> going<00:08:25.620> to<00:08:25.710> be<00:08:25.860> safe<00:08:26.130> according<00:08:26.670> to 00:08:26.750 --> 00:08:26.760 align:start position:0% that it's going to be safe according to 00:08:26.760 --> 00:08:29.330 align:start position:0% that it's going to be safe according to those<00:08:26.850> properties<00:08:27.710> the<00:08:28.710> vision<00:08:29.010> is<00:08:29.130> to<00:08:29.250> have 00:08:29.330 --> 00:08:29.340 align:start position:0% those properties the vision is to have 00:08:29.340 --> 00:08:30.740 align:start position:0% those properties the vision is to have formality<00:08:29.820> be<00:08:29.940> a<00:08:29.970> language<00:08:30.180> that<00:08:30.480> can<00:08:30.540> add 00:08:30.740 --> 00:08:30.750 align:start position:0% formality be a language that can add 00:08:30.750 --> 00:08:32.810 align:start position:0% formality be a language that can add type<00:08:31.050> safety<00:08:31.350> at<00:08:31.680> every<00:08:32.310> layer<00:08:32.430> of<00:08:32.490> the<00:08:32.760> stack 00:08:32.810 --> 00:08:32.820 align:start position:0% type safety at every layer of the stack 00:08:32.820 --> 00:08:34.640 align:start position:0% type safety at every layer of the stack having<00:08:33.719> the<00:08:33.810> same<00:08:33.960> language<00:08:34.260> every<00:08:34.469> matter 00:08:34.640 --> 00:08:34.650 align:start position:0% having the same language every matter 00:08:34.650 --> 00:08:36.110 align:start position:0% having the same language every matter means<00:08:35.130> that<00:08:35.250> you<00:08:35.310> can<00:08:35.460> use<00:08:35.580> the<00:08:35.700> same<00:08:35.849> types 00:08:36.110 --> 00:08:36.120 align:start position:0% means that you can use the same types 00:08:36.120 --> 00:08:37.880 align:start position:0% means that you can use the same types everywhere<00:08:36.539> with<00:08:36.960> minimal<00:08:37.320> friction<00:08:37.440> and 00:08:37.880 --> 00:08:37.890 align:start position:0% everywhere with minimal friction and 00:08:37.890 --> 00:08:39.409 align:start position:0% everywhere with minimal friction and this<00:08:38.370> is<00:08:38.430> what's<00:08:38.550> awesome<00:08:38.700> about<00:08:38.910> having<00:08:39.360> a 00:08:39.409 --> 00:08:39.419 align:start position:0% this is what's awesome about having a 00:08:39.419 --> 00:08:41.690 align:start position:0% this is what's awesome about having a 400<00:08:39.960> line<00:08:40.140> language<00:08:40.620> implementation<00:08:41.250> we<00:08:41.669> can 00:08:41.690 --> 00:08:41.700 align:start position:0% 400 line language implementation we can 00:08:41.700 --> 00:08:42.860 align:start position:0% 400 line language implementation we can have<00:08:41.910> the<00:08:42.000> same<00:08:42.150> language<00:08:42.419> infrastructure 00:08:42.860 --> 00:08:42.870 align:start position:0% have the same language infrastructure 00:08:42.870 --> 00:08:44.780 align:start position:0% have the same language infrastructure running<00:08:43.229> inside<00:08:43.440> a<00:08:43.500> web<00:08:43.710> app<00:08:43.890> smart<00:08:44.340> contract 00:08:44.780 --> 00:08:44.790 align:start position:0% running inside a web app smart contract 00:08:44.790 --> 00:08:49.300 align:start position:0% running inside a web app smart contract server<00:08:45.380> editor<00:08:46.380> plug-in<00:08:46.740> or<00:08:46.920> our<00:08:47.340> test<00:08:47.550> suite 00:08:49.300 --> 00:08:49.310 align:start position:0% server editor plug-in or our test suite 00:08:49.310 --> 00:08:51.620 align:start position:0% server editor plug-in or our test suite our<00:08:50.310> next<00:08:50.550> big<00:08:50.700> priority<00:08:51.270> now<00:08:51.390> that<00:08:51.420> the 00:08:51.620 --> 00:08:51.630 align:start position:0% our next big priority now that the 00:08:51.630 --> 00:08:53.329 align:start position:0% our next big priority now that the language<00:08:51.960> is<00:08:52.080> pretty<00:08:52.200> stable<00:08:52.500> is<00:08:52.800> to<00:08:53.160> write 00:08:53.329 --> 00:08:53.339 align:start position:0% language is pretty stable is to write 00:08:53.339 --> 00:08:54.740 align:start position:0% language is pretty stable is to write the<00:08:53.460> compilers<00:08:54.000> that<00:08:54.150> will<00:08:54.240> let<00:08:54.360> us<00:08:54.390> deploy 00:08:54.740 --> 00:08:54.750 align:start position:0% the compilers that will let us deploy 00:08:54.750 --> 00:08:55.550 align:start position:0% the compilers that will let us deploy formality<00:08:55.290> smart 00:08:55.550 --> 00:08:55.560 align:start position:0% formality smart 00:08:55.560 --> 00:08:57.500 align:start position:0% formality smart contracts<00:08:55.920> and<00:08:56.190> to<00:08:56.400> continue<00:08:56.730> maturing<00:08:57.420> the 00:08:57.500 --> 00:08:57.510 align:start position:0% contracts and to continue maturing the 00:08:57.510 --> 00:08:59.330 align:start position:0% contracts and to continue maturing the library's<00:08:57.900> tools<00:08:58.170> and<00:08:58.380> Docs<00:08:58.560> to<00:08:59.010> make<00:08:59.160> that<00:08:59.310> a 00:08:59.330 --> 00:08:59.340 align:start position:0% library's tools and Docs to make that a 00:08:59.340 --> 00:09:01.910 align:start position:0% library's tools and Docs to make that a really<00:08:59.670> great<00:08:59.850> user<00:09:00.060> experience<00:09:00.630> after<00:09:01.110> that 00:09:01.910 --> 00:09:01.920 align:start position:0% really great user experience after that 00:09:01.920 --> 00:09:03.590 align:start position:0% really great user experience after that implementing<00:09:02.430> formality<00:09:02.880> in<00:09:02.970> itself<00:09:03.270> will 00:09:03.590 --> 00:09:03.600 align:start position:0% implementing formality in itself will 00:09:03.600 --> 00:09:05.060 align:start position:0% implementing formality in itself will improve<00:09:03.840> portability<00:09:04.380> even<00:09:04.590> further<00:09:04.830> and 00:09:05.060 --> 00:09:05.070 align:start position:0% improve portability even further and 00:09:05.070 --> 00:09:06.380 align:start position:0% improve portability even further and we're<00:09:05.220> gonna<00:09:05.310> see<00:09:05.520> how<00:09:05.610> fast<00:09:05.820> we<00:09:05.940> can<00:09:06.029> push<00:09:06.240> the 00:09:06.380 --> 00:09:06.390 align:start position:0% we're gonna see how fast we can push the 00:09:06.390 --> 00:09:09.350 align:start position:0% we're gonna see how fast we can push the existing<00:09:06.750> C<00:09:06.900> implementation<00:09:08.240> the<00:09:09.240> two 00:09:09.350 --> 00:09:09.360 align:start position:0% existing C implementation the two 00:09:09.360 --> 00:09:10.519 align:start position:0% existing C implementation the two projects<00:09:09.690> after<00:09:09.779> that<00:09:09.990> are<00:09:10.110> going<00:09:10.200> to<00:09:10.290> be<00:09:10.380> our 00:09:10.519 --> 00:09:10.529 align:start position:0% projects after that are going to be our 00:09:10.529 --> 00:09:11.960 align:start position:0% projects after that are going to be our package<00:09:10.830> management<00:09:11.130> infrastructure<00:09:11.670> and 00:09:11.960 --> 00:09:11.970 align:start position:0% package management infrastructure and 00:09:11.970 --> 00:09:13.400 align:start position:0% package management infrastructure and putting<00:09:12.210> the<00:09:12.270> formality<00:09:12.660> type<00:09:12.839> checker<00:09:13.080> on<00:09:13.200> an 00:09:13.400 --> 00:09:13.410 align:start position:0% putting the formality type checker on an 00:09:13.410 --> 00:09:16.400 align:start position:0% putting the formality type checker on an aetherium<00:09:13.830> contract<00:09:14.570> that<00:09:15.570> enables<00:09:16.230> us<00:09:16.350> to 00:09:16.400 --> 00:09:16.410 align:start position:0% aetherium contract that enables us to 00:09:16.410 --> 00:09:18.170 align:start position:0% aetherium contract that enables us to build<00:09:16.589> a<00:09:16.680> completely<00:09:17.070> trustless<00:09:17.670> marketplace 00:09:18.170 --> 00:09:18.180 align:start position:0% build a completely trustless marketplace 00:09:18.180 --> 00:09:20.030 align:start position:0% build a completely trustless marketplace for<00:09:18.390> code<00:09:18.570> and<00:09:18.720> proofs<00:09:18.960> you<00:09:19.589> can<00:09:19.710> submit<00:09:19.980> a 00:09:20.030 --> 00:09:20.040 align:start position:0% for code and proofs you can submit a 00:09:20.040 --> 00:09:21.829 align:start position:0% for code and proofs you can submit a formality<00:09:20.400> type<00:09:20.730> to<00:09:20.910> a<00:09:20.940> contract<00:09:21.450> along<00:09:21.660> with 00:09:21.829 --> 00:09:21.839 align:start position:0% formality type to a contract along with 00:09:21.839 --> 00:09:23.030 align:start position:0% formality type to a contract along with a<00:09:21.870> bounty<00:09:22.230> for<00:09:22.380> the<00:09:22.440> first<00:09:22.680> valid 00:09:23.030 --> 00:09:23.040 align:start position:0% a bounty for the first valid 00:09:23.040 --> 00:09:24.650 align:start position:0% a bounty for the first valid implementation<00:09:23.580> of<00:09:23.670> that<00:09:23.700> type<00:09:23.970> and<00:09:24.210> then 00:09:24.650 --> 00:09:24.660 align:start position:0% implementation of that type and then 00:09:24.660 --> 00:09:25.940 align:start position:0% implementation of that type and then anyone<00:09:24.990> in<00:09:25.080> the<00:09:25.170> world<00:09:25.260> can<00:09:25.500> claim<00:09:25.740> the<00:09:25.860> bounty 00:09:25.940 --> 00:09:25.950 align:start position:0% anyone in the world can claim the bounty 00:09:25.950 --> 00:09:27.980 align:start position:0% anyone in the world can claim the bounty just<00:09:26.310> by<00:09:26.400> submitting<00:09:26.670> the<00:09:26.820> code<00:09:27.029> no<00:09:27.690> human 00:09:27.980 --> 00:09:27.990 align:start position:0% just by submitting the code no human 00:09:27.990 --> 00:09:29.750 align:start position:0% just by submitting the code no human interaction<00:09:28.200> required<00:09:28.680> if<00:09:28.980> it<00:09:29.400> passes<00:09:29.580> the 00:09:29.750 --> 00:09:29.760 align:start position:0% interaction required if it passes the 00:09:29.760 --> 00:09:33.440 align:start position:0% interaction required if it passes the type<00:09:29.910> checker<00:09:30.150> you<00:09:30.690> get<00:09:30.870> paid<00:09:32.390> and<00:09:33.390> that's 00:09:33.440 --> 00:09:33.450 align:start position:0% type checker you get paid and that's 00:09:33.450 --> 00:09:35.660 align:start position:0% type checker you get paid and that's formality<00:09:34.020> Thanks<00:09:34.770> happy<00:09:35.430> to<00:09:35.520> take<00:09:35.610> any 00:09:35.660 --> 00:09:35.670 align:start position:0% formality Thanks happy to take any 00:09:35.670 --> 00:09:37.310 align:start position:0% formality Thanks happy to take any questions<00:09:36.300> I<00:09:36.570> don't<00:09:36.720> think<00:09:36.870> I<00:09:36.930> have<00:09:37.020> any<00:09:37.140> time 00:09:37.310 --> 00:09:37.320 align:start position:0% questions I don't think I have any time 00:09:37.320 --> 00:09:40.050 align:start position:0% questions I don't think I have any time okay 00:09:40.050 --> 00:09:40.060 align:start position:0% 00:09:40.060 --> 00:09:43.180 align:start position:0% [Applause]