WEBVTT
Kind: captions
Language: en

00:00:04.620 --> 00:00:14.900 align:start position:0%
 
[Music]

00:00:14.900 --> 00:00:14.910 align:start position:0%
 
 

00:00:14.910 --> 00:00:16.710 align:start position:0%
 
[Music]

00:00:16.710 --> 00:00:16.720 align:start position:0%
[Music]
 

00:00:16.720 --> 00:00:19.470 align:start position:0%
[Music]
hello<00:00:17.119><c> everyone</c><00:00:18.119><c> uh</c><00:00:18.320><c> my</c><00:00:18.480><c> name</c><00:00:18.600><c> is</c><00:00:18.720><c> Robert</c><00:00:19.400><c> this</c>

00:00:19.470 --> 00:00:19.480 align:start position:0%
hello everyone uh my name is Robert this
 

00:00:19.480 --> 00:00:22.189 align:start position:0%
hello everyone uh my name is Robert this
is<00:00:19.680><c> Jack</c><00:00:20.680><c> and</c><00:00:21.160><c> uh</c><00:00:21.320><c> we're</c><00:00:21.560><c> currently</c><00:00:21.920><c> working</c>

00:00:22.189 --> 00:00:22.199 align:start position:0%
is Jack and uh we're currently working
 

00:00:22.199 --> 00:00:25.109 align:start position:0%
is Jack and uh we're currently working
on<00:00:22.359><c> our</c><00:00:22.519><c> Master</c><00:00:22.960><c> CIS</c><00:00:23.519><c> in</c><00:00:24.000><c> computer</c><00:00:24.400><c> science</c>

00:00:25.109 --> 00:00:25.119 align:start position:0%
on our Master CIS in computer science
 

00:00:25.119 --> 00:00:27.550 align:start position:0%
on our Master CIS in computer science
and<00:00:25.640><c> uh</c><00:00:26.199><c> we're</c><00:00:26.720><c> working</c><00:00:27.080><c> on</c><00:00:27.199><c> a</c><00:00:27.320><c> new</c>

00:00:27.550 --> 00:00:27.560 align:start position:0%
and uh we're working on a new
 

00:00:27.560 --> 00:00:30.230 align:start position:0%
and uh we're working on a new
programming<00:00:28.039><c> language</c><00:00:28.439><c> for</c><00:00:28.599><c> the</c><00:00:28.800><c> evm</c><00:00:29.800><c> and</c><00:00:30.119><c> so</c>

00:00:30.230 --> 00:00:30.240 align:start position:0%
programming language for the evm and so
 

00:00:30.240 --> 00:00:31.990 align:start position:0%
programming language for the evm and so
we're<00:00:30.480><c> here</c><00:00:30.759><c> to</c><00:00:30.920><c> talk</c><00:00:31.119><c> about</c><00:00:31.400><c> how</c><00:00:31.640><c> smart</c>

00:00:31.990 --> 00:00:32.000 align:start position:0%
we're here to talk about how smart
 

00:00:32.000 --> 00:00:33.990 align:start position:0%
we're here to talk about how smart
contracts<00:00:32.520><c> can</c><00:00:32.640><c> be</c><00:00:32.759><c> a</c><00:00:32.960><c> perfect</c><00:00:33.280><c> fit</c><00:00:33.520><c> for</c><00:00:33.719><c> a</c>

00:00:33.990 --> 00:00:34.000 align:start position:0%
contracts can be a perfect fit for a
 

00:00:34.000 --> 00:00:35.950 align:start position:0%
contracts can be a perfect fit for a
dependently<00:00:34.559><c> typed</c><00:00:34.879><c> functional</c><00:00:35.360><c> language</c>

00:00:35.950 --> 00:00:35.960 align:start position:0%
dependently typed functional language
 

00:00:35.960 --> 00:00:38.750 align:start position:0%
dependently typed functional language
and<00:00:36.280><c> why</c><00:00:36.440><c> we</c><00:00:36.559><c> want</c><00:00:36.719><c> to</c><00:00:36.840><c> do</c><00:00:37.320><c> this</c><00:00:38.320><c> uh</c><00:00:38.440><c> we</c><00:00:38.559><c> will</c>

00:00:38.750 --> 00:00:38.760 align:start position:0%
and why we want to do this uh we will
 

00:00:38.760 --> 00:00:41.790 align:start position:0%
and why we want to do this uh we will
also<00:00:39.000><c> have</c><00:00:39.120><c> a</c><00:00:39.239><c> small</c><00:00:39.559><c> example</c><00:00:40.079><c> of</c><00:00:41.079><c> uh</c><00:00:41.280><c> how</c><00:00:41.640><c> an</c>

00:00:41.790 --> 00:00:41.800 align:start position:0%
also have a small example of uh how an
 

00:00:41.800 --> 00:00:43.350 align:start position:0%
also have a small example of uh how an
expressive<00:00:42.280><c> type</c><00:00:42.559><c> system</c><00:00:42.879><c> can</c><00:00:43.000><c> help</c><00:00:43.200><c> in</c>

00:00:43.350 --> 00:00:43.360 align:start position:0%
expressive type system can help in
 

00:00:43.360 --> 00:00:44.590 align:start position:0%
expressive type system can help in
contract

00:00:44.590 --> 00:00:44.600 align:start position:0%
contract
 

00:00:44.600 --> 00:00:47.270 align:start position:0%
contract
development<00:00:45.600><c> so</c><00:00:46.239><c> when</c><00:00:46.360><c> you</c><00:00:46.520><c> deploy</c><00:00:46.840><c> a</c><00:00:46.960><c> smart</c>

00:00:47.270 --> 00:00:47.280 align:start position:0%
development so when you deploy a smart
 

00:00:47.280 --> 00:00:49.470 align:start position:0%
development so when you deploy a smart
contract<00:00:47.600><c> to</c><00:00:47.800><c> production</c><00:00:48.800><c> uh</c><00:00:48.920><c> you</c><00:00:49.039><c> want</c><00:00:49.160><c> to</c><00:00:49.280><c> be</c>

00:00:49.470 --> 00:00:49.480 align:start position:0%
contract to production uh you want to be
 

00:00:49.480 --> 00:00:51.990 align:start position:0%
contract to production uh you want to be
really<00:00:49.719><c> sure</c><00:00:50.360><c> that</c><00:00:50.800><c> it</c><00:00:51.000><c> behaves</c><00:00:51.480><c> precisely</c><00:00:51.879><c> as</c>

00:00:51.990 --> 00:00:52.000 align:start position:0%
really sure that it behaves precisely as
 

00:00:52.000 --> 00:00:54.750 align:start position:0%
really sure that it behaves precisely as
you<00:00:52.120><c> intended</c><00:00:52.640><c> to</c><00:00:53.640><c> um</c><00:00:53.960><c> so</c><00:00:54.280><c> the</c><00:00:54.399><c> more</c><00:00:54.600><c> the</c>

00:00:54.750 --> 00:00:54.760 align:start position:0%
you intended to um so the more the
 

00:00:54.760 --> 00:00:57.590 align:start position:0%
you intended to um so the more the
compilator<00:00:55.239><c> can</c><00:00:55.399><c> catch</c><00:00:55.640><c> for</c><00:00:55.800><c> you</c><00:00:56.000><c> the</c><00:00:56.600><c> better</c>

00:00:57.590 --> 00:00:57.600 align:start position:0%
compilator can catch for you the better
 

00:00:57.600 --> 00:01:02.029 align:start position:0%
compilator can catch for you the better
so<00:00:58.320><c> we</c><00:00:58.680><c> also</c><00:00:59.680><c> want</c><00:01:00.160><c> to</c><00:01:00.359><c> give</c><00:01:00.840><c> developers</c><00:01:01.840><c> high</c>

00:01:02.029 --> 00:01:02.039 align:start position:0%
so we also want to give developers high
 

00:01:02.039 --> 00:01:05.070 align:start position:0%
so we also want to give developers high
level<00:01:02.640><c> abstraction</c><00:01:03.640><c> uh</c><00:01:03.879><c> of</c><00:01:04.600><c> standard</c>

00:01:05.070 --> 00:01:05.080 align:start position:0%
level abstraction uh of standard
 

00:01:05.080 --> 00:01:08.310 align:start position:0%
level abstraction uh of standard
behavior<00:01:05.720><c> and</c><00:01:05.920><c> common</c><00:01:06.280><c> patterns</c><00:01:07.080><c> stuff</c><00:01:07.439><c> like</c>

00:01:08.310 --> 00:01:08.320 align:start position:0%
behavior and common patterns stuff like
 

00:01:08.320 --> 00:01:10.230 align:start position:0%
behavior and common patterns stuff like
high<00:01:08.560><c> level</c><00:01:08.840><c> cryptography</c><00:01:09.479><c> and</c><00:01:09.640><c> boiler</c><00:01:10.000><c> plate</c>

00:01:10.230 --> 00:01:10.240 align:start position:0%
high level cryptography and boiler plate
 

00:01:10.240 --> 00:01:12.149 align:start position:0%
high level cryptography and boiler plate
for<00:01:10.400><c> errors</c><00:01:10.880><c> and</c>

00:01:12.149 --> 00:01:12.159 align:start position:0%
for errors and
 

00:01:12.159 --> 00:01:14.990 align:start position:0%
for errors and
cleanup<00:01:13.159><c> and</c><00:01:13.439><c> I</c><00:01:13.560><c> hope</c><00:01:13.799><c> that</c><00:01:14.000><c> after</c><00:01:14.240><c> hearing</c>

00:01:14.990 --> 00:01:15.000 align:start position:0%
cleanup and I hope that after hearing
 

00:01:15.000 --> 00:01:16.990 align:start position:0%
cleanup and I hope that after hearing
Greg<00:01:15.400><c> this</c><00:01:15.520><c> morning</c><00:01:16.200><c> uh</c><00:01:16.320><c> you</c><00:01:16.400><c> can</c><00:01:16.560><c> appreciate</c>

00:01:16.990 --> 00:01:17.000 align:start position:0%
Greg this morning uh you can appreciate
 

00:01:17.000 --> 00:01:18.670 align:start position:0%
Greg this morning uh you can appreciate
that<00:01:17.119><c> a</c><00:01:17.280><c> language</c><00:01:17.640><c> that</c><00:01:17.799><c> allows</c><00:01:18.119><c> for</c>

00:01:18.670 --> 00:01:18.680 align:start position:0%
that a language that allows for
 

00:01:18.680 --> 00:01:20.789 align:start position:0%
that a language that allows for
compositionality<00:01:19.560><c> of</c><00:01:19.759><c> combinators</c><00:01:20.560><c> and</c>

00:01:20.789 --> 00:01:20.799 align:start position:0%
compositionality of combinators and
 

00:01:20.799 --> 00:01:24.270 align:start position:0%
compositionality of combinators and
functions<00:01:21.759><c> can</c><00:01:21.880><c> be</c><00:01:22.079><c> really</c><00:01:22.520><c> powerful</c><00:01:23.520><c> lll</c><00:01:24.079><c> is</c>

00:01:24.270 --> 00:01:24.280 align:start position:0%
functions can be really powerful lll is
 

00:01:24.280 --> 00:01:26.030 align:start position:0%
functions can be really powerful lll is
functional<00:01:24.759><c> but</c><00:01:24.920><c> it's</c><00:01:25.119><c> way</c><00:01:25.240><c> too</c><00:01:25.439><c> low</c><00:01:25.680><c> level</c>

00:01:26.030 --> 00:01:26.040 align:start position:0%
functional but it's way too low level
 

00:01:26.040 --> 00:01:29.310 align:start position:0%
functional but it's way too low level
for<00:01:26.280><c> a</c><00:01:26.400><c> lot</c><00:01:26.560><c> of</c><00:01:27.119><c> purposes</c><00:01:28.119><c> uh</c><00:01:28.560><c> so</c><00:01:29.079><c> without</c>

00:01:29.310 --> 00:01:29.320 align:start position:0%
for a lot of purposes uh so without
 

00:01:29.320 --> 00:01:31.830 align:start position:0%
for a lot of purposes uh so without
further<00:01:29.560><c> ado</c><00:01:29.960><c> Jack</c><00:01:30.200><c> will</c><00:01:30.400><c> now</c><00:01:31.119><c> present</c><00:01:31.600><c> two</c>

00:01:31.830 --> 00:01:31.840 align:start position:0%
further ado Jack will now present two
 

00:01:31.840 --> 00:01:34.429 align:start position:0%
further ado Jack will now present two
types<00:01:32.079><c> of</c><00:01:32.240><c> errors</c><00:01:32.799><c> that</c><00:01:33.240><c> programmers</c><00:01:34.079><c> usually</c>

00:01:34.429 --> 00:01:34.439 align:start position:0%
types of errors that programmers usually
 

00:01:34.439 --> 00:01:36.149 align:start position:0%
types of errors that programmers usually
make<00:01:34.720><c> when</c><00:01:34.880><c> they</c><00:01:35.040><c> start</c><00:01:35.320><c> developing</c><00:01:35.759><c> smart</c>

00:01:36.149 --> 00:01:36.159 align:start position:0%
make when they start developing smart
 

00:01:36.159 --> 00:01:38.149 align:start position:0%
make when they start developing smart
contracts<00:01:36.960><c> and</c><00:01:37.159><c> how</c><00:01:37.320><c> we</c><00:01:37.439><c> can</c><00:01:37.600><c> catch</c><00:01:37.799><c> them</c><00:01:38.000><c> at</c>

00:01:38.149 --> 00:01:38.159 align:start position:0%
contracts and how we can catch them at
 

00:01:38.159 --> 00:01:39.830 align:start position:0%
contracts and how we can catch them at
compile

00:01:39.830 --> 00:01:39.840 align:start position:0%
compile
 

00:01:39.840 --> 00:01:44.550 align:start position:0%
compile
time<00:01:41.000><c> right</c><00:01:42.000><c> so</c><00:01:42.840><c> we</c><00:01:43.280><c> look</c><00:01:43.520><c> at</c><00:01:43.680><c> a</c><00:01:44.000><c> simple</c>

00:01:44.550 --> 00:01:44.560 align:start position:0%
time right so we look at a simple
 

00:01:44.560 --> 00:01:47.350 align:start position:0%
time right so we look at a simple
example<00:01:45.320><c> game</c><00:01:45.680><c> of</c><00:01:46.240><c> rock</c><00:01:46.479><c> paper</c><00:01:46.759><c> scissors</c>

00:01:47.350 --> 00:01:47.360 align:start position:0%
example game of rock paper scissors
 

00:01:47.360 --> 00:01:50.630 align:start position:0%
example game of rock paper scissors
that's<00:01:47.560><c> played</c><00:01:47.799><c> for</c><00:01:48.280><c> money</c><00:01:49.280><c> uh</c><00:01:49.560><c> joining</c><00:01:50.200><c> costs</c>

00:01:50.630 --> 00:01:50.640 align:start position:0%
that's played for money uh joining costs
 

00:01:50.640 --> 00:01:53.270 align:start position:0%
that's played for money uh joining costs
10<00:01:50.960><c> ether</c><00:01:51.479><c> and</c><00:01:51.680><c> the</c><00:01:51.840><c> price</c><00:01:52.079><c> is</c><00:01:52.320><c> 20</c><00:01:52.840><c> because</c>

00:01:53.270 --> 00:01:53.280 align:start position:0%
10 ether and the price is 20 because
 

00:01:53.280 --> 00:01:54.709 align:start position:0%
10 ether and the price is 20 because
there's<00:01:53.560><c> two</c>

00:01:54.709 --> 00:01:54.719 align:start position:0%
there's two
 

00:01:54.719 --> 00:01:57.749 align:start position:0%
there's two
players<00:01:55.719><c> uh</c><00:01:56.000><c> and</c><00:01:56.320><c> I</c><00:01:56.560><c> hope</c><00:01:56.759><c> you</c><00:01:56.920><c> know</c><00:01:57.159><c> the</c><00:01:57.320><c> rules</c>

00:01:57.749 --> 00:01:57.759 align:start position:0%
players uh and I hope you know the rules
 

00:01:57.759 --> 00:01:59.310 align:start position:0%
players uh and I hope you know the rules
but<00:01:58.000><c> it</c><00:01:58.320><c> doesn't</c><00:01:58.640><c> really</c><00:01:58.840><c> matter</c><00:01:59.119><c> if</c><00:01:59.200><c> you</c>

00:01:59.310 --> 00:01:59.320 align:start position:0%
but it doesn't really matter if you
 

00:01:59.320 --> 00:02:00.510 align:start position:0%
but it doesn't really matter if you
don't

00:02:00.510 --> 00:02:00.520 align:start position:0%
don't
 

00:02:00.520 --> 00:02:04.709 align:start position:0%
don't
uh<00:02:01.039><c> and</c><00:02:01.560><c> here</c><00:02:01.680><c> is</c><00:02:01.880><c> a</c><00:02:02.520><c> small</c><00:02:02.880><c> example</c><00:02:03.600><c> of</c><00:02:04.159><c> uh</c><00:02:04.399><c> how</c>

00:02:04.709 --> 00:02:04.719 align:start position:0%
uh and here is a small example of uh how
 

00:02:04.719 --> 00:02:07.429 align:start position:0%
uh and here is a small example of uh how
the<00:02:05.000><c> function</c><00:02:05.479><c> that</c><00:02:05.680><c> lets</c><00:02:06.320><c> players</c><00:02:06.880><c> join</c><00:02:07.240><c> the</c>

00:02:07.429 --> 00:02:07.439 align:start position:0%
the function that lets players join the
 

00:02:07.439 --> 00:02:08.749 align:start position:0%
the function that lets players join the
game<00:02:07.960><c> could</c>

00:02:08.749 --> 00:02:08.759 align:start position:0%
game could
 

00:02:08.759 --> 00:02:10.830 align:start position:0%
game could
look<00:02:09.759><c> it's</c><00:02:10.039><c> very</c>

00:02:10.830 --> 00:02:10.840 align:start position:0%
look it's very
 

00:02:10.840 --> 00:02:14.390 align:start position:0%
look it's very
straightforward<00:02:11.840><c> um</c><00:02:12.599><c> it's</c><00:02:13.599><c> the</c><00:02:13.760><c> game</c><00:02:14.200><c> can</c>

00:02:14.390 --> 00:02:14.400 align:start position:0%
straightforward um it's the game can
 

00:02:14.400 --> 00:02:17.589 align:start position:0%
straightforward um it's the game can
only<00:02:14.760><c> be</c><00:02:15.040><c> be</c><00:02:15.160><c> joined</c><00:02:15.519><c> if</c><00:02:15.640><c> it</c><00:02:15.720><c> isn't</c><00:02:16.280><c> full</c><00:02:17.280><c> uh</c>

00:02:17.589 --> 00:02:17.599 align:start position:0%
only be be joined if it isn't full uh
 

00:02:17.599 --> 00:02:21.350 align:start position:0%
only be be joined if it isn't full uh
the<00:02:17.879><c> player</c><00:02:18.239><c> has</c><00:02:18.400><c> to</c><00:02:18.560><c> pay</c><00:02:18.760><c> the</c><00:02:19.200><c> fee</c><00:02:20.200><c> and</c><00:02:21.000><c> if</c>

00:02:21.350 --> 00:02:21.360 align:start position:0%
the player has to pay the fee and if
 

00:02:21.360 --> 00:02:23.990 align:start position:0%
the player has to pay the fee and if
both<00:02:21.599><c> of</c><00:02:21.920><c> those</c><00:02:22.080><c> are</c><00:02:22.319><c> okay</c><00:02:22.599><c> we</c><00:02:22.840><c> just</c><00:02:23.080><c> save</c><00:02:23.640><c> the</c>

00:02:23.990 --> 00:02:24.000 align:start position:0%
both of those are okay we just save the
 

00:02:24.000 --> 00:02:26.710 align:start position:0%
both of those are okay we just save the
move<00:02:24.360><c> and</c><00:02:24.519><c> the</c><00:02:24.680><c> address</c><00:02:25.000><c> of</c><00:02:25.120><c> the</c><00:02:25.280><c> player</c><00:02:26.080><c> and</c>

00:02:26.710 --> 00:02:26.720 align:start position:0%
move and the address of the player and
 

00:02:26.720 --> 00:02:28.910 align:start position:0%
move and the address of the player and
yeah<00:02:26.879><c> the</c><00:02:27.000><c> move</c><00:02:27.319><c> is</c><00:02:27.720><c> just</c><00:02:27.959><c> represent</c><00:02:28.480><c> this</c><00:02:28.640><c> Z</c>

00:02:28.910 --> 00:02:28.920 align:start position:0%
yeah the move is just represent this Z
 

00:02:28.920 --> 00:02:31.550 align:start position:0%
yeah the move is just represent this Z
one<00:02:29.080><c> or</c><00:02:29.200><c> two</c><00:02:29.360><c> for</c><00:02:29.599><c> simp</c>

00:02:31.550 --> 00:02:31.560 align:start position:0%
one or two for simp
 

00:02:31.560 --> 00:02:34.589 align:start position:0%
one or two for simp
uh<00:02:32.120><c> so</c><00:02:32.519><c> this</c><00:02:33.000><c> for</c><00:02:33.239><c> a</c><00:02:33.400><c> regular</c><00:02:33.879><c> programmer</c><00:02:34.480><c> this</c>

00:02:34.589 --> 00:02:34.599 align:start position:0%
uh so this for a regular programmer this
 

00:02:34.599 --> 00:02:36.350 align:start position:0%
uh so this for a regular programmer this
would<00:02:34.800><c> seem</c><00:02:35.120><c> quite</c><00:02:35.360><c> reasonable</c><00:02:36.040><c> but</c><00:02:36.239><c> there</c>

00:02:36.350 --> 00:02:36.360 align:start position:0%
would seem quite reasonable but there
 

00:02:36.360 --> 00:02:40.390 align:start position:0%
would seem quite reasonable but there
are<00:02:36.640><c> actually</c><00:02:36.879><c> a</c><00:02:36.959><c> few</c><00:02:37.160><c> bugs</c><00:02:37.920><c> here</c><00:02:38.920><c> um</c><00:02:39.599><c> so</c><00:02:40.159><c> what</c>

00:02:40.390 --> 00:02:40.400 align:start position:0%
are actually a few bugs here um so what
 

00:02:40.400 --> 00:02:42.390 align:start position:0%
are actually a few bugs here um so what
happens<00:02:40.760><c> if</c><00:02:40.879><c> a</c><00:02:41.080><c> third</c><00:02:41.440><c> player</c><00:02:41.920><c> attempts</c><00:02:42.280><c> to</c>

00:02:42.390 --> 00:02:42.400 align:start position:0%
happens if a third player attempts to
 

00:02:42.400 --> 00:02:43.509 align:start position:0%
happens if a third player attempts to
join<00:02:42.680><c> the</c>

00:02:43.509 --> 00:02:43.519 align:start position:0%
join the
 

00:02:43.519 --> 00:02:46.949 align:start position:0%
join the
game<00:02:44.519><c> he</c><00:02:44.680><c> would</c><00:02:44.920><c> lose</c><00:02:45.280><c> all</c><00:02:45.560><c> his</c><00:02:45.879><c> ether</c><00:02:46.560><c> and</c>

00:02:46.949 --> 00:02:46.959 align:start position:0%
game he would lose all his ether and
 

00:02:46.959 --> 00:02:48.830 align:start position:0%
game he would lose all his ether and
there's<00:02:47.239><c> no</c><00:02:47.440><c> way</c><00:02:47.599><c> to</c><00:02:47.800><c> retrieve</c>

00:02:48.830 --> 00:02:48.840 align:start position:0%
there's no way to retrieve
 

00:02:48.840 --> 00:02:51.430 align:start position:0%
there's no way to retrieve
it<00:02:49.840><c> so</c><00:02:50.040><c> let's</c><00:02:50.239><c> fix</c>

00:02:51.430 --> 00:02:51.440 align:start position:0%
it so let's fix
 

00:02:51.440 --> 00:02:55.949 align:start position:0%
it so let's fix
this<00:02:52.440><c> um</c><00:02:53.400><c> this</c><00:02:53.519><c> is</c><00:02:53.959><c> better</c><00:02:54.959><c> but</c><00:02:55.239><c> there</c><00:02:55.360><c> is</c><00:02:55.720><c> one</c>

00:02:55.949 --> 00:02:55.959 align:start position:0%
this um this is better but there is one
 

00:02:55.959 --> 00:02:57.270 align:start position:0%
this um this is better but there is one
problem

00:02:57.270 --> 00:02:57.280 align:start position:0%
problem
 

00:02:57.280 --> 00:02:59.990 align:start position:0%
problem
left<00:02:58.280><c> uh</c><00:02:58.480><c> since</c><00:02:58.760><c> the</c><00:02:58.879><c> blockchain</c><00:02:59.400><c> is</c><00:02:59.560><c> trans</c>

00:02:59.990 --> 00:03:00.000 align:start position:0%
left uh since the blockchain is trans
 

00:03:00.000 --> 00:03:02.550 align:start position:0%
left uh since the blockchain is trans
arent<00:03:00.360><c> the</c><00:03:00.480><c> first</c><00:03:00.760><c> player</c><00:03:01.360><c> will</c><00:03:01.800><c> reveal</c><00:03:02.400><c> his</c>

00:03:02.550 --> 00:03:02.560 align:start position:0%
arent the first player will reveal his
 

00:03:02.560 --> 00:03:04.470 align:start position:0%
arent the first player will reveal his
move<00:03:03.120><c> to</c><00:03:03.400><c> the</c><00:03:03.560><c> second</c>

00:03:04.470 --> 00:03:04.480 align:start position:0%
move to the second
 

00:03:04.480 --> 00:03:07.470 align:start position:0%
move to the second
player<00:03:05.480><c> we'll</c><00:03:05.720><c> not</c><00:03:05.879><c> solve</c><00:03:06.159><c> this</c><00:03:06.360><c> now</c><00:03:06.720><c> but</c><00:03:07.319><c> keep</c>

00:03:07.470 --> 00:03:07.480 align:start position:0%
player we'll not solve this now but keep
 

00:03:07.480 --> 00:03:11.710 align:start position:0%
player we'll not solve this now but keep
it<00:03:07.560><c> in</c><00:03:07.680><c> mind</c><00:03:08.440><c> later</c><00:03:09.440><c> so</c><00:03:09.760><c> just</c><00:03:09.920><c> a</c><00:03:10.360><c> quick</c><00:03:10.959><c> recap</c>

00:03:11.710 --> 00:03:11.720 align:start position:0%
it in mind later so just a quick recap
 

00:03:11.720 --> 00:03:14.350 align:start position:0%
it in mind later so just a quick recap
there's<00:03:12.440><c> two</c><00:03:13.360><c> uh</c><00:03:13.480><c> classes</c><00:03:13.799><c> of</c><00:03:13.920><c> error</c><00:03:14.239><c> that</c>

00:03:14.350 --> 00:03:14.360 align:start position:0%
there's two uh classes of error that
 

00:03:14.360 --> 00:03:16.789 align:start position:0%
there's two uh classes of error that
we're<00:03:14.599><c> focusing</c><00:03:15.080><c> on</c><00:03:15.560><c> that's</c><00:03:15.840><c> very</c><00:03:16.080><c> common</c><00:03:16.440><c> for</c>

00:03:16.789 --> 00:03:16.799 align:start position:0%
we're focusing on that's very common for
 

00:03:16.799 --> 00:03:18.910 align:start position:0%
we're focusing on that's very common for
developers<00:03:17.440><c> that's</c><00:03:17.640><c> getting</c><00:03:17.920><c> into</c><00:03:18.480><c> smart</c>

00:03:18.910 --> 00:03:18.920 align:start position:0%
developers that's getting into smart
 

00:03:18.920 --> 00:03:20.309 align:start position:0%
developers that's getting into smart
contract

00:03:20.309 --> 00:03:20.319 align:start position:0%
contract
 

00:03:20.319 --> 00:03:22.550 align:start position:0%
contract
development<00:03:21.319><c> uh</c><00:03:21.519><c> what</c><00:03:21.760><c> we</c><00:03:22.000><c> what</c><00:03:22.120><c> we're</c><00:03:22.360><c> trying</c>

00:03:22.550 --> 00:03:22.560 align:start position:0%
development uh what we what we're trying
 

00:03:22.560 --> 00:03:24.910 align:start position:0%
development uh what we what we're trying
to<00:03:22.760><c> do</c><00:03:23.200><c> is</c><00:03:23.400><c> to</c><00:03:23.560><c> use</c><00:03:23.879><c> an</c><00:03:24.080><c> expressive</c><00:03:24.599><c> type</c>

00:03:24.910 --> 00:03:24.920 align:start position:0%
to do is to use an expressive type
 

00:03:24.920 --> 00:03:28.190 align:start position:0%
to do is to use an expressive type
system<00:03:25.480><c> to</c><00:03:25.680><c> help</c><00:03:26.000><c> identify</c><00:03:26.599><c> and</c><00:03:26.760><c> solve</c>

00:03:28.190 --> 00:03:28.200 align:start position:0%
system to help identify and solve
 

00:03:28.200 --> 00:03:31.630 align:start position:0%
system to help identify and solve
this<00:03:29.200><c> and</c><00:03:29.519><c> to</c><00:03:29.760><c> to</c><00:03:29.879><c> do</c><00:03:30.080><c> this</c><00:03:30.519><c> we</c><00:03:30.720><c> are</c><00:03:31.040><c> including</c>

00:03:31.630 --> 00:03:31.640 align:start position:0%
this and to to do this we are including
 

00:03:31.640 --> 00:03:34.270 align:start position:0%
this and to to do this we are including
both<00:03:31.920><c> ether</c><00:03:32.319><c> flow</c><00:03:33.000><c> and</c><00:03:33.599><c> cryptography</c>

00:03:34.270 --> 00:03:34.280 align:start position:0%
both ether flow and cryptography
 

00:03:34.280 --> 00:03:37.309 align:start position:0%
both ether flow and cryptography
directly<00:03:34.640><c> in</c><00:03:34.760><c> the</c><00:03:34.879><c> type</c>

00:03:37.309 --> 00:03:37.319 align:start position:0%
 
 

00:03:37.319 --> 00:03:40.149 align:start position:0%
 
system<00:03:38.319><c> so</c><00:03:38.680><c> if</c><00:03:38.760><c> we</c><00:03:38.920><c> want</c><00:03:39.080><c> to</c><00:03:39.319><c> encode</c><00:03:39.760><c> ether</c>

00:03:40.149 --> 00:03:40.159 align:start position:0%
system so if we want to encode ether
 

00:03:40.159 --> 00:03:43.550 align:start position:0%
system so if we want to encode ether
flow<00:03:40.560><c> in</c><00:03:40.720><c> the</c><00:03:40.879><c> type</c><00:03:41.159><c> system</c><00:03:41.879><c> what</c><00:03:42.200><c> can</c><00:03:42.360><c> we</c><00:03:42.560><c> do</c>

00:03:43.550 --> 00:03:43.560 align:start position:0%
flow in the type system what can we do
 

00:03:43.560 --> 00:03:45.750 align:start position:0%
flow in the type system what can we do
well<00:03:43.799><c> we</c><00:03:43.920><c> can</c><00:03:44.159><c> start</c><00:03:44.680><c> with</c><00:03:44.959><c> including</c><00:03:45.439><c> the</c>

00:03:45.750 --> 00:03:45.760 align:start position:0%
well we can start with including the
 

00:03:45.760 --> 00:03:48.070 align:start position:0%
well we can start with including the
transaction<00:03:46.360><c> value</c><00:03:46.959><c> in</c><00:03:47.159><c> the</c><00:03:47.319><c> type</c><00:03:47.560><c> signature</c>

00:03:48.070 --> 00:03:48.080 align:start position:0%
transaction value in the type signature
 

00:03:48.080 --> 00:03:48.830 align:start position:0%
transaction value in the type signature
like

00:03:48.830 --> 00:03:48.840 align:start position:0%
like
 

00:03:48.840 --> 00:03:52.270 align:start position:0%
like
this<00:03:49.840><c> and</c><00:03:50.319><c> as</c><00:03:50.439><c> you</c><00:03:50.560><c> can</c><00:03:50.720><c> see</c><00:03:51.159><c> we</c><00:03:51.799><c> we</c><00:03:51.920><c> have</c><00:03:52.079><c> also</c>

00:03:52.270 --> 00:03:52.280 align:start position:0%
this and as you can see we we have also
 

00:03:52.280 --> 00:03:54.750 align:start position:0%
this and as you can see we we have also
put<00:03:52.439><c> a</c><00:03:52.599><c> precondition</c><00:03:53.319><c> on</c><00:03:53.439><c> the</c><00:03:53.599><c> value</c><00:03:54.360><c> saying</c>

00:03:54.750 --> 00:03:54.760 align:start position:0%
put a precondition on the value saying
 

00:03:54.760 --> 00:03:57.789 align:start position:0%
put a precondition on the value saying
that<00:03:54.959><c> this</c><00:03:55.360><c> function</c><00:03:56.360><c> requires</c><00:03:56.840><c> at</c><00:03:57.000><c> least</c><00:03:57.519><c> 10</c>

00:03:57.789 --> 00:03:57.799 align:start position:0%
that this function requires at least 10
 

00:03:57.799 --> 00:04:00.750 align:start position:0%
that this function requires at least 10
ethers<00:03:58.640><c> to</c><00:03:59.040><c> be</c><00:03:59.239><c> executed</c>

00:04:00.750 --> 00:04:00.760 align:start position:0%
ethers to be executed
 

00:04:00.760 --> 00:04:02.470 align:start position:0%
ethers to be executed
uh<00:04:00.920><c> otherwise</c><00:04:01.360><c> the</c><00:04:01.519><c> transaction</c><00:04:02.079><c> is</c>

00:04:02.470 --> 00:04:02.480 align:start position:0%
uh otherwise the transaction is
 

00:04:02.480 --> 00:04:04.630 align:start position:0%
uh otherwise the transaction is
considered<00:04:02.959><c> invalid</c><00:04:03.400><c> for</c><00:04:03.599><c> our</c><00:04:03.879><c> purposes</c><00:04:04.439><c> and</c>

00:04:04.630 --> 00:04:04.640 align:start position:0%
considered invalid for our purposes and
 

00:04:04.640 --> 00:04:07.390 align:start position:0%
considered invalid for our purposes and
all<00:04:04.879><c> ether</c><00:04:05.319><c> is</c><00:04:05.760><c> automat</c><00:04:06.400><c> automatically</c>

00:04:07.390 --> 00:04:07.400 align:start position:0%
all ether is automat automatically
 

00:04:07.400 --> 00:04:08.750 align:start position:0%
all ether is automat automatically
returned<00:04:07.640><c> to</c><00:04:07.760><c> the</c>

00:04:08.750 --> 00:04:08.760 align:start position:0%
returned to the
 

00:04:08.760 --> 00:04:11.429 align:start position:0%
returned to the
sender<00:04:09.760><c> and</c><00:04:09.959><c> this</c><00:04:10.079><c> is</c><00:04:10.239><c> certainly</c><00:04:10.720><c> neat</c><00:04:11.079><c> but</c><00:04:11.239><c> it</c>

00:04:11.429 --> 00:04:11.439 align:start position:0%
sender and this is certainly neat but it
 

00:04:11.439 --> 00:04:15.349 align:start position:0%
sender and this is certainly neat but it
doesn't<00:04:11.760><c> solve</c><00:04:12.159><c> our</c><00:04:12.519><c> problem</c><00:04:12.959><c> our</c><00:04:13.280><c> problem</c>

00:04:15.349 --> 00:04:15.359 align:start position:0%
doesn't solve our problem our problem
 

00:04:15.359 --> 00:04:17.629 align:start position:0%
doesn't solve our problem our problem
problems<00:04:16.359><c> uh</c><00:04:16.600><c> but</c><00:04:16.759><c> as</c><00:04:16.919><c> you</c><00:04:17.040><c> can</c><00:04:17.160><c> see</c><00:04:17.440><c> we</c>

00:04:17.629 --> 00:04:17.639 align:start position:0%
problems uh but as you can see we
 

00:04:17.639 --> 00:04:20.870 align:start position:0%
problems uh but as you can see we
actually<00:04:18.199><c> already</c><00:04:18.880><c> know</c><00:04:19.880><c> uh</c><00:04:20.239><c> the</c><00:04:20.359><c> functions</c>

00:04:20.870 --> 00:04:20.880 align:start position:0%
actually already know uh the functions
 

00:04:20.880 --> 00:04:25.830 align:start position:0%
actually already know uh the functions
result<00:04:22.199><c> success</c><00:04:23.199><c> and</c><00:04:23.680><c> the</c><00:04:23.919><c> transaction</c><00:04:24.440><c> value</c>

00:04:25.830 --> 00:04:25.840 align:start position:0%
result success and the transaction value
 

00:04:25.840 --> 00:04:27.870 align:start position:0%
result success and the transaction value
value<00:04:26.840><c> this</c><00:04:26.960><c> is</c><00:04:27.199><c> actually</c><00:04:27.600><c> enough</c>

00:04:27.870 --> 00:04:27.880 align:start position:0%
value this is actually enough
 

00:04:27.880 --> 00:04:30.189 align:start position:0%
value this is actually enough
information<00:04:28.400><c> for</c><00:04:28.600><c> us</c><00:04:28.960><c> to</c><00:04:29.320><c> specify</c><00:04:29.680><c> spe</c><00:04:29.840><c> ify</c>

00:04:30.189 --> 00:04:30.199 align:start position:0%
information for us to specify spe ify
 

00:04:30.199 --> 00:04:32.029 align:start position:0%
information for us to specify spe ify
how<00:04:30.400><c> the</c><00:04:30.560><c> function</c><00:04:31.160><c> should</c><00:04:31.479><c> should</c><00:04:31.720><c> handle</c>

00:04:32.029 --> 00:04:32.039 align:start position:0%
how the function should should handle
 

00:04:32.039 --> 00:04:35.150 align:start position:0%
how the function should should handle
ether<00:04:32.400><c> in</c><00:04:32.560><c> all</c><00:04:32.880><c> execution</c>

00:04:35.150 --> 00:04:35.160 align:start position:0%
ether in all execution
 

00:04:35.160 --> 00:04:38.150 align:start position:0%
ether in all execution
pths<00:04:36.160><c> so</c><00:04:36.479><c> we</c><00:04:36.680><c> just</c><00:04:36.919><c> take</c><00:04:37.199><c> the</c><00:04:37.520><c> return</c><00:04:37.800><c> value</c>

00:04:38.150 --> 00:04:38.160 align:start position:0%
pths so we just take the return value
 

00:04:38.160 --> 00:04:40.189 align:start position:0%
pths so we just take the return value
and<00:04:38.280><c> do</c><00:04:38.479><c> a</c><00:04:38.840><c> conditional</c><00:04:39.160><c> check</c><00:04:39.400><c> on</c><00:04:39.560><c> it</c><00:04:39.919><c> that's</c>

00:04:40.189 --> 00:04:40.199 align:start position:0%
and do a conditional check on it that's
 

00:04:40.199 --> 00:04:42.830 align:start position:0%
and do a conditional check on it that's
the<00:04:40.639><c> question</c><00:04:40.919><c> mark</c><00:04:41.160><c> and</c><00:04:41.360><c> colon</c><00:04:41.800><c> there</c><00:04:42.440><c> as</c><00:04:42.560><c> you</c>

00:04:42.830 --> 00:04:42.840 align:start position:0%
the question mark and colon there as you
 

00:04:42.840 --> 00:04:44.590 align:start position:0%
the question mark and colon there as you
probably<00:04:43.360><c> recognize</c><00:04:43.880><c> from</c><00:04:44.080><c> imperative</c>

00:04:44.590 --> 00:04:44.600 align:start position:0%
probably recognize from imperative
 

00:04:44.600 --> 00:04:46.629 align:start position:0%
probably recognize from imperative
language

00:04:46.629 --> 00:04:46.639 align:start position:0%
language
 

00:04:46.639 --> 00:04:49.189 align:start position:0%
language
languages<00:04:47.639><c> uh</c><00:04:47.880><c> if</c><00:04:48.000><c> the</c><00:04:48.160><c> player</c><00:04:48.479><c> was</c><00:04:48.759><c> able</c><00:04:49.039><c> to</c>

00:04:49.189 --> 00:04:49.199 align:start position:0%
languages uh if the player was able to
 

00:04:49.199 --> 00:04:51.469 align:start position:0%
languages uh if the player was able to
join<00:04:49.400><c> the</c><00:04:49.600><c> game</c><00:04:50.240><c> we</c><00:04:50.360><c> should</c><00:04:50.759><c> say</c><00:04:51.120><c> we</c><00:04:51.199><c> should</c>

00:04:51.469 --> 00:04:51.479 align:start position:0%
join the game we should say we should
 

00:04:51.479 --> 00:04:54.390 align:start position:0%
join the game we should say we should
save<00:04:51.960><c> 10</c><00:04:52.280><c> ether</c><00:04:52.600><c> and</c><00:04:52.919><c> return</c><00:04:53.120><c> the</c><00:04:53.880><c> return</c><00:04:54.120><c> the</c>

00:04:54.390 --> 00:04:54.400 align:start position:0%
save 10 ether and return the return the
 

00:04:54.400 --> 00:04:56.749 align:start position:0%
save 10 ether and return the return the
rest<00:04:55.360><c> and</c><00:04:55.520><c> if</c><00:04:55.639><c> the</c><00:04:55.759><c> player</c><00:04:56.039><c> wasn't</c><00:04:56.360><c> able</c><00:04:56.600><c> to</c>

00:04:56.749 --> 00:04:56.759 align:start position:0%
rest and if the player wasn't able to
 

00:04:56.759 --> 00:04:58.909 align:start position:0%
rest and if the player wasn't able to
join<00:04:57.039><c> the</c><00:04:57.160><c> game</c><00:04:57.880><c> then</c><00:04:58.000><c> we</c><00:04:58.120><c> should</c><00:04:58.360><c> send</c><00:04:58.639><c> back</c>

00:04:58.909 --> 00:04:58.919 align:start position:0%
join the game then we should send back
 

00:04:58.919 --> 00:05:01.469 align:start position:0%
join the game then we should send back
everything<00:04:59.400><c> and</c><00:04:59.720><c> don't</c><00:04:59.880><c> save</c>

00:05:01.469 --> 00:05:01.479 align:start position:0%
everything and don't save
 

00:05:01.479 --> 00:05:04.310 align:start position:0%
everything and don't save
anything<00:05:02.479><c> now</c><00:05:02.880><c> this</c><00:05:03.160><c> type</c><00:05:03.560><c> signature</c>

00:05:04.310 --> 00:05:04.320 align:start position:0%
anything now this type signature
 

00:05:04.320 --> 00:05:05.990 align:start position:0%
anything now this type signature
actually<00:05:04.720><c> causes</c><00:05:05.199><c> the</c><00:05:05.400><c> problematic</c>

00:05:05.990 --> 00:05:06.000 align:start position:0%
actually causes the problematic
 

00:05:06.000 --> 00:05:08.189 align:start position:0%
actually causes the problematic
implementation<00:05:06.800><c> from</c><00:05:07.000><c> before</c><00:05:07.400><c> to</c><00:05:07.600><c> be</c><00:05:07.759><c> a</c><00:05:07.919><c> type</c>

00:05:08.189 --> 00:05:08.199 align:start position:0%
implementation from before to be a type
 

00:05:08.199 --> 00:05:11.390 align:start position:0%
implementation from before to be a type
error<00:05:08.639><c> that's</c><00:05:08.880><c> catched</c><00:05:09.320><c> at</c><00:05:09.560><c> compile</c><00:05:10.400><c> time</c>

00:05:11.390 --> 00:05:11.400 align:start position:0%
error that's catched at compile time
 

00:05:11.400 --> 00:05:14.590 align:start position:0%
error that's catched at compile time
this<00:05:11.600><c> is</c><00:05:12.440><c> quite</c><00:05:12.720><c> amazing</c><00:05:13.320><c> because</c><00:05:13.759><c> it</c><00:05:14.199><c> allows</c>

00:05:14.590 --> 00:05:14.600 align:start position:0%
this is quite amazing because it allows
 

00:05:14.600 --> 00:05:15.430 align:start position:0%
this is quite amazing because it allows
us

00:05:15.430 --> 00:05:15.440 align:start position:0%
us
 

00:05:15.440 --> 00:05:18.830 align:start position:0%
us
to<00:05:16.440><c> uh</c><00:05:16.720><c> eliminate</c><00:05:17.160><c> a</c><00:05:17.320><c> large</c><00:05:17.600><c> class</c><00:05:17.840><c> of</c><00:05:18.000><c> bugs</c>

00:05:18.830 --> 00:05:18.840 align:start position:0%
to uh eliminate a large class of bugs
 

00:05:18.840 --> 00:05:21.670 align:start position:0%
to uh eliminate a large class of bugs
without<00:05:19.199><c> doing</c><00:05:19.880><c> any</c><00:05:20.160><c> testing</c><00:05:20.639><c> or</c><00:05:20.840><c> formal</c><00:05:21.280><c> ver</c>

00:05:21.670 --> 00:05:21.680 align:start position:0%
without doing any testing or formal ver
 

00:05:21.680 --> 00:05:25.150 align:start position:0%
without doing any testing or formal ver
formal<00:05:22.080><c> verification</c>

00:05:25.150 --> 00:05:25.160 align:start position:0%
 
 

00:05:25.160 --> 00:05:27.430 align:start position:0%
 
whatsoever<00:05:26.160><c> this</c><00:05:26.360><c> technique</c><00:05:26.800><c> can</c><00:05:27.039><c> actually</c>

00:05:27.430 --> 00:05:27.440 align:start position:0%
whatsoever this technique can actually
 

00:05:27.440 --> 00:05:31.150 align:start position:0%
whatsoever this technique can actually
also<00:05:27.720><c> be</c><00:05:27.880><c> used</c><00:05:28.479><c> for</c><00:05:29.280><c> by</c><00:05:29.759><c> contract</c><00:05:30.160><c> developers</c>

00:05:31.150 --> 00:05:31.160 align:start position:0%
also be used for by contract developers
 

00:05:31.160 --> 00:05:33.270 align:start position:0%
also be used for by contract developers
uh<00:05:31.280><c> to</c><00:05:31.600><c> specify</c><00:05:32.039><c> the</c><00:05:32.240><c> behaviors</c><00:05:32.880><c> of</c><00:05:33.080><c> their</c>

00:05:33.270 --> 00:05:33.280 align:start position:0%
uh to specify the behaviors of their
 

00:05:33.280 --> 00:05:35.510 align:start position:0%
uh to specify the behaviors of their
contracts<00:05:34.240><c> but</c><00:05:34.560><c> that</c><00:05:34.759><c> requires</c><00:05:35.199><c> a</c><00:05:35.280><c> little</c>

00:05:35.510 --> 00:05:35.520 align:start position:0%
contracts but that requires a little
 

00:05:35.520 --> 00:05:37.909 align:start position:0%
contracts but that requires a little
more<00:05:36.080><c> a</c><00:05:36.199><c> little</c><00:05:36.400><c> more</c><00:05:36.720><c> work</c><00:05:37.120><c> on</c><00:05:37.319><c> the</c><00:05:37.479><c> part</c><00:05:37.759><c> of</c>

00:05:37.909 --> 00:05:37.919 align:start position:0%
more a little more work on the part of
 

00:05:37.919 --> 00:05:40.950 align:start position:0%
more a little more work on the part of
the<00:05:38.080><c> developer</c><00:05:38.600><c> so</c><00:05:38.800><c> we</c><00:05:38.919><c> won't</c><00:05:39.280><c> go</c><00:05:39.440><c> into</c>

00:05:40.950 --> 00:05:40.960 align:start position:0%
the developer so we won't go into
 

00:05:40.960 --> 00:05:43.590 align:start position:0%
the developer so we won't go into
this<00:05:41.960><c> uh</c><00:05:42.199><c> but</c><00:05:42.360><c> we</c><00:05:42.479><c> still</c><00:05:42.720><c> have</c><00:05:42.840><c> the</c><00:05:43.039><c> problem</c>

00:05:43.590 --> 00:05:43.600 align:start position:0%
this uh but we still have the problem
 

00:05:43.600 --> 00:05:46.110 align:start position:0%
this uh but we still have the problem
that<00:05:44.080><c> uh</c><00:05:44.199><c> the</c><00:05:44.360><c> move</c><00:05:44.800><c> is</c><00:05:45.280><c> disclosed</c><00:05:45.880><c> when</c><00:05:46.039><c> it</c>

00:05:46.110 --> 00:05:46.120 align:start position:0%
that uh the move is disclosed when it
 

00:05:46.120 --> 00:05:47.150 align:start position:0%
that uh the move is disclosed when it
shouldn't

00:05:47.150 --> 00:05:47.160 align:start position:0%
shouldn't
 

00:05:47.160 --> 00:05:49.909 align:start position:0%
shouldn't
be<00:05:48.160><c> the</c><00:05:48.319><c> way</c><00:05:48.479><c> to</c><00:05:48.639><c> solve</c><00:05:49.000><c> this</c><00:05:49.319><c> is</c><00:05:49.440><c> to</c><00:05:49.600><c> use</c>

00:05:49.909 --> 00:05:49.919 align:start position:0%
be the way to solve this is to use
 

00:05:49.919 --> 00:05:52.629 align:start position:0%
be the way to solve this is to use
cryptographic<00:05:50.840><c> commitments</c><00:05:51.840><c> they</c><00:05:52.039><c> basically</c>

00:05:52.629 --> 00:05:52.639 align:start position:0%
cryptographic commitments they basically
 

00:05:52.639 --> 00:05:55.270 align:start position:0%
cryptographic commitments they basically
allow<00:05:52.960><c> you</c><00:05:53.160><c> to</c><00:05:53.680><c> commit</c><00:05:53.960><c> to</c><00:05:54.120><c> a</c><00:05:54.319><c> value</c><00:05:54.840><c> and</c><00:05:55.039><c> then</c>

00:05:55.270 --> 00:05:55.280 align:start position:0%
allow you to commit to a value and then
 

00:05:55.280 --> 00:05:57.950 align:start position:0%
allow you to commit to a value and then
reveal<00:05:55.680><c> it</c><00:05:55.880><c> at</c><00:05:55.960><c> a</c><00:05:56.080><c> later</c>

00:05:57.950 --> 00:05:57.960 align:start position:0%
reveal it at a later
 

00:05:57.960 --> 00:06:00.670 align:start position:0%
reveal it at a later
time<00:05:58.960><c> but</c><00:05:59.120><c> Developers</c><00:05:59.759><c> shouldn't</c><00:06:00.199><c> Implement</c>

00:06:00.670 --> 00:06:00.680 align:start position:0%
time but Developers shouldn't Implement
 

00:06:00.680 --> 00:06:02.590 align:start position:0%
time but Developers shouldn't Implement
their<00:06:00.840><c> own</c><00:06:01.160><c> crypto</c><00:06:01.720><c> each</c><00:06:01.880><c> and</c><00:06:02.039><c> every</c><00:06:02.319><c> time</c>

00:06:02.590 --> 00:06:02.600 align:start position:0%
their own crypto each and every time
 

00:06:02.600 --> 00:06:06.029 align:start position:0%
their own crypto each and every time
it's<00:06:02.960><c> tedious</c><00:06:03.600><c> and</c><00:06:03.960><c> very</c><00:06:04.240><c> error</c>

00:06:06.029 --> 00:06:06.039 align:start position:0%
it's tedious and very error
 

00:06:06.039 --> 00:06:10.629 align:start position:0%
it's tedious and very error
prone<00:06:07.400><c> so</c><00:06:08.400><c> the</c><00:06:08.560><c> way</c><00:06:08.720><c> we</c><00:06:08.880><c> solve</c><00:06:09.319><c> this</c><00:06:10.240><c> is</c><00:06:10.440><c> by</c>

00:06:10.629 --> 00:06:10.639 align:start position:0%
prone so the way we solve this is by
 

00:06:10.639 --> 00:06:13.589 align:start position:0%
prone so the way we solve this is by
annotating<00:06:11.280><c> the</c><00:06:11.520><c> types</c><00:06:11.880><c> of</c><00:06:12.039><c> secret</c><00:06:12.479><c> values</c><00:06:13.479><c> as</c>

00:06:13.589 --> 00:06:13.599 align:start position:0%
annotating the types of secret values as
 

00:06:13.599 --> 00:06:17.230 align:start position:0%
annotating the types of secret values as
you<00:06:13.720><c> can</c><00:06:13.880><c> see</c><00:06:14.199><c> there</c><00:06:15.080><c> with</c>

00:06:17.230 --> 00:06:17.240 align:start position:0%
you can see there with
 

00:06:17.240 --> 00:06:20.670 align:start position:0%
you can see there with
commit<00:06:18.240><c> um</c><00:06:18.880><c> this</c><00:06:19.080><c> indicates</c><00:06:19.560><c> to</c><00:06:19.720><c> the</c><00:06:19.880><c> compiler</c>

00:06:20.670 --> 00:06:20.680 align:start position:0%
commit um this indicates to the compiler
 

00:06:20.680 --> 00:06:23.990 align:start position:0%
commit um this indicates to the compiler
that<00:06:21.280><c> this</c><00:06:21.520><c> value</c><00:06:22.039><c> should</c><00:06:22.319><c> be</c><00:06:22.440><c> treated</c><00:06:22.840><c> as</c><00:06:22.960><c> a</c>

00:06:23.990 --> 00:06:24.000 align:start position:0%
that this value should be treated as a
 

00:06:24.000 --> 00:06:26.350 align:start position:0%
that this value should be treated as a
commitment<00:06:25.000><c> and</c><00:06:25.479><c> the</c><00:06:25.639><c> compiler</c><00:06:26.120><c> will</c>

00:06:26.350 --> 00:06:26.360 align:start position:0%
commitment and the compiler will
 

00:06:26.360 --> 00:06:28.710 align:start position:0%
commitment and the compiler will
automatically<00:06:27.039><c> generate</c><00:06:27.440><c> a</c><00:06:27.639><c> function</c><00:06:28.520><c> for</c>

00:06:28.710 --> 00:06:28.720 align:start position:0%
automatically generate a function for
 

00:06:28.720 --> 00:06:32.270 align:start position:0%
automatically generate a function for
the<00:06:28.840><c> sender</c><00:06:29.199><c> to</c><00:06:29.319><c> review</c><00:06:29.759><c> it</c><00:06:29.840><c> at</c><00:06:29.919><c> a</c><00:06:30.280><c> at</c><00:06:30.360><c> a</c><00:06:30.599><c> later</c>

00:06:32.270 --> 00:06:32.280 align:start position:0%
the sender to review it at a at a later
 

00:06:32.280 --> 00:06:35.110 align:start position:0%
the sender to review it at a at a later
time<00:06:33.280><c> when</c><00:06:33.440><c> it</c><00:06:33.599><c> has</c><00:06:33.759><c> been</c><00:06:33.960><c> revealed</c><00:06:34.680><c> it</c><00:06:34.800><c> can</c><00:06:34.960><c> be</c>

00:06:35.110 --> 00:06:35.120 align:start position:0%
time when it has been revealed it can be
 

00:06:35.120 --> 00:06:37.150 align:start position:0%
time when it has been revealed it can be
accessed<00:06:35.520><c> in</c><00:06:35.800><c> Code</c><00:06:36.199><c> by</c><00:06:36.360><c> using</c><00:06:36.680><c> the</c><00:06:36.800><c> standard</c>

00:06:37.150 --> 00:06:37.160 align:start position:0%
accessed in Code by using the standard
 

00:06:37.160 --> 00:06:39.909 align:start position:0%
accessed in Code by using the standard
Library<00:06:37.800><c> open</c><00:06:38.319><c> function</c><00:06:38.919><c> which</c><00:06:39.319><c> takes</c><00:06:39.639><c> any</c>

00:06:39.909 --> 00:06:39.919 align:start position:0%
Library open function which takes any
 

00:06:39.919 --> 00:06:42.430 align:start position:0%
Library open function which takes any
commitment<00:06:40.560><c> and</c><00:06:40.919><c> Returns</c><00:06:41.400><c> the</c><00:06:41.880><c> and</c><00:06:42.199><c> Returns</c>

00:06:42.430 --> 00:06:42.440 align:start position:0%
commitment and Returns the and Returns
 

00:06:42.440 --> 00:06:46.350 align:start position:0%
commitment and Returns the and Returns
the<00:06:43.039><c> value</c><00:06:44.039><c> if</c><00:06:44.240><c> it</c><00:06:44.680><c> hadn't</c><00:06:45.039><c> been</c><00:06:45.560><c> revealed</c>

00:06:46.350 --> 00:06:46.360 align:start position:0%
the value if it hadn't been revealed
 

00:06:46.360 --> 00:06:48.189 align:start position:0%
the value if it hadn't been revealed
previous<00:06:46.759><c> to</c><00:06:46.960><c> calling</c>

00:06:48.189 --> 00:06:48.199 align:start position:0%
previous to calling
 

00:06:48.199 --> 00:06:52.230 align:start position:0%
previous to calling
open<00:06:49.199><c> uh</c><00:06:49.440><c> then</c><00:06:49.639><c> open</c><00:06:50.039><c> will</c><00:06:50.280><c> fail</c><00:06:51.280><c> return</c><00:06:51.599><c> all</c><00:06:51.919><c> e</c>

00:06:52.230 --> 00:06:52.240 align:start position:0%
open uh then open will fail return all e
 

00:06:52.240 --> 00:06:56.710 align:start position:0%
open uh then open will fail return all e
to<00:06:52.360><c> the</c><00:06:52.520><c> sender</c><00:06:53.080><c> and</c><00:06:53.280><c> abort</c>

00:06:56.710 --> 00:06:56.720 align:start position:0%
 
 

00:06:56.720 --> 00:06:59.589 align:start position:0%
 
execution<00:06:57.720><c> uh</c><00:06:57.919><c> so</c><00:06:58.240><c> our</c><00:06:58.479><c> final</c><00:06:58.879><c> type</c><00:06:59.160><c> correct</c>

00:06:59.589 --> 00:06:59.599 align:start position:0%
execution uh so our final type correct
 

00:06:59.599 --> 00:07:02.469 align:start position:0%
execution uh so our final type correct
implementation<00:07:00.160><c> would</c><00:07:00.319><c> look</c><00:07:00.599><c> like</c><00:07:00.960><c> this</c><00:07:01.960><c> note</c>

00:07:02.469 --> 00:07:02.479 align:start position:0%
implementation would look like this note
 

00:07:02.479 --> 00:07:06.029 align:start position:0%
implementation would look like this note
that<00:07:02.879><c> we</c><00:07:03.039><c> are</c><00:07:03.360><c> forced</c><00:07:03.759><c> to</c><00:07:04.080><c> explicitly</c><00:07:05.039><c> save</c>

00:07:06.029 --> 00:07:06.039 align:start position:0%
that we are forced to explicitly save
 

00:07:06.039 --> 00:07:09.029 align:start position:0%
that we are forced to explicitly save
all<00:07:06.360><c> ether</c><00:07:06.800><c> that</c><00:07:06.919><c> we</c><00:07:07.039><c> want</c><00:07:07.199><c> to</c><00:07:07.400><c> keep</c><00:07:08.400><c> because</c>

00:07:09.029 --> 00:07:09.039 align:start position:0%
all ether that we want to keep because
 

00:07:09.039 --> 00:07:11.670 align:start position:0%
all ether that we want to keep because
otherwise<00:07:09.440><c> it</c><00:07:09.639><c> was</c><00:07:10.000><c> wouldn't</c>

00:07:11.670 --> 00:07:11.680 align:start position:0%
otherwise it was wouldn't
 

00:07:11.680 --> 00:07:15.110 align:start position:0%
otherwise it was wouldn't
compile<00:07:12.680><c> and</c><00:07:13.160><c> now</c><00:07:13.479><c> Robert</c><00:07:13.919><c> will</c><00:07:14.560><c> talk</c><00:07:14.840><c> about</c>

00:07:15.110 --> 00:07:15.120 align:start position:0%
compile and now Robert will talk about
 

00:07:15.120 --> 00:07:17.230 align:start position:0%
compile and now Robert will talk about
how<00:07:15.319><c> we</c><00:07:15.720><c> intend</c><00:07:16.039><c> to</c><00:07:16.199><c> implement</c>

00:07:17.230 --> 00:07:17.240 align:start position:0%
how we intend to implement
 

00:07:17.240 --> 00:07:21.189 align:start position:0%
how we intend to implement
this<00:07:18.240><c> thank</c><00:07:18.440><c> you</c><00:07:19.360><c> so</c><00:07:20.319><c> some</c><00:07:20.560><c> of</c><00:07:20.680><c> you</c><00:07:20.840><c> might</c><00:07:21.039><c> have</c>

00:07:21.189 --> 00:07:21.199 align:start position:0%
this thank you so some of you might have
 

00:07:21.199 --> 00:07:23.749 align:start position:0%
this thank you so some of you might have
noticed<00:07:21.680><c> that</c><00:07:21.960><c> the</c><00:07:22.319><c> syntax</c><00:07:22.879><c> we</c><00:07:23.000><c> have</c><00:07:23.160><c> used</c><00:07:23.560><c> is</c>

00:07:23.749 --> 00:07:23.759 align:start position:0%
noticed that the syntax we have used is
 

00:07:23.759 --> 00:07:26.670 align:start position:0%
noticed that the syntax we have used is
very<00:07:23.960><c> similar</c><00:07:24.319><c> to</c><00:07:24.680><c> ascal</c><00:07:25.680><c> and</c><00:07:26.160><c> when</c><00:07:26.319><c> we</c><00:07:26.440><c> first</c>

00:07:26.670 --> 00:07:26.680 align:start position:0%
very similar to ascal and when we first
 

00:07:26.680 --> 00:07:29.390 align:start position:0%
very similar to ascal and when we first
started<00:07:27.000><c> looking</c><00:07:27.240><c> at</c><00:07:27.440><c> this</c><00:07:27.960><c> we</c><00:07:28.879><c> had</c><00:07:29.039><c> the</c><00:07:29.160><c> idea</c>

00:07:29.390 --> 00:07:29.400 align:start position:0%
started looking at this we had the idea
 

00:07:29.400 --> 00:07:31.469 align:start position:0%
started looking at this we had the idea
of<00:07:29.599><c> of</c><00:07:29.759><c> making</c><00:07:30.199><c> hll</c><00:07:30.639><c> on</c><00:07:30.759><c> the</c><00:07:30.879><c> blockchain</c>

00:07:31.469 --> 00:07:31.479 align:start position:0%
of of making hll on the blockchain
 

00:07:31.479 --> 00:07:34.869 align:start position:0%
of of making hll on the blockchain
basically<00:07:32.479><c> but</c><00:07:32.800><c> the</c><00:07:32.919><c> more</c><00:07:33.160><c> we</c><00:07:33.319><c> looked</c><00:07:33.680><c> at</c><00:07:34.599><c> U</c>

00:07:34.869 --> 00:07:34.879 align:start position:0%
basically but the more we looked at U
 

00:07:34.879 --> 00:07:37.469 align:start position:0%
basically but the more we looked at U
these<00:07:35.720><c> problems</c><00:07:36.400><c> and</c><00:07:36.800><c> how</c><00:07:37.000><c> they</c><00:07:37.120><c> could</c><00:07:37.240><c> be</c>

00:07:37.469 --> 00:07:37.479 align:start position:0%
these problems and how they could be
 

00:07:37.479 --> 00:07:40.029 align:start position:0%
these problems and how they could be
solved<00:07:37.960><c> we</c><00:07:38.639><c> realized</c><00:07:39.080><c> that</c><00:07:39.240><c> dependent</c><00:07:39.720><c> types</c>

00:07:40.029 --> 00:07:40.039 align:start position:0%
solved we realized that dependent types
 

00:07:40.039 --> 00:07:44.070 align:start position:0%
solved we realized that dependent types
would<00:07:40.199><c> be</c><00:07:40.400><c> really</c><00:07:40.639><c> cool</c><00:07:41.280><c> to</c><00:07:41.479><c> do</c><00:07:41.879><c> this</c><00:07:42.879><c> uh</c><00:07:43.240><c> also</c>

00:07:44.070 --> 00:07:44.080 align:start position:0%
would be really cool to do this uh also
 

00:07:44.080 --> 00:07:46.510 align:start position:0%
would be really cool to do this uh also
haskill<00:07:44.560><c> is</c><00:07:44.680><c> lazily</c><00:07:45.120><c> evaluated</c><00:07:46.120><c> which</c>

00:07:46.510 --> 00:07:46.520 align:start position:0%
haskill is lazily evaluated which
 

00:07:46.520 --> 00:07:49.350 align:start position:0%
haskill is lazily evaluated which
becomes<00:07:46.919><c> prohibit</c><00:07:47.599><c> expensive</c><00:07:48.440><c> in</c><00:07:48.759><c> real</c><00:07:49.080><c> life</c>

00:07:49.350 --> 00:07:49.360 align:start position:0%
becomes prohibit expensive in real life
 

00:07:49.360 --> 00:07:51.830 align:start position:0%
becomes prohibit expensive in real life
on<00:07:49.479><c> the</c><00:07:49.599><c> evm</c><00:07:50.000><c> as</c><00:07:50.080><c> it</c><00:07:50.199><c> is</c><00:07:50.400><c> now</c><00:07:51.280><c> and</c><00:07:51.479><c> then</c><00:07:51.680><c> we</c>

00:07:51.830 --> 00:07:51.840 align:start position:0%
on the evm as it is now and then we
 

00:07:51.840 --> 00:07:53.189 align:start position:0%
on the evm as it is now and then we
found

00:07:53.189 --> 00:07:53.199 align:start position:0%
found
 

00:07:53.199 --> 00:07:58.189 align:start position:0%
found
Idris<00:07:54.199><c> uh</c><00:07:54.919><c> Idris</c><00:07:55.599><c> is</c><00:07:56.280><c> very</c><00:07:56.599><c> similar</c><00:07:56.919><c> to</c><00:07:57.199><c> hcll</c>

00:07:58.189 --> 00:07:58.199 align:start position:0%
Idris uh Idris is very similar to hcll
 

00:07:58.199 --> 00:08:00.270 align:start position:0%
Idris uh Idris is very similar to hcll
but<00:07:58.400><c> it</c><00:07:58.560><c> has</c><00:07:58.680><c> some</c><00:07:58.919><c> key</c><00:07:59.080><c> difference</c>

00:08:00.270 --> 00:08:00.280 align:start position:0%
but it has some key difference
 

00:08:00.280 --> 00:08:02.950 align:start position:0%
but it has some key difference
uh<00:08:00.560><c> first</c><00:08:00.759><c> of</c><00:08:01.000><c> which</c><00:08:01.560><c> it</c><00:08:01.680><c> is</c><00:08:01.879><c> dependently</c>

00:08:02.950 --> 00:08:02.960 align:start position:0%
uh first of which it is dependently
 

00:08:02.960 --> 00:08:08.070 align:start position:0%
uh first of which it is dependently
typed<00:08:03.960><c> uh</c><00:08:04.680><c> and</c><00:08:05.680><c> it</c><00:08:05.879><c> has</c><00:08:06.599><c> side</c><00:08:06.879><c> effects</c><00:08:07.639><c> is</c>

00:08:08.070 --> 00:08:08.080 align:start position:0%
typed uh and it has side effects is
 

00:08:08.080 --> 00:08:11.749 align:start position:0%
typed uh and it has side effects is
model<00:08:08.560><c> with</c><00:08:08.840><c> Al</c><00:08:09.240><c> algebraic</c><00:08:09.919><c> effects</c><00:08:10.680><c> so</c><00:08:11.520><c> these</c>

00:08:11.749 --> 00:08:11.759 align:start position:0%
model with Al algebraic effects so these
 

00:08:11.759 --> 00:08:13.790 align:start position:0%
model with Al algebraic effects so these
two<00:08:12.039><c> things</c><00:08:12.360><c> combined</c><00:08:12.840><c> is</c><00:08:13.000><c> what</c><00:08:13.159><c> allows</c><00:08:13.479><c> us</c><00:08:13.639><c> to</c>

00:08:13.790 --> 00:08:13.800 align:start position:0%
two things combined is what allows us to
 

00:08:13.800 --> 00:08:16.869 align:start position:0%
two things combined is what allows us to
have<00:08:13.919><c> the</c><00:08:14.080><c> neat</c><00:08:14.840><c> uh</c><00:08:15.840><c> uh</c><00:08:16.120><c> expressiveness</c><00:08:16.759><c> in</c>

00:08:16.869 --> 00:08:16.879 align:start position:0%
have the neat uh uh expressiveness in
 

00:08:16.879 --> 00:08:19.029 align:start position:0%
have the neat uh uh expressiveness in
the<00:08:17.000><c> type</c><00:08:17.240><c> signatures</c><00:08:17.879><c> that</c><00:08:18.000><c> we</c><00:08:18.080><c> saw</c>

00:08:19.029 --> 00:08:19.039 align:start position:0%
the type signatures that we saw
 

00:08:19.039 --> 00:08:22.230 align:start position:0%
the type signatures that we saw
before<00:08:20.039><c> and</c><00:08:20.720><c> Idris</c><00:08:21.120><c> is</c><00:08:21.319><c> also</c><00:08:21.759><c> strictly</c>

00:08:22.230 --> 00:08:22.240 align:start position:0%
before and Idris is also strictly
 

00:08:22.240 --> 00:08:24.270 align:start position:0%
before and Idris is also strictly
evaluated<00:08:22.879><c> from</c><00:08:23.039><c> the</c><00:08:23.159><c> GetGo</c><00:08:23.720><c> so</c><00:08:24.000><c> we</c><00:08:24.120><c> don't</c>

00:08:24.270 --> 00:08:24.280 align:start position:0%
evaluated from the GetGo so we don't
 

00:08:24.280 --> 00:08:26.670 align:start position:0%
evaluated from the GetGo so we don't
need<00:08:24.440><c> to</c><00:08:24.680><c> have</c><00:08:25.280><c> make</c><00:08:25.479><c> any</c><00:08:25.639><c> changes</c><00:08:26.080><c> there</c><00:08:26.560><c> and</c>

00:08:26.670 --> 00:08:26.680 align:start position:0%
need to have make any changes there and
 

00:08:26.680 --> 00:08:29.909 align:start position:0%
need to have make any changes there and
as<00:08:26.800><c> a</c><00:08:26.960><c> nice</c><00:08:27.240><c> bonus</c><00:08:28.000><c> we</c><00:08:28.479><c> don't</c><00:08:28.840><c> have</c><00:08:29.000><c> to</c><00:08:29.159><c> venture</c>

00:08:29.909 --> 00:08:29.919 align:start position:0%
as a nice bonus we don't have to venture
 

00:08:29.919 --> 00:08:32.070 align:start position:0%
as a nice bonus we don't have to venture
down<00:08:30.080><c> into</c><00:08:30.280><c> the</c><00:08:30.400><c> murky</c><00:08:30.800><c> depths</c><00:08:31.120><c> of</c><00:08:31.280><c> the</c><00:08:31.440><c> GHC</c>

00:08:32.070 --> 00:08:32.080 align:start position:0%
down into the murky depths of the GHC
 

00:08:32.080 --> 00:08:34.509 align:start position:0%
down into the murky depths of the GHC
API<00:08:32.880><c> if</c><00:08:32.959><c> you're</c><00:08:33.200><c> familiar</c><00:08:33.640><c> with</c>

00:08:34.509 --> 00:08:34.519 align:start position:0%
API if you're familiar with
 

00:08:34.519 --> 00:08:38.070 align:start position:0%
API if you're familiar with
that<00:08:35.640><c> um</c><00:08:36.640><c> so</c><00:08:36.959><c> I</c><00:08:37.080><c> hope</c><00:08:37.279><c> we</c><00:08:37.399><c> have</c><00:08:37.560><c> shown</c><00:08:37.880><c> how</c>

00:08:38.070 --> 00:08:38.080 align:start position:0%
that um so I hope we have shown how
 

00:08:38.080 --> 00:08:40.350 align:start position:0%
that um so I hope we have shown how
dependent<00:08:38.519><c> types</c><00:08:38.760><c> and</c><00:08:39.240><c> algebraic</c><00:08:39.839><c> effects</c>

00:08:40.350 --> 00:08:40.360 align:start position:0%
dependent types and algebraic effects
 

00:08:40.360 --> 00:08:42.310 align:start position:0%
dependent types and algebraic effects
can<00:08:40.479><c> be</c><00:08:40.599><c> used</c><00:08:41.000><c> together</c><00:08:41.320><c> to</c><00:08:41.519><c> define</c><00:08:41.880><c> the</c><00:08:42.000><c> flow</c>

00:08:42.310 --> 00:08:42.320 align:start position:0%
can be used together to define the flow
 

00:08:42.320 --> 00:08:45.150 align:start position:0%
can be used together to define the flow
of<00:08:42.479><c> ether</c><00:08:43.159><c> throughout</c><00:08:43.800><c> execution</c><00:08:44.240><c> of</c><00:08:44.360><c> a</c>

00:08:45.150 --> 00:08:45.160 align:start position:0%
of ether throughout execution of a
 

00:08:45.160 --> 00:08:48.630 align:start position:0%
of ether throughout execution of a
contract<00:08:46.160><c> and</c><00:08:46.519><c> we'll</c><00:08:46.720><c> see</c><00:08:47.080><c> how</c><00:08:48.040><c> we</c><00:08:48.200><c> have</c><00:08:48.320><c> seen</c>

00:08:48.630 --> 00:08:48.640 align:start position:0%
contract and we'll see how we have seen
 

00:08:48.640 --> 00:08:51.470 align:start position:0%
contract and we'll see how we have seen
how<00:08:49.040><c> high</c><00:08:49.320><c> level</c><00:08:50.040><c> type</c><00:08:50.320><c> annotations</c><00:08:51.320><c> can</c>

00:08:51.470 --> 00:08:51.480 align:start position:0%
how high level type annotations can
 

00:08:51.480 --> 00:08:53.190 align:start position:0%
how high level type annotations can
ensure<00:08:51.839><c> that</c><00:08:52.000><c> secret</c><00:08:52.399><c> information</c><00:08:52.880><c> stays</c>

00:08:53.190 --> 00:08:53.200 align:start position:0%
ensure that secret information stays
 

00:08:53.200 --> 00:08:55.310 align:start position:0%
ensure that secret information stays
secret<00:08:53.760><c> until</c><00:08:54.000><c> it's</c><00:08:54.160><c> supposed</c><00:08:54.440><c> to</c><00:08:54.519><c> be</c>

00:08:55.310 --> 00:08:55.320 align:start position:0%
secret until it's supposed to be
 

00:08:55.320 --> 00:08:58.430 align:start position:0%
secret until it's supposed to be
revealed<00:08:56.320><c> and</c><00:08:56.839><c> we</c><00:08:57.000><c> have</c><00:08:57.120><c> a</c><00:08:57.320><c> language</c><00:08:57.920><c> where</c>

00:08:58.430 --> 00:08:58.440 align:start position:0%
revealed and we have a language where
 

00:08:58.440 --> 00:09:00.110 align:start position:0%
revealed and we have a language where
compositionality<00:08:59.279><c> can</c><00:08:59.440><c> can</c><00:08:59.560><c> be</c><00:08:59.680><c> achieved</c><00:09:00.000><c> in</c>

00:09:00.110 --> 00:09:00.120 align:start position:0%
compositionality can can be achieved in
 

00:09:00.120 --> 00:09:02.230 align:start position:0%
compositionality can can be achieved in
a<00:09:00.519><c> natural</c>

00:09:02.230 --> 00:09:02.240 align:start position:0%
a natural
 

00:09:02.240 --> 00:09:06.630 align:start position:0%
a natural
way<00:09:03.240><c> so</c><00:09:04.120><c> where</c><00:09:04.320><c> are</c><00:09:04.519><c> we</c><00:09:04.800><c> currently</c><00:09:05.320><c> with</c><00:09:05.640><c> this</c>

00:09:06.630 --> 00:09:06.640 align:start position:0%
way so where are we currently with this
 

00:09:06.640 --> 00:09:08.069 align:start position:0%
way so where are we currently with this
well<00:09:06.800><c> we</c><00:09:06.920><c> still</c><00:09:07.079><c> have</c><00:09:07.200><c> a</c><00:09:07.320><c> long</c><00:09:07.519><c> way</c><00:09:07.680><c> to</c><00:09:07.839><c> go</c>

00:09:08.069 --> 00:09:08.079 align:start position:0%
well we still have a long way to go
 

00:09:08.079 --> 00:09:10.269 align:start position:0%
well we still have a long way to go
before<00:09:08.320><c> it's</c><00:09:08.680><c> actually</c><00:09:08.959><c> usable</c><00:09:09.399><c> in</c><00:09:09.600><c> practice</c>

00:09:10.269 --> 00:09:10.279 align:start position:0%
before it's actually usable in practice
 

00:09:10.279 --> 00:09:12.750 align:start position:0%
before it's actually usable in practice
to<00:09:10.480><c> create</c><00:09:10.920><c> working</c><00:09:11.560><c> smart</c><00:09:11.920><c> contract</c><00:09:12.320><c> bite</c>

00:09:12.750 --> 00:09:12.760 align:start position:0%
to create working smart contract bite
 

00:09:12.760 --> 00:09:15.670 align:start position:0%
to create working smart contract bite
code<00:09:13.760><c> uh</c><00:09:14.040><c> we</c><00:09:14.240><c> have</c><00:09:14.480><c> created</c><00:09:14.880><c> models</c><00:09:15.399><c> for</c><00:09:15.560><c> how</c>

00:09:15.670 --> 00:09:15.680 align:start position:0%
code uh we have created models for how
 

00:09:15.680 --> 00:09:17.870 align:start position:0%
code uh we have created models for how
we<00:09:15.800><c> want</c><00:09:16.000><c> stuff</c><00:09:16.200><c> to</c><00:09:16.360><c> look</c><00:09:16.560><c> for</c><00:09:16.760><c> the</c><00:09:16.959><c> developer</c>

00:09:17.870 --> 00:09:17.880 align:start position:0%
we want stuff to look for the developer
 

00:09:17.880 --> 00:09:20.150 align:start position:0%
we want stuff to look for the developer
and<00:09:18.120><c> made</c><00:09:18.360><c> sure</c><00:09:18.760><c> that</c><00:09:19.160><c> all</c><00:09:19.320><c> the</c><00:09:19.480><c> properties</c><00:09:20.000><c> we</c>

00:09:20.150 --> 00:09:20.160 align:start position:0%
and made sure that all the properties we
 

00:09:20.160 --> 00:09:22.030 align:start position:0%
and made sure that all the properties we
want<00:09:20.320><c> to</c><00:09:20.560><c> enforce</c><00:09:21.040><c> can</c><00:09:21.200><c> be</c><00:09:21.360><c> enforced</c><00:09:21.760><c> using</c>

00:09:22.030 --> 00:09:22.040 align:start position:0%
want to enforce can be enforced using
 

00:09:22.040 --> 00:09:25.389 align:start position:0%
want to enforce can be enforced using
addresses<00:09:22.600><c> type</c><00:09:23.160><c> system</c><00:09:24.160><c> and</c><00:09:24.519><c> we</c><00:09:24.720><c> have</c><00:09:25.120><c> just</c>

00:09:25.389 --> 00:09:25.399 align:start position:0%
addresses type system and we have just
 

00:09:25.399 --> 00:09:27.670 align:start position:0%
addresses type system and we have just
recently<00:09:25.800><c> started</c><00:09:26.200><c> looking</c><00:09:26.600><c> at</c><00:09:27.120><c> uh</c><00:09:27.320><c> how</c><00:09:27.519><c> we</c>

00:09:27.670 --> 00:09:27.680 align:start position:0%
recently started looking at uh how we
 

00:09:27.680 --> 00:09:29.990 align:start position:0%
recently started looking at uh how we
can<00:09:28.279><c> create</c><00:09:28.519><c> a</c><00:09:28.640><c> code</c><00:09:28.880><c> generator</c><00:09:29.680><c> that</c><00:09:29.760><c> will</c>

00:09:29.990 --> 00:09:30.000 align:start position:0%
can create a code generator that will
 

00:09:30.000 --> 00:09:34.030 align:start position:0%
can create a code generator that will
take<00:09:30.920><c> that</c><00:09:31.000><c> will</c><00:09:31.200><c> go</c><00:09:31.399><c> from</c><00:09:31.640><c> midis</c><00:09:32.200><c> to</c><00:09:32.839><c> lll</c><00:09:33.839><c> um</c>

00:09:34.030 --> 00:09:34.040 align:start position:0%
take that will go from midis to lll um
 

00:09:34.040 --> 00:09:36.269 align:start position:0%
take that will go from midis to lll um
in<00:09:34.160><c> a</c><00:09:34.279><c> similar</c><00:09:34.600><c> way</c><00:09:34.720><c> the</c><00:09:34.839><c> serpent</c><00:09:35.200><c> does</c><00:09:35.399><c> it</c>

00:09:36.269 --> 00:09:36.279 align:start position:0%
in a similar way the serpent does it
 

00:09:36.279 --> 00:09:52.350 align:start position:0%
in a similar way the serpent does it
today<00:09:37.519><c> and</c><00:09:38.519><c> that's</c><00:09:39.160><c> it</c><00:09:39.519><c> for</c><00:09:39.760><c> us</c><00:09:40.320><c> thank</c><00:09:40.560><c> you</c>

00:09:52.350 --> 00:09:52.360 align:start position:0%
 
 

00:09:52.360 --> 00:09:56.249 align:start position:0%
 
[Music]