WEBVTT
Kind: captions
Language: en

00:00:00.030 --> 00:00:02.180 align:start position:0%
 
in<00:00:00.930><c> the</c><00:00:01.079><c> same</c><00:00:01.260><c> way</c><00:00:01.380><c> computers</c><00:00:01.920><c> the</c><00:00:02.159><c> internet</c>

00:00:02.180 --> 00:00:02.190 align:start position:0%
in the same way computers the internet
 

00:00:02.190 --> 00:00:04.579 align:start position:0%
in the same way computers the internet
and<00:00:02.700><c> smartphones</c><00:00:03.030><c> gave</c><00:00:03.810><c> us</c><00:00:04.080><c> new</c><00:00:04.380><c> ways</c><00:00:04.529><c> to</c>

00:00:04.579 --> 00:00:04.589 align:start position:0%
and smartphones gave us new ways to
 

00:00:04.589 --> 00:00:06.829 align:start position:0%
and smartphones gave us new ways to
interactive<00:00:05.160><c> software</c><00:00:05.430><c> we</c><00:00:06.240><c> believe</c><00:00:06.509><c> a</c><00:00:06.660><c> new</c>

00:00:06.829 --> 00:00:06.839 align:start position:0%
interactive software we believe a new
 

00:00:06.839 --> 00:00:10.480 align:start position:0%
interactive software we believe a new
era<00:00:07.109><c> of</c><00:00:07.350><c> crypto</c><00:00:07.859><c> browsers</c><00:00:08.280><c> is</c><00:00:08.460><c> about</c><00:00:08.730><c> to</c><00:00:08.940><c> begin</c>

00:00:10.480 --> 00:00:10.490 align:start position:0%
era of crypto browsers is about to begin
 

00:00:10.490 --> 00:00:13.280 align:start position:0%
era of crypto browsers is about to begin
the<00:00:11.490><c> moon</c><00:00:11.670><c> project</c><00:00:12.090><c> is</c><00:00:12.300><c> our</c><00:00:12.630><c> attempt</c><00:00:13.170><c> at</c>

00:00:13.280 --> 00:00:13.290 align:start position:0%
the moon project is our attempt at
 

00:00:13.290 --> 00:00:15.860 align:start position:0%
the moon project is our attempt at
finding<00:00:13.650><c> the</c><00:00:14.009><c> best</c><00:00:14.160><c> user</c><00:00:14.580><c> experience</c><00:00:15.240><c> for</c><00:00:15.809><c> a</c>

00:00:15.860 --> 00:00:15.870 align:start position:0%
finding the best user experience for a
 

00:00:15.870 --> 00:00:19.099 align:start position:0%
finding the best user experience for a
children<00:00:16.199><c> okay</c><00:00:17.570><c> okay</c>

00:00:19.099 --> 00:00:19.109 align:start position:0%
children okay okay
 

00:00:19.109 --> 00:00:24.650 align:start position:0%
children okay okay
this<00:00:19.560><c> is</c><00:00:20.779><c> example</c><00:00:21.779><c> tap</c><00:00:22.140><c> on</c><00:00:22.590><c> moon</c><00:00:22.890><c> browser</c><00:00:23.660><c> the</c>

00:00:24.650 --> 00:00:24.660 align:start position:0%
this is example tap on moon browser the
 

00:00:24.660 --> 00:00:29.089 align:start position:0%
this is example tap on moon browser the
browser<00:00:24.689><c> is</c><00:00:27.140><c> just</c><00:00:28.140><c> looks</c><00:00:28.349><c> like</c><00:00:28.439><c> a</c><00:00:28.590><c> normal</c><00:00:28.800><c> web</c>

00:00:29.089 --> 00:00:29.099 align:start position:0%
browser is just looks like a normal web
 

00:00:29.099 --> 00:00:30.890 align:start position:0%
browser is just looks like a normal web
browser<00:00:29.369><c> but</c><00:00:29.670><c> it</c><00:00:30.000><c> has</c><00:00:30.179><c> three</c><00:00:30.630><c> major</c>

00:00:30.890 --> 00:00:30.900 align:start position:0%
browser but it has three major
 

00:00:30.900 --> 00:00:32.959 align:start position:0%
browser but it has three major
differences<00:00:31.529><c> there</c><00:00:32.099><c> which</c><00:00:32.309><c> are</c><00:00:32.460><c> represented</c>

00:00:32.959 --> 00:00:32.969 align:start position:0%
differences there which are represented
 

00:00:32.969 --> 00:00:35.150 align:start position:0%
differences there which are represented
by<00:00:33.090><c> those</c><00:00:33.239><c> three</c><00:00:33.780><c> buttons</c><00:00:34.380><c> on</c><00:00:34.680><c> the</c><00:00:34.860><c> upper</c>

00:00:35.150 --> 00:00:35.160 align:start position:0%
by those three buttons on the upper
 

00:00:35.160 --> 00:00:38.389 align:start position:0%
by those three buttons on the upper
right<00:00:35.399><c> corner</c><00:00:36.260><c> first</c><00:00:37.260><c> instead</c><00:00:37.649><c> of</c><00:00:37.710><c> normal</c>

00:00:38.389 --> 00:00:38.399 align:start position:0%
right corner first instead of normal
 

00:00:38.399 --> 00:00:40.819 align:start position:0%
right corner first instead of normal
accounts<00:00:38.790><c> and</c><00:00:38.940><c> passwords</c><00:00:39.739><c> everything</c><00:00:40.739><c> is</c>

00:00:40.819 --> 00:00:40.829 align:start position:0%
accounts and passwords everything is
 

00:00:40.829 --> 00:00:45.889 align:start position:0%
accounts and passwords everything is
based<00:00:41.070><c> on</c><00:00:42.170><c> crypto</c><00:00:43.170><c> signatures</c><00:00:44.070><c> right</c><00:00:44.899><c> so</c>

00:00:45.889 --> 00:00:45.899 align:start position:0%
based on crypto signatures right so
 

00:00:45.899 --> 00:00:49.910 align:start position:0%
based on crypto signatures right so
first<00:00:46.760><c> like</c><00:00:47.760><c> a</c><00:00:47.820><c> mist</c><00:00:48.120><c> you</c><00:00:48.660><c> can</c><00:00:48.690><c> just</c><00:00:49.379><c> store</c>

00:00:49.910 --> 00:00:49.920 align:start position:0%
first like a mist you can just store
 

00:00:49.920 --> 00:00:51.410 align:start position:0%
first like a mist you can just store
your<00:00:50.100><c> assets</c><00:00:50.430><c> here</c><00:00:50.670><c> you</c><00:00:50.850><c> can</c><00:00:51.030><c> manage</c><00:00:51.210><c> them</c>

00:00:51.410 --> 00:00:51.420 align:start position:0%
your assets here you can manage them
 

00:00:51.420 --> 00:00:55.430 align:start position:0%
your assets here you can manage them
without<00:00:51.870><c> a</c><00:00:51.899><c> bank</c><00:00:52.170><c> and</c><00:00:52.969><c> but</c><00:00:53.969><c> really</c><00:00:54.960><c> nothing</c><00:00:55.199><c> of</c>

00:00:55.430 --> 00:00:55.440 align:start position:0%
without a bank and but really nothing of
 

00:00:55.440 --> 00:00:58.580 align:start position:0%
without a bank and but really nothing of
this<00:00:55.559><c> is</c><00:00:55.770><c> no</c><00:00:56.160><c> so</c><00:00:56.820><c> let's</c><00:00:57.420><c> move</c><00:00:57.600><c> on</c><00:00:57.809><c> yes</c><00:00:58.289><c> this</c><00:00:58.469><c> is</c>

00:00:58.580 --> 00:00:58.590 align:start position:0%
this is no so let's move on yes this is
 

00:00:58.590 --> 00:01:00.290 align:start position:0%
this is no so let's move on yes this is
not<00:00:58.739><c> really</c><00:00:59.100><c> new</c><00:00:59.129><c> because</c><00:00:59.489><c> miss</c><00:00:59.789><c> does</c><00:01:00.090><c> that</c>

00:01:00.290 --> 00:01:00.300 align:start position:0%
not really new because miss does that
 

00:01:00.300 --> 00:01:04.899 align:start position:0%
not really new because miss does that
alright<00:01:00.719><c> but</c><00:01:01.530><c> imagine</c><00:01:02.520><c> if</c><00:01:02.899><c> you</c><00:01:03.899><c> could</c><00:01:04.170><c> fork</c><00:01:04.530><c> an</c>

00:01:04.899 --> 00:01:04.909 align:start position:0%
alright but imagine if you could fork an
 

00:01:04.909 --> 00:01:07.640 align:start position:0%
alright but imagine if you could fork an
application<00:01:05.909><c> in</c><00:01:06.090><c> a</c><00:01:06.210><c> single</c><00:01:06.510><c> click</c><00:01:06.720><c> not</c><00:01:07.409><c> just</c>

00:01:07.640 --> 00:01:07.650 align:start position:0%
application in a single click not just
 

00:01:07.650 --> 00:01:10.010 align:start position:0%
application in a single click not just
the<00:01:07.770><c> front</c><00:01:07.950><c> end</c><00:01:08.250><c> not</c><00:01:08.640><c> just</c><00:01:08.880><c> a</c><00:01:09.000><c> interface</c><00:01:09.570><c> not</c>

00:01:10.010 --> 00:01:10.020 align:start position:0%
the front end not just a interface not
 

00:01:10.020 --> 00:01:12.620 align:start position:0%
the front end not just a interface not
just<00:01:10.229><c> a</c><00:01:10.290><c> video</c><00:01:10.590><c> the</c><00:01:11.100><c> entire</c><00:01:11.520><c> company</c><00:01:12.210><c> in</c><00:01:12.479><c> a</c>

00:01:12.620 --> 00:01:12.630 align:start position:0%
just a video the entire company in a
 

00:01:12.630 --> 00:01:15.969 align:start position:0%
just a video the entire company in a
single<00:01:12.990><c> click</c><00:01:13.170><c> imagine</c><00:01:13.860><c> if</c><00:01:14.040><c> you</c><00:01:14.189><c> called</c><00:01:14.659><c> fork</c>

00:01:15.969 --> 00:01:15.979 align:start position:0%
single click imagine if you called fork
 

00:01:15.979 --> 00:01:19.940 align:start position:0%
single click imagine if you called fork
YouTube<00:01:16.979><c> in</c><00:01:17.939><c> a</c><00:01:18.060><c> single</c><00:01:18.420><c> click</c><00:01:18.650><c> that's</c><00:01:19.650><c> what</c>

00:01:19.940 --> 00:01:19.950 align:start position:0%
YouTube in a single click that's what
 

00:01:19.950 --> 00:01:22.429 align:start position:0%
YouTube in a single click that's what
the<00:01:20.070><c> fork</c><00:01:20.310><c> button</c><00:01:20.580><c> above</c><00:01:21.119><c> there</c><00:01:21.420><c> does</c><00:01:22.170><c> and</c>

00:01:22.429 --> 00:01:22.439 align:start position:0%
the fork button above there does and
 

00:01:22.439 --> 00:01:27.469 align:start position:0%
the fork button above there does and
that's<00:01:22.740><c> one</c><00:01:22.950><c> of</c><00:01:23.159><c> the</c><00:01:23.400><c> difference</c><00:01:24.000><c> we</c><00:01:24.420><c> have</c><00:01:26.479><c> so</c>

00:01:27.469 --> 00:01:27.479 align:start position:0%
that's one of the difference we have so
 

00:01:27.479 --> 00:01:33.410 align:start position:0%
that's one of the difference we have so
now<00:01:27.950><c> if</c><00:01:28.950><c> we</c><00:01:29.369><c> are</c><00:01:30.000><c> outside</c><00:01:31.189><c> if</c><00:01:32.189><c> we</c><00:01:32.820><c> want</c><00:01:33.090><c> to</c>

00:01:33.410 --> 00:01:33.420 align:start position:0%
now if we are outside if we want to
 

00:01:33.420 --> 00:01:36.140 align:start position:0%
now if we are outside if we want to
store<00:01:33.659><c> real</c><00:01:34.110><c> money</c><00:01:34.409><c> on</c><00:01:34.619><c> apps</c><00:01:34.860><c> then</c><00:01:35.610><c> we</c><00:01:36.000><c> need</c>

00:01:36.140 --> 00:01:36.150 align:start position:0%
store real money on apps then we need
 

00:01:36.150 --> 00:01:39.080 align:start position:0%
store real money on apps then we need
something<00:01:36.630><c> else</c><00:01:36.930><c> than</c><00:01:37.680><c> JavaScript</c><00:01:38.640><c> like</c>

00:01:39.080 --> 00:01:39.090 align:start position:0%
something else than JavaScript like
 

00:01:39.090 --> 00:01:42.080 align:start position:0%
something else than JavaScript like
languages<00:01:39.659><c> which</c><00:01:40.229><c> are</c><00:01:40.409><c> not</c><00:01:40.979><c> enough</c><00:01:41.250><c> anymore</c>

00:01:42.080 --> 00:01:42.090 align:start position:0%
languages which are not enough anymore
 

00:01:42.090 --> 00:01:45.649 align:start position:0%
languages which are not enough anymore
really<00:01:42.890><c> the</c><00:01:43.890><c> tabs</c><00:01:44.250><c> need</c><00:01:44.790><c> a</c><00:01:45.060><c> formal</c>

00:01:45.649 --> 00:01:45.659 align:start position:0%
really the tabs need a formal
 

00:01:45.659 --> 00:01:47.929 align:start position:0%
really the tabs need a formal
specification<00:01:46.159><c> something</c><00:01:47.159><c> that</c><00:01:47.399><c> tells</c><00:01:47.670><c> us</c>

00:01:47.929 --> 00:01:47.939 align:start position:0%
specification something that tells us
 

00:01:47.939 --> 00:01:52.460 align:start position:0%
specification something that tells us
that<00:01:49.280><c> states</c><00:01:50.280><c> in</c><00:01:50.610><c> cold</c><00:01:50.909><c> actually</c><00:01:51.470><c> everything</c>

00:01:52.460 --> 00:01:52.470 align:start position:0%
that states in cold actually everything
 

00:01:52.470 --> 00:01:57.350 align:start position:0%
that states in cold actually everything
that<00:01:52.820><c> promises</c><00:01:53.820><c> to</c><00:01:53.939><c> do</c><00:01:54.409><c> then</c><00:01:55.460><c> if</c><00:01:56.460><c> we</c><00:01:56.729><c> ask</c><00:01:56.969><c> the</c>

00:01:57.350 --> 00:01:57.360 align:start position:0%
that promises to do then if we ask the
 

00:01:57.360 --> 00:01:59.359 align:start position:0%
that promises to do then if we ask the
browser<00:01:57.540><c> to</c><00:01:58.170><c> check</c><00:01:58.200><c> on</c><00:01:58.740><c> the</c><00:01:58.950><c> formal</c>

00:01:59.359 --> 00:01:59.369 align:start position:0%
browser to check on the formal
 

00:01:59.369 --> 00:02:01.370 align:start position:0%
browser to check on the formal
specification<00:01:59.549><c> the</c><00:02:00.149><c> mathematical</c><00:02:00.810><c> proof</c><00:02:01.079><c> of</c>

00:02:01.370 --> 00:02:01.380 align:start position:0%
specification the mathematical proof of
 

00:02:01.380 --> 00:02:03.679 align:start position:0%
specification the mathematical proof of
that<00:02:01.590><c> specification</c><00:02:01.979><c> we</c><00:02:02.880><c> can</c><00:02:03.030><c> be</c><00:02:03.149><c> sure</c><00:02:03.390><c> that</c>

00:02:03.679 --> 00:02:03.689 align:start position:0%
that specification we can be sure that
 

00:02:03.689 --> 00:02:07.209 align:start position:0%
that specification we can be sure that
the<00:02:04.350><c> program</c><00:02:04.799><c> does</c><00:02:05.009><c> what</c><00:02:05.250><c> we</c><00:02:05.549><c> expect</c>

00:02:07.209 --> 00:02:07.219 align:start position:0%
the program does what we expect
 

00:02:07.219 --> 00:02:09.639 align:start position:0%
the program does what we expect
in<00:02:07.789><c> other</c><00:02:07.939><c> words</c><00:02:08.209><c> by</c><00:02:08.840><c> just</c><00:02:09.110><c> checking</c><00:02:09.319><c> the</c>

00:02:09.639 --> 00:02:09.649 align:start position:0%
in other words by just checking the
 

00:02:09.649 --> 00:02:14.710 align:start position:0%
in other words by just checking the
first<00:02:11.650><c> the</c><00:02:12.650><c> first</c><00:02:12.800><c> line</c><00:02:13.069><c> is</c><00:02:13.250><c> there</c><00:02:13.459><c> we</c><00:02:14.269><c> could</c>

00:02:14.710 --> 00:02:14.720 align:start position:0%
first the first line is there we could
 

00:02:14.720 --> 00:02:17.190 align:start position:0%
first the first line is there we could
have<00:02:14.750><c> avoided</c><00:02:15.110><c> the</c><00:02:15.590><c> entire</c><00:02:15.920><c> deal</c><00:02:16.190><c> instead</c>

00:02:17.190 --> 00:02:17.200 align:start position:0%
have avoided the entire deal instead
 

00:02:17.200 --> 00:02:20.259 align:start position:0%
have avoided the entire deal instead
it's<00:02:18.200><c> one</c><00:02:18.470><c> line</c><00:02:18.739><c> that</c><00:02:19.160><c> if</c><00:02:19.430><c> someone</c><00:02:19.819><c> just</c><00:02:20.030><c> read</c>

00:02:20.259 --> 00:02:20.269 align:start position:0%
it's one line that if someone just read
 

00:02:20.269 --> 00:02:22.660 align:start position:0%
it's one line that if someone just read
it<00:02:20.420><c> it</c><00:02:20.870><c> could</c><00:02:21.260><c> have</c><00:02:21.470><c> avoided</c><00:02:21.739><c> everything</c><00:02:22.519><c> that</c>

00:02:22.660 --> 00:02:22.670 align:start position:0%
it it could have avoided everything that
 

00:02:22.670 --> 00:02:25.710 align:start position:0%
it it could have avoided everything that
happened<00:02:23.120><c> two</c><00:02:23.599><c> years</c><00:02:23.629><c> ago</c><00:02:23.870><c> on</c><00:02:24.290><c> the</c><00:02:24.470><c> Dow</c><00:02:24.620><c> fiasco</c>

00:02:25.710 --> 00:02:25.720 align:start position:0%
happened two years ago on the Dow fiasco
 

00:02:25.720 --> 00:02:28.990 align:start position:0%
happened two years ago on the Dow fiasco
so<00:02:26.720><c> this</c><00:02:27.260><c> was</c><00:02:27.530><c> our</c><00:02:27.739><c> vision</c><00:02:28.040><c> but</c><00:02:28.670><c> there</c><00:02:28.819><c> was</c><00:02:28.970><c> a</c>

00:02:28.990 --> 00:02:29.000 align:start position:0%
so this was our vision but there was a
 

00:02:29.000 --> 00:02:30.270 align:start position:0%
so this was our vision but there was a
problem

00:02:30.270 --> 00:02:30.280 align:start position:0%
problem
 

00:02:30.280 --> 00:02:33.850 align:start position:0%
problem
those<00:02:31.280><c> are</c><00:02:31.640><c> some</c><00:02:32.420><c> of</c><00:02:32.540><c> the</c><00:02:32.569><c> most</c><00:02:32.900><c> popular</c><00:02:33.140><c> proof</c>

00:02:33.850 --> 00:02:33.860 align:start position:0%
those are some of the most popular proof
 

00:02:33.860 --> 00:02:37.150 align:start position:0%
those are some of the most popular proof
languages<00:02:34.400><c> in</c><00:02:34.549><c> the</c><00:02:34.670><c> market</c><00:02:35.470><c> for</c><00:02:36.470><c> many</c><00:02:36.650><c> reasons</c>

00:02:37.150 --> 00:02:37.160 align:start position:0%
languages in the market for many reasons
 

00:02:37.160 --> 00:02:40.119 align:start position:0%
languages in the market for many reasons
some<00:02:37.370><c> simple</c><00:02:37.790><c> or</c><00:02:37.970><c> the</c><00:02:38.120><c> very</c><00:02:38.480><c> complex</c><00:02:38.989><c> none</c><00:02:39.860><c> of</c>

00:02:40.119 --> 00:02:40.129 align:start position:0%
some simple or the very complex none of
 

00:02:40.129 --> 00:02:42.280 align:start position:0%
some simple or the very complex none of
them<00:02:40.400><c> had</c><00:02:40.730><c> everything</c><00:02:41.180><c> we</c><00:02:41.540><c> needed</c><00:02:41.569><c> like</c><00:02:41.989><c> we</c>

00:02:42.280 --> 00:02:42.290 align:start position:0%
them had everything we needed like we
 

00:02:42.290 --> 00:02:43.960 align:start position:0%
them had everything we needed like we
wanted<00:02:42.680><c> those</c><00:02:42.920><c> one</c><00:02:43.310><c> of</c><00:02:43.459><c> those</c><00:02:43.640><c> languages</c>

00:02:43.960 --> 00:02:43.970 align:start position:0%
wanted those one of those languages
 

00:02:43.970 --> 00:02:45.759 align:start position:0%
wanted those one of those languages
should<00:02:44.180><c> be</c><00:02:44.269><c> the</c><00:02:44.390><c> JavaScript</c><00:02:44.870><c> of</c><00:02:45.140><c> our</c><00:02:45.410><c> browser</c>

00:02:45.759 --> 00:02:45.769 align:start position:0%
should be the JavaScript of our browser
 

00:02:45.769 --> 00:02:49.720 align:start position:0%
should be the JavaScript of our browser
but<00:02:46.430><c> none</c><00:02:46.700><c> of</c><00:02:46.849><c> them</c><00:02:47.090><c> had</c><00:02:47.390><c> had</c><00:02:47.840><c> at</c><00:02:47.959><c> all</c><00:02:48.579><c> some</c><00:02:49.579><c> of</c>

00:02:49.720 --> 00:02:49.730 align:start position:0%
but none of them had had at all some of
 

00:02:49.730 --> 00:02:51.100 align:start position:0%
but none of them had had at all some of
them<00:02:50.000><c> almost</c><00:02:50.299><c> did</c><00:02:50.780><c> it</c>

00:02:51.100 --> 00:02:51.110 align:start position:0%
them almost did it
 

00:02:51.110 --> 00:02:54.720 align:start position:0%
them almost did it
but<00:02:51.530><c> there's</c><00:02:51.709><c> one</c><00:02:52.010><c> thing</c><00:02:52.370><c> none</c><00:02:53.150><c> of</c><00:02:53.180><c> them</c><00:02:53.780><c> had</c>

00:02:54.720 --> 00:02:54.730 align:start position:0%
but there's one thing none of them had
 

00:02:54.730 --> 00:03:00.369 align:start position:0%
but there's one thing none of them had
performance<00:02:57.910><c> there</c><00:02:58.910><c> was</c><00:02:59.120><c> no</c><00:02:59.480><c> language</c><00:02:59.930><c> in</c><00:03:00.290><c> the</c>

00:03:00.369 --> 00:03:00.379 align:start position:0%
performance there was no language in the
 

00:03:00.379 --> 00:03:04.240 align:start position:0%
performance there was no language in the
world<00:03:00.739><c> that</c><00:03:01.430><c> had</c><00:03:01.700><c> high</c><00:03:02.299><c> level</c><00:03:02.750><c> that</c><00:03:03.739><c> what</c><00:03:03.980><c> was</c>

00:03:04.240 --> 00:03:04.250 align:start position:0%
world that had high level that what was
 

00:03:04.250 --> 00:03:07.330 align:start position:0%
world that had high level that what was
high<00:03:04.519><c> level</c><00:03:04.940><c> had</c><00:03:05.480><c> former</c><00:03:06.049><c> proofs</c><00:03:06.349><c> and</c><00:03:06.590><c> was</c>

00:03:07.330 --> 00:03:07.340 align:start position:0%
high level had former proofs and was
 

00:03:07.340 --> 00:03:12.330 align:start position:0%
high level had former proofs and was
first<00:03:07.549><c> enough</c><00:03:07.849><c> was</c><00:03:08.239><c> fast</c><00:03:08.540><c> enough</c><00:03:08.810><c> for</c><00:03:09.049><c> us</c><00:03:09.170><c> so</c>

00:03:12.330 --> 00:03:12.340 align:start position:0%
 
 

00:03:12.340 --> 00:03:14.920 align:start position:0%
 
if<00:03:13.340><c> you</c><00:03:13.519><c> wanted</c><00:03:13.819><c> to</c><00:03:13.880><c> compile</c><00:03:14.359><c> some</c><00:03:14.389><c> of</c><00:03:14.750><c> those</c>

00:03:14.920 --> 00:03:14.930 align:start position:0%
if you wanted to compile some of those
 

00:03:14.930 --> 00:03:18.699 align:start position:0%
if you wanted to compile some of those
language<00:03:15.410><c> to</c><00:03:15.829><c> to</c><00:03:16.609><c> the</c><00:03:16.730><c> idiom</c><00:03:17.139><c> the</c><00:03:18.139><c> cost</c><00:03:18.440><c> of</c>

00:03:18.699 --> 00:03:18.709 align:start position:0%
language to to the idiom the cost of
 

00:03:18.709 --> 00:03:20.920 align:start position:0%
language to to the idiom the cost of
course<00:03:18.920><c> of</c><00:03:19.220><c> doing</c><00:03:19.549><c> that</c><00:03:19.700><c> would</c><00:03:20.000><c> be</c><00:03:20.269><c> very</c>

00:03:20.920 --> 00:03:20.930 align:start position:0%
course of doing that would be very
 

00:03:20.930 --> 00:03:23.140 align:start position:0%
course of doing that would be very
expensive<00:03:21.230><c> you</c><00:03:21.590><c> guys</c><00:03:21.950><c> with</c><00:03:22.160><c> a</c><00:03:22.400><c> lot</c><00:03:22.579><c> of</c><00:03:22.790><c> a</c><00:03:22.940><c> lot</c>

00:03:23.140 --> 00:03:23.150 align:start position:0%
expensive you guys with a lot of a lot
 

00:03:23.150 --> 00:03:25.449 align:start position:0%
expensive you guys with a lot of a lot
of<00:03:23.209><c> money</c><00:03:23.450><c> yet</c><00:03:23.840><c> in</c><00:03:24.139><c> our</c><00:03:24.230><c> transaction</c><00:03:24.799><c> and</c><00:03:24.950><c> then</c>

00:03:25.449 --> 00:03:25.459 align:start position:0%
of money yet in our transaction and then
 

00:03:25.459 --> 00:03:27.520 align:start position:0%
of money yet in our transaction and then
it<00:03:25.639><c> would</c><00:03:25.910><c> not</c><00:03:26.090><c> be</c><00:03:26.150><c> practical</c><00:03:26.630><c> yeah</c>

00:03:27.520 --> 00:03:27.530 align:start position:0%
it would not be practical yeah
 

00:03:27.530 --> 00:03:29.440 align:start position:0%
it would not be practical yeah
the<00:03:27.650><c> bad</c><00:03:27.799><c> news</c><00:03:28.040><c> is</c><00:03:28.220><c> that</c><00:03:28.340><c> we</c><00:03:28.519><c> had</c><00:03:28.669><c> to</c><00:03:28.819><c> stop</c><00:03:29.239><c> our</c>

00:03:29.440 --> 00:03:29.450 align:start position:0%
the bad news is that we had to stop our
 

00:03:29.450 --> 00:03:31.690 align:start position:0%
the bad news is that we had to stop our
browser<00:03:29.750><c> development</c><00:03:30.230><c> to</c><00:03:30.590><c> focus</c><00:03:31.160><c> on</c><00:03:31.310><c> making</c>

00:03:31.690 --> 00:03:31.700 align:start position:0%
browser development to focus on making
 

00:03:31.700 --> 00:03:34.000 align:start position:0%
browser development to focus on making
our<00:03:31.790><c> own</c><00:03:31.849><c> language</c><00:03:32.419><c> the</c><00:03:33.260><c> good</c><00:03:33.440><c> news</c><00:03:33.620><c> is</c><00:03:33.950><c> that</c>

00:03:34.000 --> 00:03:34.010 align:start position:0%
our own language the good news is that
 

00:03:34.010 --> 00:03:37.599 align:start position:0%
our own language the good news is that
it<00:03:34.819><c> is</c><00:03:35.299><c> awesome</c><00:03:35.900><c> so</c><00:03:36.560><c> better</c><00:03:37.220><c> than</c><00:03:37.340><c> our</c>

00:03:37.599 --> 00:03:37.609 align:start position:0%
it is awesome so better than our
 

00:03:37.609 --> 00:03:40.360 align:start position:0%
it is awesome so better than our
presentation<00:03:38.480><c> so</c><00:03:38.780><c> that</c><00:03:39.049><c> con</c><00:03:39.319><c> today</c><00:03:39.919><c> the</c><00:03:40.220><c> moon</c>

00:03:40.360 --> 00:03:40.370 align:start position:0%
presentation so that con today the moon
 

00:03:40.370 --> 00:03:50.180 align:start position:0%
presentation so that con today the moon
team<00:03:40.870><c> proudly</c><00:03:41.870><c> presents</c><00:03:42.380><c> you</c><00:03:43.480><c> formality</c>

00:03:50.180 --> 00:03:50.190 align:start position:0%
 
 

00:03:50.190 --> 00:03:52.560 align:start position:0%
 
formality<00:03:51.190><c> is</c><00:03:51.250><c> a</c><00:03:51.280><c> high-level</c><00:03:51.820><c> functional</c>

00:03:52.560 --> 00:03:52.570 align:start position:0%
formality is a high-level functional
 

00:03:52.570 --> 00:03:54.150 align:start position:0%
formality is a high-level functional
programming<00:03:52.900><c> language</c><00:03:53.290><c> that</c><00:03:53.500><c> features</c>

00:03:54.150 --> 00:03:54.160 align:start position:0%
programming language that features
 

00:03:54.160 --> 00:03:56.220 align:start position:0%
programming language that features
formal<00:03:54.640><c> proofs</c><00:03:54.910><c> that</c><00:03:55.180><c> is</c><00:03:55.660><c> not</c><00:03:55.840><c> garbage</c>

00:03:56.220 --> 00:03:56.230 align:start position:0%
formal proofs that is not garbage
 

00:03:56.230 --> 00:03:59.370 align:start position:0%
formal proofs that is not garbage
collected<00:03:56.740><c> and</c><00:03:56.920><c> that</c><00:03:57.370><c> targets</c><00:03:57.820><c> DVM</c><00:03:58.480><c> and</c><00:03:58.750><c> GPU</c>

00:03:59.370 --> 00:03:59.380 align:start position:0%
collected and that targets DVM and GPU
 

00:03:59.380 --> 00:04:01.290 align:start position:0%
collected and that targets DVM and GPU
the<00:03:59.860><c> only</c><00:04:00.190><c> language</c><00:04:00.370><c> in</c><00:04:00.610><c> the</c><00:04:00.730><c> world</c><00:04:00.880><c> that</c><00:04:01.090><c> does</c>

00:04:01.290 --> 00:04:01.300 align:start position:0%
the only language in the world that does
 

00:04:01.300 --> 00:04:03.510 align:start position:0%
the only language in the world that does
that<00:04:01.540><c> it's</c><00:04:02.140><c> simple</c><00:04:02.560><c> enough</c><00:04:02.620><c> for</c><00:04:03.280><c> you</c><00:04:03.370><c> to</c>

00:04:03.510 --> 00:04:03.520 align:start position:0%
that it's simple enough for you to
 

00:04:03.520 --> 00:04:05.430 align:start position:0%
that it's simple enough for you to
implement<00:04:03.730><c> it</c><00:04:04.000><c> yourself</c><00:04:04.120><c> in</c><00:04:04.870><c> other</c><00:04:05.020><c> words</c><00:04:05.260><c> if</c>

00:04:05.430 --> 00:04:05.440 align:start position:0%
implement it yourself in other words if
 

00:04:05.440 --> 00:04:07.260 align:start position:0%
implement it yourself in other words if
you<00:04:05.530><c> don't</c><00:04:05.770><c> trust</c><00:04:05.980><c> our</c><00:04:06.280><c> shaker</c><00:04:06.670><c> you</c><00:04:06.910><c> can</c><00:04:07.090><c> do</c>

00:04:07.260 --> 00:04:07.270 align:start position:0%
you don't trust our shaker you can do
 

00:04:07.270 --> 00:04:09.180 align:start position:0%
you don't trust our shaker you can do
you<00:04:07.450><c> can</c><00:04:07.600><c> implement</c><00:04:07.960><c> for</c><00:04:08.170><c> mulcher</c><00:04:08.650><c> self</c><00:04:08.920><c> and</c>

00:04:09.180 --> 00:04:09.190 align:start position:0%
you can implement for mulcher self and
 

00:04:09.190 --> 00:04:11.340 align:start position:0%
you can implement for mulcher self and
it<00:04:09.700><c> has</c><00:04:09.910><c> the</c><00:04:10.060><c> potential</c><00:04:10.450><c> to</c><00:04:10.660><c> be</c><00:04:10.900><c> very</c><00:04:11.080><c> fast</c>

00:04:11.340 --> 00:04:11.350 align:start position:0%
it has the potential to be very fast
 

00:04:11.350 --> 00:04:18.140 align:start position:0%
it has the potential to be very fast
which<00:04:12.070><c> we</c><00:04:12.600><c> will</c><00:04:13.600><c> explain</c><00:04:14.050><c> some</c><00:04:16.140><c> thank</c><00:04:17.140><c> you</c>

00:04:18.140 --> 00:04:18.150 align:start position:0%
which we will explain some thank you
 

00:04:18.150 --> 00:04:21.360 align:start position:0%
which we will explain some thank you
well<00:04:19.150><c> fermented</c><00:04:20.109><c> programs</c><00:04:20.590><c> have</c><00:04:20.799><c> two</c>

00:04:21.360 --> 00:04:21.370 align:start position:0%
well fermented programs have two
 

00:04:21.370 --> 00:04:25.410 align:start position:0%
well fermented programs have two
building<00:04:22.000><c> blocks</c><00:04:22.980><c> one</c><00:04:23.980><c> inductive</c><00:04:24.730><c> data</c><00:04:24.940><c> data</c>

00:04:25.410 --> 00:04:25.420 align:start position:0%
building blocks one inductive data data
 

00:04:25.420 --> 00:04:25.980 align:start position:0%
building blocks one inductive data data
types

00:04:25.980 --> 00:04:25.990 align:start position:0%
types
 

00:04:25.990 --> 00:04:29.040 align:start position:0%
types
they<00:04:26.410><c> represent</c><00:04:27.070><c> data</c><00:04:27.370><c> like</c><00:04:27.940><c> natural</c><00:04:28.690><c> numbers</c>

00:04:29.040 --> 00:04:29.050 align:start position:0%
they represent data like natural numbers
 

00:04:29.050 --> 00:04:33.210 align:start position:0%
they represent data like natural numbers
like<00:04:30.930><c> vector</c><00:04:31.930><c> vectors</c><00:04:32.320><c> equality</c>

00:04:33.210 --> 00:04:33.220 align:start position:0%
like vector vectors equality
 

00:04:33.220 --> 00:04:37.380 align:start position:0%
like vector vectors equality
certificates<00:04:33.820><c> and</c><00:04:34.060><c> two</c><00:04:35.340><c> functions</c><00:04:36.390><c> they</c>

00:04:37.380 --> 00:04:37.390 align:start position:0%
certificates and two functions they
 

00:04:37.390 --> 00:04:41.390 align:start position:0%
certificates and two functions they
represent<00:04:38.160><c> computations</c><00:04:39.160><c> and</c><00:04:39.430><c> proofs</c><00:04:39.910><c> so</c>

00:04:41.390 --> 00:04:41.400 align:start position:0%
represent computations and proofs so
 

00:04:41.400 --> 00:04:44.190 align:start position:0%
represent computations and proofs so
some<00:04:42.400><c> things</c><00:04:42.640><c> like</c><00:04:42.880><c> doubling</c><00:04:43.690><c> in</c><00:04:43.780><c> a</c><00:04:43.870><c> number</c>

00:04:44.190 --> 00:04:44.200 align:start position:0%
some things like doubling in a number
 

00:04:44.200 --> 00:04:49.190 align:start position:0%
some things like doubling in a number
like<00:04:45.600><c> fetching</c><00:04:46.600><c> the</c><00:04:46.750><c> first</c><00:04:47.050><c> the</c><00:04:48.010><c> first</c>

00:04:49.190 --> 00:04:49.200 align:start position:0%
like fetching the first the first
 

00:04:49.200 --> 00:04:52.410 align:start position:0%
like fetching the first the first
element<00:04:50.200><c> of</c><00:04:50.290><c> a</c><00:04:50.380><c> vector</c><00:04:50.710><c> or</c><00:04:51.300><c> proving</c><00:04:52.300><c> the</c>

00:04:52.410 --> 00:04:52.420 align:start position:0%
element of a vector or proving the
 

00:04:52.420 --> 00:04:55.680 align:start position:0%
element of a vector or proving the
symmetry<00:04:52.900><c> of</c><00:04:53.020><c> equality</c><00:04:54.120><c> but</c><00:04:55.120><c> that's</c><00:04:55.330><c> pretty</c>

00:04:55.680 --> 00:04:55.690 align:start position:0%
symmetry of equality but that's pretty
 

00:04:55.690 --> 00:04:57.390 align:start position:0%
symmetry of equality but that's pretty
standard<00:04:55.990><c> on</c><00:04:56.320><c> proof</c><00:04:56.620><c> language</c><00:04:56.950><c> so</c><00:04:57.160><c> we</c><00:04:57.250><c> won't</c>

00:04:57.390 --> 00:04:57.400 align:start position:0%
standard on proof language so we won't
 

00:04:57.400 --> 00:04:59.670 align:start position:0%
standard on proof language so we won't
spend<00:04:57.550><c> a</c><00:04:57.760><c> lot</c><00:04:57.790><c> of</c><00:04:57.910><c> time</c><00:04:58.180><c> this</c><00:04:58.360><c> so</c><00:04:58.870><c> let's</c><00:04:59.470><c> move</c>

00:04:59.670 --> 00:04:59.680 align:start position:0%
spend a lot of time this so let's move
 

00:04:59.680 --> 00:05:02.490 align:start position:0%
spend a lot of time this so let's move
on<00:04:59.890><c> to</c><00:05:00.010><c> the</c><00:05:00.160><c> fun</c><00:05:00.340><c> part</c><00:05:00.400><c> that's</c><00:05:01.270><c> how</c><00:05:02.110><c> fast</c>

00:05:02.490 --> 00:05:02.500 align:start position:0%
on to the fun part that's how fast
 

00:05:02.500 --> 00:05:09.930 align:start position:0%
on to the fun part that's how fast
format<00:05:03.280><c> is</c><00:05:03.550><c> how</c><00:05:04.300><c> fast</c><00:05:04.660><c> it</c><00:05:04.870><c> can</c><00:05:05.230><c> be</c><00:05:08.940><c> please</c>

00:05:09.930 --> 00:05:09.940 align:start position:0%
format is how fast it can be please
 

00:05:09.940 --> 00:05:12.240 align:start position:0%
format is how fast it can be please
check<00:05:10.210><c> this</c><00:05:10.390><c> code</c><00:05:10.660><c> it's</c><00:05:11.260><c> very</c><00:05:11.350><c> simple</c><00:05:11.860><c> it</c><00:05:12.010><c> does</c>

00:05:12.240 --> 00:05:12.250 align:start position:0%
check this code it's very simple it does
 

00:05:12.250 --> 00:05:14.760 align:start position:0%
check this code it's very simple it does
three<00:05:12.490><c> things</c><00:05:12.760><c> first</c><00:05:13.480><c> it</c><00:05:13.840><c> creates</c><00:05:14.290><c> an</c><00:05:14.530><c> array</c>

00:05:14.760 --> 00:05:14.770 align:start position:0%
three things first it creates an array
 

00:05:14.770 --> 00:05:17.940 align:start position:0%
three things first it creates an array
with<00:05:15.130><c> 100</c><00:05:15.730><c> zeros</c><00:05:16.090><c> then</c><00:05:16.810><c> it</c><00:05:17.050><c> used</c><00:05:17.500><c> the</c><00:05:17.740><c> map</c>

00:05:17.940 --> 00:05:17.950 align:start position:0%
with 100 zeros then it used the map
 

00:05:17.950 --> 00:05:20.640 align:start position:0%
with 100 zeros then it used the map
function<00:05:18.340><c> to</c><00:05:19.000><c> increment</c><00:05:19.150><c> every</c><00:05:19.600><c> number</c><00:05:20.140><c> by</c><00:05:20.440><c> 1</c>

00:05:20.640 --> 00:05:20.650 align:start position:0%
function to increment every number by 1
 

00:05:20.650 --> 00:05:22.950 align:start position:0%
function to increment every number by 1
and<00:05:20.890><c> million</c><00:05:21.550><c> times</c><00:05:21.820><c> and</c><00:05:22.480><c> then</c><00:05:22.630><c> it</c><00:05:22.810><c> outputs</c>

00:05:22.950 --> 00:05:22.960 align:start position:0%
and million times and then it outputs
 

00:05:22.960 --> 00:05:25.590 align:start position:0%
and million times and then it outputs
the<00:05:23.380><c> result</c><00:05:23.500><c> it's</c><00:05:23.919><c> very</c><00:05:24.160><c> simple</c><00:05:24.490><c> how</c><00:05:25.150><c> long</c><00:05:25.390><c> it</c>

00:05:25.590 --> 00:05:25.600 align:start position:0%
the result it's very simple how long it
 

00:05:25.600 --> 00:05:27.180 align:start position:0%
the result it's very simple how long it
takes<00:05:25.900><c> to</c><00:05:26.140><c> run</c><00:05:26.290><c> this</c><00:05:26.530><c> code</c><00:05:26.800><c> in</c><00:05:27.040><c> different</c>

00:05:27.180 --> 00:05:27.190 align:start position:0%
takes to run this code in different
 

00:05:27.190 --> 00:05:31.440 align:start position:0%
takes to run this code in different
levels<00:05:28.830><c> as</c><00:05:29.830><c> you</c><00:05:29.860><c> can</c><00:05:30.130><c> see</c><00:05:30.280><c> for</c><00:05:30.820><c> mulch</c><00:05:31.090><c> bits</c>

00:05:31.440 --> 00:05:31.450 align:start position:0%
levels as you can see for mulch bits
 

00:05:31.450 --> 00:05:34.110 align:start position:0%
levels as you can see for mulch bits
every<00:05:32.020><c> other</c><00:05:32.229><c> language</c><00:05:32.860><c> and</c><00:05:33.100><c> the</c><00:05:33.760><c> difference</c>

00:05:34.110 --> 00:05:34.120 align:start position:0%
every other language and the difference
 

00:05:34.120 --> 00:05:35.190 align:start position:0%
every other language and the difference
is<00:05:34.390><c> huge</c>

00:05:35.190 --> 00:05:35.200 align:start position:0%
is huge
 

00:05:35.200 --> 00:05:36.990 align:start position:0%
is huge
this<00:05:35.770><c> is</c><00:05:35.890><c> not</c><00:05:36.040><c> a</c><00:05:36.070><c> compile</c><00:05:36.460><c> time</c><00:05:36.520><c> optimization</c>

00:05:36.990 --> 00:05:37.000 align:start position:0%
this is not a compile time optimization
 

00:05:37.000 --> 00:05:39.090 align:start position:0%
this is not a compile time optimization
is<00:05:37.450><c> not</c><00:05:37.660><c> some</c><00:05:37.870><c> clever</c><00:05:38.050><c> trick</c><00:05:38.380><c> this</c><00:05:38.979><c> is</c>

00:05:39.090 --> 00:05:39.100 align:start position:0%
is not some clever trick this is
 

00:05:39.100 --> 00:05:41.280 align:start position:0%
is not some clever trick this is
actually<00:05:39.550><c> what</c><00:05:39.790><c> happens</c><00:05:39.820><c> when</c><00:05:40.570><c> we</c><00:05:40.690><c> want</c><00:05:40.930><c> very</c>

00:05:41.280 --> 00:05:41.290 align:start position:0%
actually what happens when we want very
 

00:05:41.290 --> 00:05:43.590 align:start position:0%
actually what happens when we want very
high<00:05:41.440><c> level</c><00:05:41.860><c> code</c><00:05:42.070><c> of</c><00:05:42.280><c> a</c><00:05:42.490><c> mallet</c><00:05:42.790><c> there</c><00:05:43.300><c> is</c><00:05:43.390><c> no</c>

00:05:43.590 --> 00:05:43.600 align:start position:0%
high level code of a mallet there is no
 

00:05:43.600 --> 00:05:45.659 align:start position:0%
high level code of a mallet there is no
other<00:05:43.870><c> language</c><00:05:44.200><c> in</c><00:05:44.530><c> the</c><00:05:44.650><c> world</c><00:05:44.860><c> capable</c><00:05:45.190><c> of</c>

00:05:45.659 --> 00:05:45.669 align:start position:0%
other language in the world capable of
 

00:05:45.669 --> 00:05:47.969 align:start position:0%
other language in the world capable of
optimizing<00:05:46.229><c> functional</c><00:05:47.229><c> high</c><00:05:47.470><c> level</c><00:05:47.770><c> code</c>

00:05:47.969 --> 00:05:47.979 align:start position:0%
optimizing functional high level code
 

00:05:47.979 --> 00:05:50.550 align:start position:0%
optimizing functional high level code
like<00:05:48.580><c> it</c><00:05:48.820><c> if</c><00:05:49.210><c> you</c><00:05:49.360><c> don't</c><00:05:49.540><c> believe</c><00:05:49.660><c> me</c><00:05:49.780><c> please</c>

00:05:50.550 --> 00:05:50.560 align:start position:0%
like it if you don't believe me please
 

00:05:50.560 --> 00:05:52.290 align:start position:0%
like it if you don't believe me please
check<00:05:50.890><c> our</c><00:05:51.070><c> benchmarks</c><00:05:51.610><c> on</c><00:05:51.820><c> the</c><00:05:51.940><c> link</c><00:05:52.120><c> below</c>

00:05:52.290 --> 00:05:52.300 align:start position:0%
check our benchmarks on the link below
 

00:05:52.300 --> 00:05:55.290 align:start position:0%
check our benchmarks on the link below
where<00:05:52.870><c> we</c><00:05:53.169><c> also</c><00:05:53.410><c> explain</c><00:05:54.040><c> why</c><00:05:54.610><c> that's</c><00:05:55.030><c> the</c>

00:05:55.290 --> 00:05:55.300 align:start position:0%
where we also explain why that's the
 

00:05:55.300 --> 00:05:58.200 align:start position:0%
where we also explain why that's the
case<00:05:55.330><c> but</c><00:05:55.750><c> that's</c><00:05:56.650><c> not</c><00:05:57.010><c> a</c><00:05:57.040><c> whole</c><00:05:57.310><c> history</c><00:05:57.520><c> yeah</c>

00:05:58.200 --> 00:05:58.210 align:start position:0%
case but that's not a whole history yeah
 

00:05:58.210 --> 00:06:00.390 align:start position:0%
case but that's not a whole history yeah
let's<00:05:58.570><c> have</c><00:05:59.110><c> a</c><00:05:59.140><c> look</c><00:05:59.380><c> at</c><00:05:59.470><c> this</c><00:05:59.620><c> other</c><00:05:59.979><c> example</c>

00:06:00.390 --> 00:06:00.400 align:start position:0%
let's have a look at this other example
 

00:06:00.400 --> 00:06:02.709 align:start position:0%
let's have a look at this other example
this<00:06:01.120><c> also</c><00:06:01.720><c> does</c><00:06:01.960><c> three</c><00:06:02.320><c> things</c>

00:06:02.709 --> 00:06:02.719 align:start position:0%
this also does three things
 

00:06:02.719 --> 00:06:05.019 align:start position:0%
this also does three things
the<00:06:02.869><c> first</c><00:06:03.139><c> thing</c><00:06:03.349><c> it</c><00:06:04.159><c> creates</c><00:06:04.399><c> a</c><00:06:04.639><c> linkedlist</c>

00:06:05.019 --> 00:06:05.029 align:start position:0%
the first thing it creates a linkedlist
 

00:06:05.029 --> 00:06:08.379 align:start position:0%
the first thing it creates a linkedlist
of<00:06:05.509><c> bits</c><00:06:06.110><c> then</c><00:06:06.889><c> just</c><00:06:07.309><c> flips</c><00:06:07.610><c> them</c><00:06:07.819><c> over</c><00:06:08.269><c> and</c>

00:06:08.379 --> 00:06:08.389 align:start position:0%
of bits then just flips them over and
 

00:06:08.389 --> 00:06:11.109 align:start position:0%
of bits then just flips them over and
over<00:06:08.509><c> about</c><00:06:09.110><c> a</c><00:06:09.259><c> million</c><00:06:09.619><c> times</c><00:06:09.889><c> and</c><00:06:10.189><c> then</c><00:06:10.939><c> it</c>

00:06:11.109 --> 00:06:11.119 align:start position:0%
over about a million times and then it
 

00:06:11.119 --> 00:06:12.189 align:start position:0%
over about a million times and then it
prints<00:06:11.479><c> out</c><00:06:11.569><c> the</c><00:06:11.599><c> result</c>

00:06:12.189 --> 00:06:12.199 align:start position:0%
prints out the result
 

00:06:12.199 --> 00:06:16.209 align:start position:0%
prints out the result
how<00:06:12.739><c> fast</c><00:06:13.249><c> can</c><00:06:13.489><c> this</c><00:06:13.639><c> execute</c><00:06:14.269><c> as</c><00:06:14.769><c> we</c><00:06:15.769><c> see</c><00:06:15.949><c> here</c>

00:06:16.209 --> 00:06:16.219 align:start position:0%
how fast can this execute as we see here
 

00:06:16.219 --> 00:06:19.239 align:start position:0%
how fast can this execute as we see here
formalities<00:06:16.729><c> now</c><00:06:17.239><c> slower</c><00:06:17.929><c> than</c><00:06:18.529><c> the</c><00:06:18.619><c> rest</c><00:06:18.769><c> it</c>

00:06:19.239 --> 00:06:19.249 align:start position:0%
formalities now slower than the rest it
 

00:06:19.249 --> 00:06:21.909 align:start position:0%
formalities now slower than the rest it
happens<00:06:19.669><c> because</c><00:06:20.269><c> the</c><00:06:21.049><c> code</c><00:06:21.499><c> is</c><00:06:21.529><c> too</c>

00:06:21.909 --> 00:06:21.919 align:start position:0%
happens because the code is too
 

00:06:21.919 --> 00:06:25.449 align:start position:0%
happens because the code is too
low-level<00:06:22.809><c> so</c><00:06:23.809><c> it</c><00:06:24.499><c> can't</c><00:06:24.829><c> be</c><00:06:25.039><c> really</c>

00:06:25.449 --> 00:06:25.459 align:start position:0%
low-level so it can't be really
 

00:06:25.459 --> 00:06:29.259 align:start position:0%
low-level so it can't be really
optimized<00:06:27.279><c> formality</c><00:06:28.279><c> is</c><00:06:28.339><c> to</c><00:06:28.579><c> an</c><00:06:28.699><c> interpreted</c>

00:06:29.259 --> 00:06:29.269 align:start position:0%
optimized formality is to an interpreted
 

00:06:29.269 --> 00:06:31.329 align:start position:0%
optimized formality is to an interpreted
language<00:06:29.299><c> so</c><00:06:30.049><c> it</c><00:06:30.289><c> can't</c><00:06:30.529><c> compete</c><00:06:30.919><c> and</c><00:06:31.159><c> raw</c>

00:06:31.329 --> 00:06:31.339 align:start position:0%
language so it can't compete and raw
 

00:06:31.339 --> 00:06:34.649 align:start position:0%
language so it can't compete and raw
performance<00:06:31.879><c> with</c><00:06:32.029><c> other</c><00:06:32.559><c> major</c><00:06:33.559><c> compilers</c>

00:06:34.649 --> 00:06:34.659 align:start position:0%
performance with other major compilers
 

00:06:34.659 --> 00:06:38.229 align:start position:0%
performance with other major compilers
but<00:06:35.659><c> that's</c><00:06:36.139><c> okay</c><00:06:36.379><c> the</c><00:06:36.949><c> potential</c><00:06:37.399><c> is</c><00:06:37.639><c> here</c>

00:06:38.229 --> 00:06:38.239 align:start position:0%
but that's okay the potential is here
 

00:06:38.239 --> 00:06:42.719 align:start position:0%
but that's okay the potential is here
and<00:06:39.189><c> you'll</c><00:06:40.189><c> see</c><00:06:40.429><c> why</c><00:06:40.879><c> in</c><00:06:41.209><c> the</c><00:06:41.509><c> next</c><00:06:41.719><c> example</c>

00:06:42.719 --> 00:06:42.729 align:start position:0%
and you'll see why in the next example
 

00:06:42.729 --> 00:06:45.639 align:start position:0%
and you'll see why in the next example
so<00:06:43.729><c> this</c><00:06:44.089><c> is</c><00:06:44.419><c> the</c><00:06:44.629><c> same</c><00:06:44.869><c> code</c><00:06:45.199><c> this</c><00:06:45.469><c> is</c><00:06:45.559><c> the</c>

00:06:45.639 --> 00:06:45.649 align:start position:0%
so this is the same code this is the
 

00:06:45.649 --> 00:06:49.089 align:start position:0%
so this is the same code this is the
same<00:06:45.889><c> thing</c><00:06:46.129><c> now</c><00:06:46.699><c> running</c><00:06:47.209><c> on</c><00:06:47.300><c> the</c><00:06:47.509><c> GPU</c><00:06:47.919><c> so</c><00:06:48.919><c> yes</c>

00:06:49.089 --> 00:06:49.099 align:start position:0%
same thing now running on the GPU so yes
 

00:06:49.099 --> 00:06:51.219 align:start position:0%
same thing now running on the GPU so yes
that's<00:06:49.309><c> true</c><00:06:49.519><c> you</c><00:06:49.879><c> can</c><00:06:49.999><c> take</c><00:06:50.300><c> any</c><00:06:50.569><c> formality</c>

00:06:51.219 --> 00:06:51.229 align:start position:0%
that's true you can take any formality
 

00:06:51.229 --> 00:06:53.649 align:start position:0%
that's true you can take any formality
program<00:06:51.649><c> and</c><00:06:51.829><c> run</c><00:06:52.399><c> it</c><00:06:52.639><c> in</c><00:06:52.879><c> thousands</c><00:06:53.509><c> of</c>

00:06:53.649 --> 00:06:53.659 align:start position:0%
program and run it in thousands of
 

00:06:53.659 --> 00:06:56.019 align:start position:0%
program and run it in thousands of
course<00:06:54.139><c> in</c><00:06:54.409><c> parallel</c><00:06:54.919><c> with</c><00:06:55.339><c> no</c><00:06:55.639><c> program</c>

00:06:56.019 --> 00:06:56.029 align:start position:0%
course in parallel with no program
 

00:06:56.029 --> 00:06:58.540 align:start position:0%
course in parallel with no program
effort<00:06:56.509><c> at</c><00:06:56.779><c> all</c><00:06:56.959><c> and</c><00:06:57.139><c> we</c><00:06:57.469><c> can</c><00:06:57.499><c> get</c><00:06:57.829><c> real</c><00:06:58.159><c> speed</c>

00:06:58.540 --> 00:06:58.550 align:start position:0%
effort at all and we can get real speed
 

00:06:58.550 --> 00:07:00.819 align:start position:0%
effort at all and we can get real speed
ups<00:06:58.729><c> with</c><00:06:58.999><c> that</c><00:06:59.269><c> so</c><00:06:59.869><c> this</c><00:07:00.050><c> is</c><00:07:00.110><c> something</c><00:07:00.379><c> that</c>

00:07:00.819 --> 00:07:00.829 align:start position:0%
ups with that so this is something that
 

00:07:00.829 --> 00:07:03.159 align:start position:0%
ups with that so this is something that
also<00:07:01.129><c> no</c><00:07:01.610><c> other</c><00:07:01.639><c> functional</c><00:07:02.539><c> language</c><00:07:02.899><c> in</c><00:07:03.049><c> the</c>

00:07:03.159 --> 00:07:03.169 align:start position:0%
also no other functional language in the
 

00:07:03.169 --> 00:07:04.899 align:start position:0%
also no other functional language in the
world<00:07:03.379><c> is</c><00:07:03.739><c> capable</c><00:07:04.009><c> of</c><00:07:04.369><c> doing</c><00:07:04.639><c> you</c><00:07:04.699><c> can't</c>

00:07:04.899 --> 00:07:04.909 align:start position:0%
world is capable of doing you can't
 

00:07:04.909 --> 00:07:07.149 align:start position:0%
world is capable of doing you can't
compile<00:07:05.239><c> Hosko</c><00:07:05.749><c> it</c><00:07:06.259><c> is</c><00:07:06.529><c> anything</c><00:07:06.829><c> that</c><00:07:06.979><c> you</c>

00:07:07.149 --> 00:07:07.159 align:start position:0%
compile Hosko it is anything that you
 

00:07:07.159 --> 00:07:09.009 align:start position:0%
compile Hosko it is anything that you
think<00:07:07.429><c> to</c><00:07:07.489><c> the</c><00:07:07.669><c> GPU</c><00:07:07.909><c> and</c><00:07:08.149><c> formality</c><00:07:08.689><c> can</c><00:07:08.899><c> do</c>

00:07:09.009 --> 00:07:09.019 align:start position:0%
think to the GPU and formality can do
 

00:07:09.019 --> 00:07:13.899 align:start position:0%
think to the GPU and formality can do
that<00:07:10.479><c> we</c><00:07:11.479><c> believe</c><00:07:11.719><c> that</c><00:07:11.899><c> with</c><00:07:12.259><c> a</c><00:07:12.909><c> sufficiently</c>

00:07:13.899 --> 00:07:13.909 align:start position:0%
that we believe that with a sufficiently
 

00:07:13.909 --> 00:07:16.209 align:start position:0%
that we believe that with a sufficiently
major<00:07:14.329><c> compiler</c><00:07:14.869><c> we</c><00:07:15.379><c> could</c><00:07:15.649><c> beat</c><00:07:15.919><c> those</c>

00:07:16.209 --> 00:07:16.219 align:start position:0%
major compiler we could beat those
 

00:07:16.219 --> 00:07:20.319 align:start position:0%
major compiler we could beat those
language<00:07:17.679><c> so</c><00:07:18.679><c> how</c><00:07:18.860><c> how</c><00:07:19.519><c> can</c><00:07:19.579><c> a</c><00:07:19.819><c> high-level</c>

00:07:20.319 --> 00:07:20.329 align:start position:0%
language so how how can a high-level
 

00:07:20.329 --> 00:07:23.079 align:start position:0%
language so how how can a high-level
language<00:07:20.629><c> like</c><00:07:21.110><c> four</c><00:07:21.319><c> miles</c><00:07:21.610><c> have</c><00:07:22.610><c> no</c><00:07:22.789><c> garbage</c>

00:07:23.079 --> 00:07:23.089 align:start position:0%
language like four miles have no garbage
 

00:07:23.089 --> 00:07:24.819 align:start position:0%
language like four miles have no garbage
collection<00:07:23.539><c> how</c><00:07:23.869><c> can</c><00:07:24.050><c> it</c><00:07:24.139><c> often</c><00:07:24.349><c> be</c><00:07:24.499><c> fast</c><00:07:24.709><c> on</c>

00:07:24.819 --> 00:07:24.829 align:start position:0%
collection how can it often be fast on
 

00:07:24.829 --> 00:07:27.189 align:start position:0%
collection how can it often be fast on
the<00:07:24.919><c> Haskell</c><00:07:25.279><c> how</c><00:07:26.059><c> can</c><00:07:26.269><c> it</c><00:07:26.419><c> ship</c><00:07:26.659><c> the</c><00:07:26.809><c> targets</c>

00:07:27.189 --> 00:07:27.199 align:start position:0%
the Haskell how can it ship the targets
 

00:07:27.199 --> 00:07:36.759 align:start position:0%
the Haskell how can it ship the targets
the<00:07:27.349><c> VM</c><00:07:27.709><c> or</c><00:07:28.009><c> even</c><00:07:28.789><c> the</c><00:07:28.879><c> GPU</c><00:07:31.239><c> memories</c><00:07:35.769><c> those</c>

00:07:36.759 --> 00:07:36.769 align:start position:0%
the VM or even the GPU memories those
 

00:07:36.769 --> 00:07:39.579 align:start position:0%
the VM or even the GPU memories those
are<00:07:37.069><c> the</c><00:07:37.189><c> four</c><00:07:37.399><c> axes</c><00:07:37.879><c> of</c><00:07:37.909><c> formality</c><00:07:38.719><c> linear</c>

00:07:39.579 --> 00:07:39.589 align:start position:0%
are the four axes of formality linear
 

00:07:39.589 --> 00:07:43.209 align:start position:0%
are the four axes of formality linear
types<00:07:39.800><c> like</c><00:07:40.519><c> rows</c><00:07:41.019><c> values</c><00:07:42.019><c> can</c><00:07:42.229><c> only</c><00:07:42.469><c> exist</c><00:07:42.919><c> in</c>

00:07:43.209 --> 00:07:43.219 align:start position:0%
types like rows values can only exist in
 

00:07:43.219 --> 00:07:45.129 align:start position:0%
types like rows values can only exist in
one<00:07:43.459><c> place</c><00:07:43.759><c> at</c><00:07:43.999><c> the</c><00:07:44.149><c> same</c><00:07:44.300><c> time</c><00:07:44.569><c> making</c>

00:07:45.129 --> 00:07:45.139 align:start position:0%
one place at the same time making
 

00:07:45.139 --> 00:07:47.739 align:start position:0%
one place at the same time making
garbage<00:07:45.559><c> collection</c><00:07:46.039><c> unnecessary</c><00:07:46.639><c> memory</c><00:07:47.599><c> is</c>

00:07:47.739 --> 00:07:47.749 align:start position:0%
garbage collection unnecessary memory is
 

00:07:47.749 --> 00:07:50.559 align:start position:0%
garbage collection unnecessary memory is
freed<00:07:48.079><c> when</c><00:07:48.559><c> values</c><00:07:49.039><c> go</c><00:07:49.249><c> out</c><00:07:49.519><c> of</c><00:07:49.729><c> scope</c><00:07:49.999><c> simple</c>

00:07:50.559 --> 00:07:50.569 align:start position:0%
freed when values go out of scope simple
 

00:07:50.569 --> 00:07:52.659 align:start position:0%
freed when values go out of scope simple
as<00:07:50.719><c> that</c><00:07:50.979><c> these</c><00:07:51.979><c> clones</c>

00:07:52.659 --> 00:07:52.669 align:start position:0%
as that these clones
 

00:07:52.669 --> 00:07:55.779 align:start position:0%
as that these clones
unlike<00:07:53.479><c> rust</c><00:07:53.809><c> values</c><00:07:54.619><c> can</c><00:07:54.769><c> be</c><00:07:54.829><c> cloned</c><00:07:55.099><c> with</c><00:07:55.399><c> no</c>

00:07:55.779 --> 00:07:55.789 align:start position:0%
unlike rust values can be cloned with no
 

00:07:55.789 --> 00:07:59.229 align:start position:0%
unlike rust values can be cloned with no
cost<00:07:56.269><c> make</c><00:07:56.869><c> linearity</c><00:07:57.679><c> much</c><00:07:58.189><c> less</c><00:07:58.579><c> painful</c><00:07:58.849><c> as</c>

00:07:59.229 --> 00:07:59.239 align:start position:0%
cost make linearity much less painful as
 

00:07:59.239 --> 00:08:03.249 align:start position:0%
cost make linearity much less painful as
we<00:07:59.779><c> don't</c><00:08:00.169><c> need</c><00:08:00.349><c> to</c><00:08:00.559><c> borrow</c><00:08:00.800><c> values</c><00:08:01.309><c> so</c><00:08:02.259><c> that's</c>

00:08:03.249 --> 00:08:03.259 align:start position:0%
we don't need to borrow values so that's
 

00:08:03.259 --> 00:08:05.189 align:start position:0%
we don't need to borrow values so that's
possible<00:08:03.589><c> because</c><00:08:03.739><c> copies</c><00:08:04.309><c> are</c><00:08:04.429><c> made</c><00:08:04.459><c> lazily</c>

00:08:05.189 --> 00:08:05.199 align:start position:0%
possible because copies are made lazily
 

00:08:05.199 --> 00:08:08.109 align:start position:0%
possible because copies are made lazily
on<00:08:06.199><c> better</c><00:08:06.439><c> optimality</c><00:08:06.979><c> functions</c><00:08:07.969><c> are</c>

00:08:08.109 --> 00:08:08.119 align:start position:0%
on better optimality functions are
 

00:08:08.119 --> 00:08:10.659 align:start position:0%
on better optimality functions are
reduced<00:08:08.449><c> optimally</c><00:08:09.110><c> this</c><00:08:09.619><c> allows</c><00:08:09.919><c> an</c><00:08:10.189><c> insane</c>

00:08:10.659 --> 00:08:10.669 align:start position:0%
reduced optimally this allows an insane
 

00:08:10.669 --> 00:08:13.329 align:start position:0%
reduced optimally this allows an insane
amount<00:08:10.909><c> of</c><00:08:11.389><c> rot</c><00:08:11.749><c> and</c><00:08:12.019><c> fusion</c><00:08:12.379><c> to</c><00:08:12.740><c> happen</c>

00:08:13.329 --> 00:08:13.339 align:start position:0%
amount of rot and fusion to happen
 

00:08:13.339 --> 00:08:16.270 align:start position:0%
amount of rot and fusion to happen
breaking<00:08:13.969><c> down</c><00:08:14.079><c> bloated</c><00:08:15.079><c> high-level</c><00:08:15.679><c> code</c>

00:08:16.270 --> 00:08:16.280 align:start position:0%
breaking down bloated high-level code
 

00:08:16.280 --> 00:08:19.330 align:start position:0%
breaking down bloated high-level code
into<00:08:16.550><c> small</c><00:08:16.820><c> lightweight</c><00:08:17.240><c> computations</c><00:08:18.110><c> if</c><00:08:18.560><c> a</c>

00:08:19.330 --> 00:08:19.340 align:start position:0%
into small lightweight computations if a
 

00:08:19.340 --> 00:08:21.879 align:start position:0%
into small lightweight computations if a
strong<00:08:19.700><c> confluency</c><00:08:20.389><c> evaluation</c><00:08:21.139><c> is</c><00:08:21.320><c> shrunken</c>

00:08:21.879 --> 00:08:21.889 align:start position:0%
strong confluency evaluation is shrunken
 

00:08:21.889 --> 00:08:24.730 align:start position:0%
strong confluency evaluation is shrunken
fluently<00:08:22.310><c> confluent</c><00:08:23.210><c> so</c><00:08:23.870><c> the</c><00:08:24.410><c> order</c><00:08:24.620><c> of</c>

00:08:24.730 --> 00:08:24.740 align:start position:0%
fluently confluent so the order of
 

00:08:24.740 --> 00:08:27.190 align:start position:0%
fluently confluent so the order of
execution<00:08:25.240><c> doesn't</c><00:08:26.240><c> change</c><00:08:26.630><c> the</c><00:08:26.870><c> required</c>

00:08:27.190 --> 00:08:27.200 align:start position:0%
execution doesn't change the required
 

00:08:27.200 --> 00:08:30.070 align:start position:0%
execution doesn't change the required
work<00:08:27.440><c> to</c><00:08:27.620><c> complete</c><00:08:28.120><c> the</c><00:08:29.120><c> computation</c><00:08:29.780><c> this</c>

00:08:30.070 --> 00:08:30.080 align:start position:0%
work to complete the computation this
 

00:08:30.080 --> 00:08:32.320 align:start position:0%
work to complete the computation this
allows<00:08:30.550><c> reductions</c><00:08:31.550><c> to</c><00:08:31.639><c> take</c><00:08:31.790><c> place</c><00:08:31.970><c> in</c><00:08:32.150><c> any</c>

00:08:32.320 --> 00:08:32.330 align:start position:0%
allows reductions to take place in any
 

00:08:32.330 --> 00:08:37.779 align:start position:0%
allows reductions to take place in any
order<00:08:32.840><c> even</c><00:08:33.110><c> in</c><00:08:33.560><c> parallel</c><00:08:33.890><c> so</c><00:08:36.490><c> all</c><00:08:37.490><c> those</c>

00:08:37.779 --> 00:08:37.789 align:start position:0%
order even in parallel so all those
 

00:08:37.789 --> 00:08:39.550 align:start position:0%
order even in parallel so all those
things<00:08:38.210><c> allows</c><00:08:38.719><c> for</c><00:08:38.990><c> mallet</c><00:08:39.289><c> should</c><00:08:39.469><c> be</c>

00:08:39.550 --> 00:08:39.560 align:start position:0%
things allows for mallet should be
 

00:08:39.560 --> 00:08:41.409 align:start position:0%
things allows for mallet should be
compiled<00:08:39.919><c> to</c><00:08:40.159><c> a</c><00:08:40.219><c> new</c><00:08:40.460><c> model</c><00:08:40.909><c> of</c><00:08:41.090><c> computation</c>

00:08:41.409 --> 00:08:41.419 align:start position:0%
compiled to a new model of computation
 

00:08:41.419 --> 00:08:44.170 align:start position:0%
compiled to a new model of computation
called<00:08:42.349><c> interaction</c><00:08:42.890><c> combinators</c><00:08:43.580><c> which</c>

00:08:44.170 --> 00:08:44.180 align:start position:0%
called interaction combinators which
 

00:08:44.180 --> 00:08:46.630 align:start position:0%
called interaction combinators which
combines<00:08:44.690><c> the</c><00:08:44.840><c> best</c><00:08:45.320><c> aspects</c><00:08:46.010><c> of</c><00:08:46.040><c> Turing</c>

00:08:46.630 --> 00:08:46.640 align:start position:0%
combines the best aspects of Turing
 

00:08:46.640 --> 00:08:49.420 align:start position:0%
combines the best aspects of Turing
machines<00:08:47.000><c> and</c><00:08:47.240><c> the</c><00:08:47.840><c> lambda</c><00:08:48.020><c> calculus</c><00:08:48.560><c> that's</c>

00:08:49.420 --> 00:08:49.430 align:start position:0%
machines and the lambda calculus that's
 

00:08:49.430 --> 00:08:51.730 align:start position:0%
machines and the lambda calculus that's
what<00:08:49.730><c> allows</c><00:08:49.970><c> us</c><00:08:50.240><c> to</c><00:08:50.510><c> run</c><00:08:50.720><c> and</c><00:08:51.050><c> to</c><00:08:51.290><c> run</c><00:08:51.440><c> on</c><00:08:51.620><c> the</c>

00:08:51.730 --> 00:08:51.740 align:start position:0%
what allows us to run and to run on the
 

00:08:51.740 --> 00:08:54.400 align:start position:0%
what allows us to run and to run on the
GPU<00:08:51.770><c> to</c><00:08:52.280><c> compile</c><00:08:52.850><c> to</c><00:08:53.030><c> JVM</c><00:08:53.480><c> and</c><00:08:53.660><c> everything</c>

00:08:54.400 --> 00:08:54.410 align:start position:0%
GPU to compile to JVM and everything
 

00:08:54.410 --> 00:08:57.130 align:start position:0%
GPU to compile to JVM and everything
else<00:08:54.589><c> we</c><00:08:54.860><c> presented</c><00:08:55.339><c> so</c><00:08:55.520><c> far</c><00:08:55.550><c> if</c><00:08:56.360><c> that</c><00:08:56.750><c> sounds</c>

00:08:57.130 --> 00:08:57.140 align:start position:0%
else we presented so far if that sounds
 

00:08:57.140 --> 00:08:59.140 align:start position:0%
else we presented so far if that sounds
fun<00:08:57.380><c> to</c><00:08:57.589><c> you</c><00:08:57.620><c> and</c><00:08:57.920><c> they</c><00:08:58.220><c> really</c><00:08:58.460><c> think</c><00:08:58.970><c> that's</c>

00:08:59.140 --> 00:08:59.150 align:start position:0%
fun to you and they really think that's
 

00:08:59.150 --> 00:09:00.430 align:start position:0%
fun to you and they really think that's
very<00:08:59.420><c> fun</c><00:08:59.600><c> please</c><00:08:59.870><c> check</c><00:09:00.080><c> the</c><00:09:00.230><c> link</c><00:09:00.380><c> below</c>

00:09:00.430 --> 00:09:00.440 align:start position:0%
very fun please check the link below
 

00:09:00.440 --> 00:09:03.460 align:start position:0%
very fun please check the link below
where<00:09:01.220><c> we</c><00:09:01.520><c> explain</c><00:09:02.000><c> this</c><00:09:02.300><c> model</c><00:09:02.750><c> a</c><00:09:02.900><c> little</c><00:09:03.320><c> bit</c>

00:09:03.460 --> 00:09:03.470 align:start position:0%
where we explain this model a little bit
 

00:09:03.470 --> 00:09:07.650 align:start position:0%
where we explain this model a little bit
better<00:09:03.970><c> and</c><00:09:04.970><c> that's</c><00:09:05.870><c> it</c><00:09:06.080><c> formality</c><00:09:06.920><c> turns</c>

00:09:07.650 --> 00:09:07.660 align:start position:0%
better and that's it formality turns
 

00:09:07.660 --> 00:09:10.630 align:start position:0%
better and that's it formality turns
scientific<00:09:08.660><c> scientific</c><00:09:09.589><c> breakthroughs</c><00:09:10.400><c> into</c>

00:09:10.630 --> 00:09:10.640 align:start position:0%
scientific scientific breakthroughs into
 

00:09:10.640 --> 00:09:14.079 align:start position:0%
scientific scientific breakthroughs into
a<00:09:10.670><c> real-world</c><00:09:10.940><c> language</c><00:09:11.480><c> so</c><00:09:12.550><c> with</c><00:09:13.550><c> this</c><00:09:13.730><c> we</c>

00:09:14.079 --> 00:09:14.089 align:start position:0%
a real-world language so with this we
 

00:09:14.089 --> 00:09:17.079 align:start position:0%
a real-world language so with this we
are<00:09:14.120><c> closer</c><00:09:14.420><c> to</c><00:09:15.100><c> building</c><00:09:16.100><c> the</c><00:09:16.430><c> moon</c><00:09:16.670><c> browser</c>

00:09:17.079 --> 00:09:17.089 align:start position:0%
are closer to building the moon browser
 

00:09:17.089 --> 00:09:19.950 align:start position:0%
are closer to building the moon browser
as<00:09:17.480><c> we</c><00:09:17.810><c> are</c><00:09:18.160><c> originally</c><00:09:19.160><c> envisioned</c>

00:09:19.950 --> 00:09:19.960 align:start position:0%
as we are originally envisioned
 

00:09:19.960 --> 00:09:23.310 align:start position:0%
as we are originally envisioned
formality<00:09:20.960><c> is</c><00:09:21.020><c> not</c><00:09:21.290><c> officially</c><00:09:22.070><c> released</c><00:09:22.400><c> yet</c>

00:09:23.310 --> 00:09:23.320 align:start position:0%
formality is not officially released yet
 

00:09:23.320 --> 00:09:27.220 align:start position:0%
formality is not officially released yet
there's<00:09:24.320><c> a</c><00:09:24.410><c> lot</c><00:09:25.160><c> of</c><00:09:25.310><c> boring</c><00:09:25.820><c> work</c><00:09:26.089><c> to</c><00:09:26.270><c> do</c><00:09:26.420><c> but</c>

00:09:27.220 --> 00:09:27.230 align:start position:0%
there's a lot of boring work to do but
 

00:09:27.230 --> 00:09:29.770 align:start position:0%
there's a lot of boring work to do but
the<00:09:28.040><c> fundamental</c><00:09:28.550><c> parts</c><00:09:28.850><c> are</c><00:09:29.000><c> done</c><00:09:29.330><c> and</c><00:09:29.570><c> you</c>

00:09:29.770 --> 00:09:29.780 align:start position:0%
the fundamental parts are done and you
 

00:09:29.780 --> 00:09:35.110 align:start position:0%
the fundamental parts are done and you
can<00:09:29.990><c> check</c><00:09:30.260><c> it</c><00:09:30.470><c> today</c><00:09:30.860><c> on</c><00:09:31.160><c> github</c><00:09:32.710><c> ok</c><00:09:33.710><c> so</c><00:09:34.640><c> just</c>

00:09:35.110 --> 00:09:35.120 align:start position:0%
can check it today on github ok so just
 

00:09:35.120 --> 00:09:38.140 align:start position:0%
can check it today on github ok so just
a<00:09:35.630><c> Lansing</c><00:09:36.110><c> there's</c><00:09:37.100><c> a</c><00:09:37.220><c> brilliant</c><00:09:37.550><c> researcher</c>

00:09:38.140 --> 00:09:38.150 align:start position:0%
a Lansing there's a brilliant researcher
 

00:09:38.150 --> 00:09:40.450 align:start position:0%
a Lansing there's a brilliant researcher
called<00:09:38.390><c> ørestad</c><00:09:39.050><c> that</c><00:09:39.620><c> created</c><00:09:40.070><c> a</c><00:09:40.190><c> type</c>

00:09:40.450 --> 00:09:40.460 align:start position:0%
called ørestad that created a type
 

00:09:40.460 --> 00:09:42.910 align:start position:0%
called ørestad that created a type
theory<00:09:40.790><c> that</c><00:09:41.180><c> fits</c><00:09:41.240><c> in</c><00:09:41.780><c> a</c><00:09:41.870><c> single</c><00:09:42.200><c> slide</c><00:09:42.410><c> it's</c>

00:09:42.910 --> 00:09:42.920 align:start position:0%
theory that fits in a single slide it's
 

00:09:42.920 --> 00:09:45.780 align:start position:0%
theory that fits in a single slide it's
that<00:09:43.339><c> thing</c><00:09:43.880><c> you</c><00:09:43.910><c> are</c><00:09:44.150><c> seeing</c><00:09:44.360><c> here</c><00:09:44.810><c> that</c>

00:09:45.780 --> 00:09:45.790 align:start position:0%
that thing you are seeing here that
 

00:09:45.790 --> 00:09:49.240 align:start position:0%
that thing you are seeing here that
theory<00:09:46.790><c> is</c><00:09:47.150><c> not</c><00:09:47.420><c> only</c><00:09:48.080><c> very</c><00:09:48.410><c> powerful</c><00:09:49.010><c> more</c>

00:09:49.240 --> 00:09:49.250 align:start position:0%
theory is not only very powerful more
 

00:09:49.250 --> 00:09:52.540 align:start position:0%
theory is not only very powerful more
powerful<00:09:49.670><c> than</c><00:09:50.120><c> angular</c><00:09:50.660><c> and</c><00:09:51.650><c> eateries</c><00:09:52.520><c> and</c>

00:09:52.540 --> 00:09:52.550 align:start position:0%
powerful than angular and eateries and
 

00:09:52.550 --> 00:09:55.120 align:start position:0%
powerful than angular and eateries and
is<00:09:53.030><c> about</c><00:09:53.270><c> another</c><00:09:53.600><c> language</c><00:09:53.870><c> but</c><00:09:54.560><c> it's</c><00:09:54.800><c> also</c>

00:09:55.120 --> 00:09:55.130 align:start position:0%
is about another language but it's also
 

00:09:55.130 --> 00:09:58.750 align:start position:0%
is about another language but it's also
much<00:09:55.550><c> much</c><00:09:55.850><c> simpler</c><00:09:56.330><c> and</c><00:09:57.520><c> sadly</c><00:09:58.520><c> we</c><00:09:58.640><c> don't</c>

00:09:58.750 --> 00:09:58.760 align:start position:0%
much much simpler and sadly we don't
 

00:09:58.760 --> 00:10:00.880 align:start position:0%
much much simpler and sadly we don't
have<00:09:59.030><c> enough</c><00:09:59.300><c> time</c><00:09:59.570><c> to</c><00:10:00.110><c> explain</c><00:10:00.170><c> how</c><00:10:00.500><c> this</c>

00:10:00.880 --> 00:10:00.890 align:start position:0%
have enough time to explain how this
 

00:10:00.890 --> 00:10:03.730 align:start position:0%
have enough time to explain how this
work<00:10:01.130><c> today</c><00:10:01.610><c> but</c><00:10:02.240><c> this</c><00:10:02.420><c> is</c><00:10:02.690><c> what</c><00:10:03.140><c> will</c><00:10:03.410><c> be</c><00:10:03.440><c> used</c>

00:10:03.730 --> 00:10:03.740 align:start position:0%
work today but this is what will be used
 

00:10:03.740 --> 00:10:06.130 align:start position:0%
work today but this is what will be used
by<00:10:03.950><c> for</c><00:10:04.250><c> mileage</c><00:10:04.520><c> to</c><00:10:04.970><c> ensure</c><00:10:05.300><c> mathematical</c>

00:10:06.130 --> 00:10:06.140 align:start position:0%
by for mileage to ensure mathematical
 

00:10:06.140 --> 00:10:07.990 align:start position:0%
by for mileage to ensure mathematical
consistence<00:10:06.680><c> which</c><00:10:07.100><c> is</c><00:10:07.310><c> which</c><00:10:07.640><c> is</c><00:10:07.670><c> something</c>

00:10:07.990 --> 00:10:08.000 align:start position:0%
consistence which is which is something
 

00:10:08.000 --> 00:10:10.300 align:start position:0%
consistence which is which is something
very<00:10:08.300><c> hard</c><00:10:08.420><c> to</c><00:10:08.810><c> do</c><00:10:08.930><c> in</c><00:10:09.140><c> proof</c><00:10:09.350><c> language</c><00:10:09.710><c> and</c><00:10:09.890><c> we</c>

00:10:10.300 --> 00:10:10.310 align:start position:0%
very hard to do in proof language and we
 

00:10:10.310 --> 00:10:13.060 align:start position:0%
very hard to do in proof language and we
actually<00:10:10.460><c> gave</c><00:10:11.089><c> a</c><00:10:11.270><c> bread</c><00:10:11.510><c> for</c><00:10:11.810><c> our</c><00:10:12.020><c> stop</c><00:10:12.500><c> to</c>

00:10:13.060 --> 00:10:13.070 align:start position:0%
actually gave a bread for our stop to
 

00:10:13.070 --> 00:10:14.680 align:start position:0%
actually gave a bread for our stop to
make<00:10:13.250><c> this</c><00:10:13.430><c> possible</c><00:10:13.700><c> so</c><00:10:14.000><c> we</c><00:10:14.300><c> are</c><00:10:14.390><c> very</c>

00:10:14.680 --> 00:10:14.690 align:start position:0%
make this possible so we are very
 

00:10:14.690 --> 00:10:18.310 align:start position:0%
make this possible so we are very
thankful<00:10:15.020><c> to</c><00:10:15.740><c> him</c><00:10:15.860><c> for</c><00:10:16.100><c> that</c><00:10:16.280><c> and</c><00:10:17.140><c> that's</c><00:10:18.140><c> it</c>

00:10:18.310 --> 00:10:18.320 align:start position:0%
thankful to him for that and that's it
 

00:10:18.320 --> 00:10:20.930 align:start position:0%
thankful to him for that and that's it
thank<00:10:18.890><c> you</c><00:10:18.950><c> very</c><00:10:19.130><c> much</c><00:10:19.310><c> sorry</c><00:10:19.790><c> about</c><00:10:20.120><c> Java</c>

00:10:20.930 --> 00:10:20.940 align:start position:0%
thank you very much sorry about Java
 

00:10:20.940 --> 00:10:33.129 align:start position:0%
thank you very much sorry about Java
[Applause]

00:10:33.129 --> 00:10:33.139 align:start position:0%
 
 

00:10:33.139 --> 00:10:35.199 align:start position:0%
 
you