WEBVTT
Kind: captions
Language: en

00:00:07.610 --> 00:00:09.680 align:start position:0%
 
when<00:00:08.610><c> you</c><00:00:08.760><c> design</c><00:00:09.150><c> a</c><00:00:09.179><c> programming</c><00:00:09.660><c> language</c>

00:00:09.680 --> 00:00:09.690 align:start position:0%
when you design a programming language
 

00:00:09.690 --> 00:00:13.549 align:start position:0%
when you design a programming language
you<00:00:10.559><c> have</c><00:00:11.219><c> to</c><00:00:11.400><c> make</c><00:00:11.550><c> compromises</c><00:00:12.559><c> constantly</c>

00:00:13.549 --> 00:00:13.559 align:start position:0%
you have to make compromises constantly
 

00:00:13.559 --> 00:00:18.170 align:start position:0%
you have to make compromises constantly
there<00:00:13.769><c> are</c><00:00:15.199><c> people</c><00:00:16.199><c> who</c><00:00:16.770><c> request</c><00:00:17.730><c> features</c>

00:00:18.170 --> 00:00:18.180 align:start position:0%
there are people who request features
 

00:00:18.180 --> 00:00:20.720 align:start position:0%
there are people who request features
and<00:00:18.390><c> of</c><00:00:19.199><c> course</c><00:00:19.439><c> features</c><00:00:19.619><c> are</c><00:00:19.830><c> nice</c><00:00:19.980><c> but</c><00:00:20.279><c> with</c>

00:00:20.720 --> 00:00:20.730 align:start position:0%
and of course features are nice but with
 

00:00:20.730 --> 00:00:22.730 align:start position:0%
and of course features are nice but with
each<00:00:21.090><c> new</c><00:00:21.480><c> feature</c><00:00:21.750><c> the</c><00:00:22.080><c> language</c><00:00:22.380><c> gets</c><00:00:22.560><c> more</c>

00:00:22.730 --> 00:00:22.740 align:start position:0%
each new feature the language gets more
 

00:00:22.740 --> 00:00:26.390 align:start position:0%
each new feature the language gets more
complicated<00:00:23.100><c> and</c><00:00:23.580><c> thus</c><00:00:24.380><c> easier</c><00:00:25.380><c> harder</c><00:00:26.130><c> to</c>

00:00:26.390 --> 00:00:26.400 align:start position:0%
complicated and thus easier harder to
 

00:00:26.400 --> 00:00:29.000 align:start position:0%
complicated and thus easier harder to
understand<00:00:26.880><c> and</c><00:00:27.300><c> it's</c><00:00:27.779><c> easier</c><00:00:28.710><c> to</c><00:00:28.740><c> make</c><00:00:28.980><c> a</c>

00:00:29.000 --> 00:00:29.010 align:start position:0%
understand and it's easier to make a
 

00:00:29.010 --> 00:00:30.259 align:start position:0%
understand and it's easier to make a
mistake<00:00:29.460><c> the</c><00:00:29.609><c> more</c><00:00:29.760><c> complicated</c><00:00:30.210><c> the</c>

00:00:30.259 --> 00:00:30.269 align:start position:0%
mistake the more complicated the
 

00:00:30.269 --> 00:00:31.669 align:start position:0%
mistake the more complicated the
language<00:00:30.599><c> is</c><00:00:30.750><c> so</c><00:00:30.840><c> you</c><00:00:30.929><c> have</c><00:00:30.960><c> the</c><00:00:31.289><c> constant</c>

00:00:31.669 --> 00:00:31.679 align:start position:0%
language is so you have the constant
 

00:00:31.679 --> 00:00:34.430 align:start position:0%
language is so you have the constant
balance<00:00:31.949><c> between</c><00:00:32.630><c> functionality</c><00:00:33.630><c> and</c><00:00:33.870><c> safety</c>

00:00:34.430 --> 00:00:34.440 align:start position:0%
balance between functionality and safety
 

00:00:34.440 --> 00:00:38.119 align:start position:0%
balance between functionality and safety
of<00:00:34.649><c> course</c><00:00:35.309><c> there</c><00:00:35.550><c> are</c><00:00:36.270><c> features</c><00:00:37.170><c> that</c><00:00:37.980><c> are</c>

00:00:38.119 --> 00:00:38.129 align:start position:0%
of course there are features that are
 

00:00:38.129 --> 00:00:41.660 align:start position:0%
of course there are features that are
safe<00:00:38.489><c> but</c><00:00:38.969><c> yeah</c><00:00:39.870><c> that's</c><00:00:40.020><c> the</c><00:00:40.370><c> compromise</c><00:00:41.370><c> you</c>

00:00:41.660 --> 00:00:41.670 align:start position:0%
safe but yeah that's the compromise you
 

00:00:41.670 --> 00:00:46.459 align:start position:0%
safe but yeah that's the compromise you
have<00:00:41.820><c> to</c><00:00:41.969><c> find</c><00:00:42.210><c> and</c><00:00:44.809><c> this</c><00:00:45.809><c> has</c><00:00:45.989><c> not</c><00:00:46.140><c> been</c><00:00:46.350><c> the</c>

00:00:46.459 --> 00:00:46.469 align:start position:0%
have to find and this has not been the
 

00:00:46.469 --> 00:00:48.799 align:start position:0%
have to find and this has not been the
case<00:00:46.649><c> for</c><00:00:47.270><c> general-purpose</c><00:00:48.270><c> programming</c>

00:00:48.799 --> 00:00:48.809 align:start position:0%
case for general-purpose programming
 

00:00:48.809 --> 00:00:51.310 align:start position:0%
case for general-purpose programming
languages<00:00:49.590><c> for</c><00:00:49.800><c> several</c><00:00:50.100><c> years</c><00:00:50.250><c> now</c><00:00:50.309><c> but</c><00:00:50.910><c> in</c>

00:00:51.310 --> 00:00:51.320 align:start position:0%
languages for several years now but in
 

00:00:51.320 --> 00:00:54.650 align:start position:0%
languages for several years now but in
blockchain<00:00:52.370><c> there's</c><00:00:53.370><c> always</c><00:00:53.579><c> the</c><00:00:54.059><c> factor</c><00:00:54.449><c> of</c>

00:00:54.650 --> 00:00:54.660 align:start position:0%
blockchain there's always the factor of
 

00:00:54.660 --> 00:00:59.150 align:start position:0%
blockchain there's always the factor of
cost<00:00:55.260><c> so</c><00:00:57.109><c> smart</c><00:00:58.109><c> contracts</c><00:00:58.590><c> have</c><00:00:58.739><c> to</c><00:00:58.890><c> be</c><00:00:58.980><c> very</c>

00:00:59.150 --> 00:00:59.160 align:start position:0%
cost so smart contracts have to be very
 

00:00:59.160 --> 00:01:01.610 align:start position:0%
cost so smart contracts have to be very
cheap<00:00:59.399><c> to</c><00:00:59.550><c> execute</c><00:01:00.090><c> and</c><00:01:00.329><c> that</c><00:01:00.809><c> also</c><00:01:01.260><c> limits</c>

00:01:01.610 --> 00:01:01.620 align:start position:0%
cheap to execute and that also limits
 

00:01:01.620 --> 00:01:10.120 align:start position:0%
cheap to execute and that also limits
the<00:01:01.680><c> features</c><00:01:02.070><c> you</c><00:01:02.190><c> can</c><00:01:02.280><c> add</c><00:01:02.340><c> in</c><00:01:02.879><c> a</c><00:01:02.969><c> language</c>

00:01:10.120 --> 00:01:10.130 align:start position:0%
 
 

00:01:10.130 --> 00:01:12.560 align:start position:0%
 
back<00:01:11.130><c> in</c><00:01:11.250><c> the</c><00:01:11.369><c> days</c><00:01:11.549><c> when</c><00:01:11.909><c> solidity</c><00:01:12.330><c> was</c>

00:01:12.560 --> 00:01:12.570 align:start position:0%
back in the days when solidity was
 

00:01:12.570 --> 00:01:15.980 align:start position:0%
back in the days when solidity was
started<00:01:12.990><c> the</c><00:01:13.320><c> initial</c><00:01:14.220><c> goal</c><00:01:14.400><c> was</c><00:01:14.909><c> to</c><00:01:15.240><c> create</c><00:01:15.540><c> a</c>

00:01:15.980 --> 00:01:15.990 align:start position:0%
started the initial goal was to create a
 

00:01:15.990 --> 00:01:18.679 align:start position:0%
started the initial goal was to create a
usable<00:01:16.530><c> high</c><00:01:16.650><c> language</c><00:01:17.330><c> high-level</c><00:01:18.330><c> language</c>

00:01:18.679 --> 00:01:18.689 align:start position:0%
usable high language high-level language
 

00:01:18.689 --> 00:01:20.810 align:start position:0%
usable high language high-level language
as<00:01:18.930><c> fast</c><00:01:19.200><c> as</c><00:01:19.350><c> possible</c><00:01:19.740><c> and</c><00:01:19.920><c> I</c><00:01:20.159><c> think</c><00:01:20.700><c> we</c>

00:01:20.810 --> 00:01:20.820 align:start position:0%
as fast as possible and I think we
 

00:01:20.820 --> 00:01:23.660 align:start position:0%
as fast as possible and I think we
succeeded<00:01:20.970><c> in</c><00:01:21.390><c> that</c><00:01:21.420><c> but</c><00:01:22.380><c> of</c><00:01:22.950><c> course</c><00:01:23.250><c> we</c><00:01:23.460><c> made</c>

00:01:23.660 --> 00:01:23.670 align:start position:0%
succeeded in that but of course we made
 

00:01:23.670 --> 00:01:26.420 align:start position:0%
succeeded in that but of course we made
some<00:01:23.880><c> decisions</c><00:01:24.150><c> we</c><00:01:24.540><c> now</c><00:01:25.200><c> yeah</c><00:01:25.979><c> which</c><00:01:26.130><c> turned</c>

00:01:26.420 --> 00:01:26.430 align:start position:0%
some decisions we now yeah which turned
 

00:01:26.430 --> 00:01:29.690 align:start position:0%
some decisions we now yeah which turned
out<00:01:26.580><c> to</c><00:01:26.729><c> be</c><00:01:26.820><c> not</c><00:01:26.939><c> that</c><00:01:28.280><c> not</c><00:01:29.280><c> to</c><00:01:29.400><c> be</c><00:01:29.490><c> the</c><00:01:29.579><c> best</c>

00:01:29.690 --> 00:01:29.700 align:start position:0%
out to be not that not to be the best
 

00:01:29.700 --> 00:01:32.810 align:start position:0%
out to be not that not to be the best
decisions<00:01:30.240><c> and</c><00:01:30.829><c> now</c><00:01:31.829><c> is</c><00:01:32.009><c> the</c><00:01:32.340><c> time</c><00:01:32.369><c> to</c><00:01:32.670><c> change</c>

00:01:32.810 --> 00:01:32.820 align:start position:0%
decisions and now is the time to change
 

00:01:32.820 --> 00:01:37.760 align:start position:0%
decisions and now is the time to change
them<00:01:33.119><c> and</c><00:01:33.530><c> solidity</c><00:01:34.530><c> is</c><00:01:34.979><c> still</c><00:01:35.310><c> a</c><00:01:36.770><c> language</c>

00:01:37.760 --> 00:01:37.770 align:start position:0%
them and solidity is still a language
 

00:01:37.770 --> 00:01:42.050 align:start position:0%
them and solidity is still a language
that<00:01:37.950><c> changes</c><00:01:38.490><c> and</c><00:01:39.320><c> that</c><00:01:40.320><c> allows</c><00:01:40.860><c> us</c><00:01:41.130><c> to</c><00:01:41.369><c> make</c>

00:01:42.050 --> 00:01:42.060 align:start position:0%
that changes and that allows us to make
 

00:01:42.060 --> 00:01:45.490 align:start position:0%
that changes and that allows us to make
the<00:01:42.210><c> necessary</c><00:01:42.360><c> changes</c><00:01:42.990><c> to</c><00:01:43.619><c> the</c><00:01:44.220><c> design</c><00:01:44.340><c> and</c>

00:01:45.490 --> 00:01:45.500 align:start position:0%
the necessary changes to the design and
 

00:01:45.500 --> 00:01:48.950 align:start position:0%
the necessary changes to the design and
yeah<00:01:46.500><c> the</c><00:01:46.649><c> the</c><00:01:46.680><c> path</c><00:01:47.250><c> you</c><00:01:47.399><c> want</c><00:01:47.579><c> to</c><00:01:47.640><c> go</c><00:01:47.790><c> is</c><00:01:48.000><c> we</c>

00:01:48.950 --> 00:01:48.960 align:start position:0%
yeah the the path you want to go is we
 

00:01:48.960 --> 00:01:52.100 align:start position:0%
yeah the the path you want to go is we
want<00:01:49.170><c> to</c><00:01:49.290><c> keep</c><00:01:50.630><c> features</c><00:01:51.630><c> that</c><00:01:51.899><c> are</c>

00:01:52.100 --> 00:01:52.110 align:start position:0%
want to keep features that are
 

00:01:52.110 --> 00:01:58.819 align:start position:0%
want to keep features that are
relatively<00:01:52.860><c> safe</c><00:01:53.159><c> and</c><00:01:54.170><c> we</c><00:01:55.969><c> they</c><00:01:57.469><c> look</c><00:01:58.469><c> like</c>

00:01:58.819 --> 00:01:58.829 align:start position:0%
relatively safe and we they look like
 

00:01:58.829 --> 00:02:01.069 align:start position:0%
relatively safe and we they look like
high-level<00:01:59.490><c> features</c><00:02:00.149><c> but</c><00:02:00.420><c> most</c><00:02:00.659><c> of</c><00:02:00.810><c> them</c><00:02:00.960><c> are</c>

00:02:01.069 --> 00:02:01.079 align:start position:0%
high-level features but most of them are
 

00:02:01.079 --> 00:02:03.859 align:start position:0%
high-level features but most of them are
actually<00:02:01.469><c> quite</c><00:02:01.500><c> low</c><00:02:02.399><c> level</c><00:02:02.759><c> so</c><00:02:02.969><c> we</c><00:02:03.570><c> want</c><00:02:03.780><c> to</c>

00:02:03.859 --> 00:02:03.869 align:start position:0%
actually quite low level so we want to
 

00:02:03.869 --> 00:02:06.170 align:start position:0%
actually quite low level so we want to
have<00:02:03.990><c> features</c><00:02:04.380><c> that</c><00:02:04.560><c> that</c><00:02:04.790><c> look</c><00:02:05.790><c> like</c><00:02:06.000><c> here</c>

00:02:06.170 --> 00:02:06.180 align:start position:0%
have features that that look like here
 

00:02:06.180 --> 00:02:07.969 align:start position:0%
have features that that look like here
look<00:02:06.420><c> look</c><00:02:06.689><c> like</c><00:02:06.869><c> high</c><00:02:07.229><c> level</c><00:02:07.259><c> features</c><00:02:07.770><c> but</c>

00:02:07.969 --> 00:02:07.979 align:start position:0%
look look like high level features but
 

00:02:07.979 --> 00:02:12.500 align:start position:0%
look look like high level features but
are<00:02:08.220><c> still</c><00:02:09.000><c> cheap</c><00:02:09.959><c> and</c><00:02:11.030><c> we</c><00:02:12.030><c> want</c><00:02:12.209><c> to</c><00:02:12.270><c> remove</c>

00:02:12.500 --> 00:02:12.510 align:start position:0%
are still cheap and we want to remove
 

00:02:12.510 --> 00:02:13.730 align:start position:0%
are still cheap and we want to remove
everything<00:02:12.810><c> that</c>

00:02:13.730 --> 00:02:13.740 align:start position:0%
everything that
 

00:02:13.740 --> 00:02:16.310 align:start position:0%
everything that
can<00:02:14.160><c> surprise</c><00:02:14.520><c> users</c><00:02:15.060><c> or</c><00:02:15.210><c> has</c><00:02:15.420><c> some</c><00:02:15.690><c> semantic</c>

00:02:16.310 --> 00:02:16.320 align:start position:0%
can surprise users or has some semantic
 

00:02:16.320 --> 00:02:20.660 align:start position:0%
can surprise users or has some semantic
involved<00:02:16.770><c> and</c><00:02:17.010><c> then</c><00:02:17.760><c> a</c><00:02:17.790><c> third</c><00:02:18.150><c> factor</c><00:02:18.630><c> is</c><00:02:19.670><c> we</c>

00:02:20.660 --> 00:02:20.670 align:start position:0%
involved and then a third factor is we
 

00:02:20.670 --> 00:02:23.420 align:start position:0%
involved and then a third factor is we
are<00:02:21.570><c> adding</c><00:02:22.200><c> formal</c><00:02:22.560><c> verification</c><00:02:22.710><c> tools</c>

00:02:23.420 --> 00:02:23.430 align:start position:0%
are adding formal verification tools
 

00:02:23.430 --> 00:02:26.150 align:start position:0%
are adding formal verification tools
that<00:02:23.610><c> are</c><00:02:23.790><c> easy</c><00:02:24.240><c> to</c><00:02:24.510><c> use</c><00:02:24.540><c> and</c><00:02:24.990><c> this</c><00:02:25.650><c> I</c><00:02:25.950><c> would</c>

00:02:26.150 --> 00:02:26.160 align:start position:0%
that are easy to use and this I would
 

00:02:26.160 --> 00:02:27.830 align:start position:0%
that are easy to use and this I would
like<00:02:26.340><c> to</c><00:02:26.430><c> stress</c><00:02:26.640><c> this</c><00:02:26.940><c> easy-to-use</c><00:02:27.330><c> part</c>

00:02:27.830 --> 00:02:27.840 align:start position:0%
like to stress this easy-to-use part
 

00:02:27.840 --> 00:02:29.750 align:start position:0%
like to stress this easy-to-use part
because<00:02:28.170><c> that</c><00:02:28.890><c> is</c><00:02:29.010><c> essential</c><00:02:29.400><c> and</c><00:02:29.490><c> we</c><00:02:29.610><c> will</c>

00:02:29.750 --> 00:02:29.760 align:start position:0%
because that is essential and we will
 

00:02:29.760 --> 00:02:33.260 align:start position:0%
because that is essential and we will
see<00:02:30.060><c> that</c><00:02:30.210><c> later</c><00:02:30.600><c> in</c><00:02:30.870><c> the</c><00:02:30.960><c> talk</c><00:02:31.110><c> and</c><00:02:31.650><c> then</c><00:02:32.640><c> if</c>

00:02:33.260 --> 00:02:33.270 align:start position:0%
see that later in the talk and then if
 

00:02:33.270 --> 00:02:35.510 align:start position:0%
see that later in the talk and then if
there<00:02:33.480><c> is</c><00:02:33.570><c> not</c><00:02:33.720><c> enough</c><00:02:33.750><c> for</c><00:02:34.110><c> you</c><00:02:34.260><c> we</c><00:02:34.770><c> provide</c>

00:02:35.510 --> 00:02:35.520 align:start position:0%
there is not enough for you we provide
 

00:02:35.520 --> 00:02:38.390 align:start position:0%
there is not enough for you we provide
direct<00:02:36.300><c> way</c><00:02:36.690><c> to</c><00:02:36.720><c> access</c><00:02:37.350><c> very</c><00:02:37.650><c> very</c><00:02:37.920><c> low</c><00:02:38.100><c> level</c>

00:02:38.390 --> 00:02:38.400 align:start position:0%
direct way to access very very low level
 

00:02:38.400 --> 00:02:40.220 align:start position:0%
direct way to access very very low level
features<00:02:38.790><c> of</c><00:02:39.000><c> the</c><00:02:39.210><c> etherium</c><00:02:39.630><c> virtual</c><00:02:39.930><c> machine</c>

00:02:40.220 --> 00:02:40.230 align:start position:0%
features of the etherium virtual machine
 

00:02:40.230 --> 00:02:43.190 align:start position:0%
features of the etherium virtual machine
and<00:02:40.380><c> the</c><00:02:40.910><c> important</c><00:02:41.910><c> point</c><00:02:42.060><c> is</c><00:02:42.210><c> here</c><00:02:42.510><c> that</c><00:02:42.720><c> we</c>

00:02:43.190 --> 00:02:43.200 align:start position:0%
and the important point is here that we
 

00:02:43.200 --> 00:02:45.110 align:start position:0%
and the important point is here that we
remove<00:02:44.040><c> everything</c><00:02:44.580><c> that</c><00:02:44.730><c> is</c><00:02:44.820><c> kind</c><00:02:45.060><c> of</c>

00:02:45.110 --> 00:02:45.120 align:start position:0%
remove everything that is kind of
 

00:02:45.120 --> 00:02:47.180 align:start position:0%
remove everything that is kind of
intermediate<00:02:46.050><c> level</c><00:02:46.410><c> so</c><00:02:46.560><c> for</c><00:02:46.710><c> example</c>

00:02:47.180 --> 00:02:47.190 align:start position:0%
intermediate level so for example
 

00:02:47.190 --> 00:02:49.460 align:start position:0%
intermediate level so for example
address<00:02:47.940><c> dot</c><00:02:48.150><c> call</c><00:02:48.450><c> will</c><00:02:48.720><c> be</c><00:02:48.750><c> removed</c><00:02:49.230><c> in</c><00:02:49.380><c> the</c>

00:02:49.460 --> 00:02:49.470 align:start position:0%
address dot call will be removed in the
 

00:02:49.470 --> 00:02:54.560 align:start position:0%
address dot call will be removed in the
future<00:02:49.770><c> because</c><00:02:51.230><c> it</c><00:02:52.230><c> has</c><00:02:52.470><c> some</c><00:02:53.270><c> magic</c><00:02:54.270><c> some</c>

00:02:54.560 --> 00:02:54.570 align:start position:0%
future because it has some magic some
 

00:02:54.570 --> 00:02:56.900 align:start position:0%
future because it has some magic some
some<00:02:54.870><c> unexpected</c><00:02:55.290><c> things</c><00:02:55.500><c> involved</c><00:02:56.460><c> that</c><00:02:56.610><c> we</c>

00:02:56.900 --> 00:02:56.910 align:start position:0%
some unexpected things involved that we
 

00:02:56.910 --> 00:02:59.060 align:start position:0%
some unexpected things involved that we
would<00:02:57.030><c> like</c><00:02:57.180><c> to</c><00:02:57.210><c> avoid</c><00:02:57.570><c> so</c><00:02:57.900><c> if</c><00:02:58.380><c> you</c><00:02:58.590><c> want</c><00:02:58.770><c> to</c><00:02:58.890><c> do</c>

00:02:59.060 --> 00:02:59.070 align:start position:0%
would like to avoid so if you want to do
 

00:02:59.070 --> 00:03:00.860 align:start position:0%
would like to avoid so if you want to do
such<00:02:59.430><c> low-level</c><00:02:59.850><c> things</c><00:03:00.030><c> you</c><00:03:00.330><c> have</c><00:03:00.450><c> to</c><00:03:00.480><c> go</c><00:03:00.720><c> all</c>

00:03:00.860 --> 00:03:00.870 align:start position:0%
such low-level things you have to go all
 

00:03:00.870 --> 00:03:02.150 align:start position:0%
such low-level things you have to go all
the<00:03:00.900><c> way</c><00:03:01.020><c> down</c><00:03:01.260><c> to</c><00:03:01.410><c> the</c><00:03:01.560><c> human</c><00:03:01.740><c> virtual</c>

00:03:02.150 --> 00:03:02.160 align:start position:0%
the way down to the human virtual
 

00:03:02.160 --> 00:03:10.550 align:start position:0%
the way down to the human virtual
machine<00:03:05.240><c> ok</c><00:03:06.380><c> this</c><00:03:07.380><c> is</c><00:03:07.790><c> kind</c><00:03:08.790><c> of</c><00:03:08.850><c> the</c><00:03:09.380><c> the</c><00:03:10.380><c> path</c>

00:03:10.550 --> 00:03:10.560 align:start position:0%
machine ok this is kind of the the path
 

00:03:10.560 --> 00:03:11.900 align:start position:0%
machine ok this is kind of the the path
we<00:03:10.710><c> want</c><00:03:10.800><c> to</c><00:03:10.920><c> take</c><00:03:11.010><c> now</c><00:03:11.430><c> let's</c><00:03:11.730><c> talk</c><00:03:11.850><c> about</c>

00:03:11.900 --> 00:03:11.910 align:start position:0%
we want to take now let's talk about
 

00:03:11.910 --> 00:03:13.760 align:start position:0%
we want to take now let's talk about
some<00:03:12.270><c> new</c><00:03:12.390><c> features</c><00:03:12.420><c> we</c><00:03:12.900><c> added</c><00:03:12.930><c> in</c><00:03:13.290><c> the</c><00:03:13.470><c> last</c>

00:03:13.760 --> 00:03:13.770 align:start position:0%
some new features we added in the last
 

00:03:13.770 --> 00:03:18.440 align:start position:0%
some new features we added in the last
year<00:03:14.720><c> this</c><00:03:15.720><c> contract</c><00:03:16.560><c> here</c><00:03:16.980><c> is</c><00:03:17.220><c> a</c><00:03:17.450><c> simple</c>

00:03:18.440 --> 00:03:18.450 align:start position:0%
year this contract here is a simple
 

00:03:18.450 --> 00:03:21.950 align:start position:0%
year this contract here is a simple
database<00:03:18.660><c> that</c><00:03:19.080><c> stores</c><00:03:19.610><c> people</c><00:03:20.660><c> by</c><00:03:21.660><c> an</c>

00:03:21.950 --> 00:03:21.960 align:start position:0%
database that stores people by an
 

00:03:21.960 --> 00:03:24.410 align:start position:0%
database that stores people by an
identifier<00:03:22.620><c> a</c><00:03:22.650><c> name</c><00:03:23.160><c> and</c><00:03:23.550><c> some</c><00:03:23.850><c> flag</c><00:03:24.180><c> that</c>

00:03:24.410 --> 00:03:24.420 align:start position:0%
identifier a name and some flag that
 

00:03:24.420 --> 00:03:26.150 align:start position:0%
identifier a name and some flag that
says<00:03:24.630><c> whether</c><00:03:24.900><c> they</c><00:03:25.110><c> are</c><00:03:25.230><c> owner</c><00:03:25.560><c> of</c><00:03:25.770><c> something</c>

00:03:26.150 --> 00:03:26.160 align:start position:0%
says whether they are owner of something
 

00:03:26.160 --> 00:03:28.940 align:start position:0%
says whether they are owner of something
and<00:03:26.790><c> you</c><00:03:26.820><c> have</c><00:03:27.000><c> a</c><00:03:27.030><c> function</c><00:03:27.450><c> there</c><00:03:27.950><c> which</c>

00:03:28.940 --> 00:03:28.950 align:start position:0%
and you have a function there which
 

00:03:28.950 --> 00:03:31.550 align:start position:0%
and you have a function there which
allows<00:03:29.220><c> you</c><00:03:29.550><c> to</c><00:03:29.700><c> add</c><00:03:30.000><c> one</c><00:03:30.900><c> person</c><00:03:31.320><c> to</c><00:03:31.470><c> the</c>

00:03:31.550 --> 00:03:31.560 align:start position:0%
allows you to add one person to the
 

00:03:31.560 --> 00:03:35.270 align:start position:0%
allows you to add one person to the
database<00:03:33.320><c> it</c><00:03:34.320><c> already</c><00:03:34.680><c> looks</c><00:03:34.860><c> quite</c>

00:03:35.270 --> 00:03:35.280 align:start position:0%
database it already looks quite
 

00:03:35.280 --> 00:03:37.760 align:start position:0%
database it already looks quite
repetitive<00:03:35.580><c> and</c><00:03:36.240><c> but</c><00:03:37.140><c> it</c><00:03:37.260><c> gets</c><00:03:37.470><c> even</c><00:03:37.650><c> more</c>

00:03:37.760 --> 00:03:37.770 align:start position:0%
repetitive and but it gets even more
 

00:03:37.770 --> 00:03:39.080 align:start position:0%
repetitive and but it gets even more
complicated<00:03:38.010><c> if</c><00:03:38.490><c> you</c><00:03:38.520><c> want</c><00:03:38.700><c> to</c><00:03:38.790><c> add</c><00:03:38.910><c> a</c>

00:03:39.080 --> 00:03:39.090 align:start position:0%
complicated if you want to add a
 

00:03:39.090 --> 00:03:43.670 align:start position:0%
complicated if you want to add a
function<00:03:39.390><c> that</c><00:03:40.760><c> can</c><00:03:41.760><c> append</c><00:03:42.690><c> a</c><00:03:43.020><c> list</c><00:03:43.470><c> of</c>

00:03:43.670 --> 00:03:43.680 align:start position:0%
function that can append a list of
 

00:03:43.680 --> 00:03:47.170 align:start position:0%
function that can append a list of
people<00:03:44.040><c> into</c><00:03:44.400><c> that</c><00:03:44.490><c> database</c><00:03:45.380><c> the</c><00:03:46.380><c> problem</c>

00:03:47.170 --> 00:03:47.180 align:start position:0%
people into that database the problem
 

00:03:47.180 --> 00:03:51.170 align:start position:0%
people into that database the problem
many<00:03:48.180><c> people</c><00:03:48.870><c> run</c><00:03:49.440><c> into</c><00:03:49.590><c> is</c><00:03:49.890><c> that</c><00:03:50.220><c> you</c><00:03:50.820><c> kind</c><00:03:51.120><c> of</c>

00:03:51.170 --> 00:03:51.180 align:start position:0%
many people run into is that you kind of
 

00:03:51.180 --> 00:03:52.760 align:start position:0%
many people run into is that you kind of
have<00:03:51.420><c> to</c><00:03:51.600><c> create</c><00:03:51.870><c> an</c><00:03:51.990><c> array</c><00:03:52.260><c> out</c><00:03:52.470><c> of</c><00:03:52.620><c> these</c>

00:03:52.760 --> 00:03:52.770 align:start position:0%
have to create an array out of these
 

00:03:52.770 --> 00:03:54.950 align:start position:0%
have to create an array out of these
three<00:03:53.400><c> things</c><00:03:53.670><c> here</c><00:03:54.060><c> and</c><00:03:54.210><c> what</c><00:03:54.780><c> you</c><00:03:54.870><c> usually</c>

00:03:54.950 --> 00:03:54.960 align:start position:0%
three things here and what you usually
 

00:03:54.960 --> 00:03:58.010 align:start position:0%
three things here and what you usually
do<00:03:55.290><c> is</c><00:03:55.320><c> that</c><00:03:55.770><c> you</c><00:03:55.980><c> add</c><00:03:56.490><c> three</c><00:03:57.450><c> parameters</c>

00:03:58.010 --> 00:03:58.020 align:start position:0%
do is that you add three parameters
 

00:03:58.020 --> 00:04:00.830 align:start position:0%
do is that you add three parameters
which<00:03:58.200><c> are</c><00:03:58.380><c> each</c><00:03:59.040><c> an</c><00:03:59.400><c> array</c><00:03:59.700><c> this</c><00:04:00.660><c> of</c><00:04:00.810><c> course</c>

00:04:00.830 --> 00:04:00.840 align:start position:0%
which are each an array this of course
 

00:04:00.840 --> 00:04:02.420 align:start position:0%
which are each an array this of course
creates<00:04:01.140><c> the</c><00:04:01.410><c> problem</c><00:04:01.740><c> that</c><00:04:01.890><c> you</c><00:04:02.070><c> have</c><00:04:02.220><c> to</c>

00:04:02.420 --> 00:04:02.430 align:start position:0%
creates the problem that you have to
 

00:04:02.430 --> 00:04:04.400 align:start position:0%
creates the problem that you have to
check<00:04:03.120><c> that</c><00:04:03.270><c> all</c><00:04:03.840><c> of</c><00:04:04.080><c> them</c><00:04:04.170><c> have</c><00:04:04.290><c> the</c><00:04:04.380><c> same</c>

00:04:04.400 --> 00:04:04.410 align:start position:0%
check that all of them have the same
 

00:04:04.410 --> 00:04:06.170 align:start position:0%
check that all of them have the same
length<00:04:04.770><c> because</c><00:04:05.160><c> you</c><00:04:05.430><c> have</c><00:04:05.580><c> an</c><00:04:05.760><c> ID</c><00:04:06.060><c> that</c>

00:04:06.170 --> 00:04:06.180 align:start position:0%
length because you have an ID that
 

00:04:06.180 --> 00:04:11.060 align:start position:0%
length because you have an ID that
corresponds<00:04:06.720><c> to</c><00:04:06.810><c> name</c><00:04:07.080><c> and</c><00:04:08.180><c> this</c><00:04:09.180><c> flag</c><00:04:10.070><c> this</c>

00:04:11.060 --> 00:04:11.070 align:start position:0%
corresponds to name and this flag this
 

00:04:11.070 --> 00:04:13.690 align:start position:0%
corresponds to name and this flag this
looks<00:04:11.310><c> really</c><00:04:11.700><c> really</c><00:04:11.880><c> ugly</c><00:04:12.230><c> but</c><00:04:13.230><c> fortunately</c>

00:04:13.690 --> 00:04:13.700 align:start position:0%
looks really really ugly but fortunately
 

00:04:13.700 --> 00:04:18.370 align:start position:0%
looks really really ugly but fortunately
now<00:04:14.700><c> what</c><00:04:15.270><c> you</c><00:04:15.390><c> can</c><00:04:15.540><c> do</c><00:04:15.660><c> now</c><00:04:15.810><c> is</c><00:04:16.080><c> hope</c><00:04:16.560><c> sorry</c>

00:04:18.370 --> 00:04:18.380 align:start position:0%
now what you can do now is hope sorry
 

00:04:18.380 --> 00:04:21.950 align:start position:0%
now what you can do now is hope sorry
what<00:04:19.380><c> you</c><00:04:19.530><c> can</c><00:04:19.680><c> do</c><00:04:19.799><c> now</c><00:04:19.980><c> is</c><00:04:20.250><c> this</c><00:04:20.489><c> and</c><00:04:20.820><c> we</c><00:04:21.780><c> added</c>

00:04:21.950 --> 00:04:21.960 align:start position:0%
what you can do now is this and we added
 

00:04:21.960 --> 00:04:25.610 align:start position:0%
what you can do now is this and we added
structs<00:04:22.919><c> as</c><00:04:23.040><c> a</c><00:04:23.370><c> central</c><00:04:24.360><c> feature</c><00:04:24.540><c> to</c><00:04:25.200><c> the</c><00:04:25.320><c> ABI</c>

00:04:25.610 --> 00:04:25.620 align:start position:0%
structs as a central feature to the ABI
 

00:04:25.620 --> 00:04:27.590 align:start position:0%
structs as a central feature to the ABI
which<00:04:26.070><c> allows</c><00:04:26.340><c> you</c><00:04:26.490><c> to</c><00:04:26.640><c> actually</c><00:04:26.790><c> put</c><00:04:27.150><c> just</c>

00:04:27.590 --> 00:04:27.600 align:start position:0%
which allows you to actually put just
 

00:04:27.600 --> 00:04:29.420 align:start position:0%
which allows you to actually put just
we<00:04:27.660><c> passed</c><00:04:28.080><c> this</c><00:04:28.320><c> truck</c><00:04:28.590><c> from</c><00:04:28.770><c> JavaScript</c>

00:04:29.420 --> 00:04:29.430 align:start position:0%
we passed this truck from JavaScript
 

00:04:29.430 --> 00:04:32.000 align:start position:0%
we passed this truck from JavaScript
into<00:04:30.090><c> the</c><00:04:30.210><c> contract</c><00:04:30.690><c> and</c><00:04:30.900><c> remove</c><00:04:31.590><c> all</c><00:04:31.830><c> this</c>

00:04:32.000 --> 00:04:32.010 align:start position:0%
into the contract and remove all this
 

00:04:32.010 --> 00:04:35.240 align:start position:0%
into the contract and remove all this
these<00:04:32.970><c> weird</c><00:04:33.300><c> repetitions</c><00:04:33.870><c> and</c><00:04:34.590><c> of</c><00:04:35.070><c> course</c>

00:04:35.240 --> 00:04:35.250 align:start position:0%
these weird repetitions and of course
 

00:04:35.250 --> 00:04:38.000 align:start position:0%
these weird repetitions and of course
you<00:04:35.370><c> can</c><00:04:35.490><c> also</c><00:04:35.640><c> return</c><00:04:36.600><c> an</c><00:04:36.930><c> array</c><00:04:37.530><c> of</c><00:04:37.560><c> structs</c>

00:04:38.000 --> 00:04:38.010 align:start position:0%
you can also return an array of structs
 

00:04:38.010 --> 00:04:41.570 align:start position:0%
you can also return an array of structs
so<00:04:38.550><c> this</c><00:04:38.730><c> is</c><00:04:38.850><c> not</c><00:04:39.380><c> this</c><00:04:40.380><c> is</c><00:04:40.560><c> not</c><00:04:40.590><c> yet</c><00:04:41.280><c> available</c>

00:04:41.570 --> 00:04:41.580 align:start position:0%
so this is not this is not yet available
 

00:04:41.580 --> 00:04:49.040 align:start position:0%
so this is not this is not yet available
but<00:04:42.090><c> yeah</c><00:04:42.630><c> thanks</c><00:04:46.940><c> so</c><00:04:47.940><c> we</c><00:04:48.180><c> hope</c><00:04:48.330><c> to</c><00:04:48.660><c> get</c><00:04:48.810><c> that</c>

00:04:49.040 --> 00:04:49.050 align:start position:0%
but yeah thanks so we hope to get that
 

00:04:49.050 --> 00:04:52.630 align:start position:0%
but yeah thanks so we hope to get that
fully<00:04:49.260><c> functional</c><00:04:49.740><c> by</c><00:04:49.920><c> the</c><00:04:49.980><c> end</c><00:04:50.160><c> of</c><00:04:50.280><c> the</c><00:04:50.400><c> year</c>

00:04:52.630 --> 00:04:52.640 align:start position:0%
 
 

00:04:52.640 --> 00:04:57.260 align:start position:0%
 
so<00:04:53.640><c> and</c><00:04:54.000><c> the</c><00:04:54.540><c> way</c><00:04:54.720><c> we</c><00:04:55.620><c> the</c><00:04:56.520><c> way</c><00:04:56.610><c> what</c><00:04:56.790><c> this</c><00:04:56.940><c> this</c>

00:04:57.260 --> 00:04:57.270 align:start position:0%
so and the way we the way what this this
 

00:04:57.270 --> 00:05:00.170 align:start position:0%
so and the way we the way what this this
was<00:04:57.450><c> possible</c><00:04:57.810><c> while</c><00:04:57.990><c> was</c><00:04:58.430><c> through</c><00:04:59.430><c> a</c><00:04:59.460><c> change</c>

00:05:00.170 --> 00:05:00.180 align:start position:0%
was possible while was through a change
 

00:05:00.180 --> 00:05:02.660 align:start position:0%
was possible while was through a change
in<00:05:00.420><c> the</c><00:05:00.510><c> compiler</c><00:05:00.870><c> itself</c><00:05:01.140><c> so</c><00:05:01.560><c> we</c><00:05:01.770><c> we</c><00:05:02.460><c> could</c>

00:05:02.660 --> 00:05:02.670 align:start position:0%
in the compiler itself so we we could
 

00:05:02.670 --> 00:05:04.610 align:start position:0%
in the compiler itself so we we could
have<00:05:02.790><c> done</c><00:05:02.940><c> that</c><00:05:03.000><c> the</c><00:05:03.270><c> old</c><00:05:03.390><c> way</c><00:05:03.630><c> but</c><00:05:04.170><c> we</c>

00:05:04.610 --> 00:05:04.620 align:start position:0%
have done that the old way but we
 

00:05:04.620 --> 00:05:06.680 align:start position:0%
have done that the old way but we
decided<00:05:05.100><c> to</c><00:05:05.160><c> do</c><00:05:05.250><c> a</c><00:05:05.280><c> full</c><00:05:05.640><c> rewrite</c><00:05:06.030><c> of</c><00:05:06.060><c> the</c><00:05:06.270><c> ABI</c>

00:05:06.680 --> 00:05:06.690 align:start position:0%
decided to do a full rewrite of the ABI
 

00:05:06.690 --> 00:05:09.200 align:start position:0%
decided to do a full rewrite of the ABI
encoder<00:05:07.200><c> and</c><00:05:07.410><c> decoder</c><00:05:07.560><c> and</c><00:05:08.030><c> this</c><00:05:09.030><c> is</c><00:05:09.180><c> a</c>

00:05:09.200 --> 00:05:09.210 align:start position:0%
encoder and decoder and this is a
 

00:05:09.210 --> 00:05:11.540 align:start position:0%
encoder and decoder and this is a
snippet<00:05:09.570><c> of</c><00:05:09.690><c> the</c><00:05:09.870><c> solidity</c><00:05:10.620><c> code</c><00:05:11.100><c> generator</c>

00:05:11.540 --> 00:05:11.550 align:start position:0%
snippet of the solidity code generator
 

00:05:11.550 --> 00:05:15.910 align:start position:0%
snippet of the solidity code generator
and<00:05:11.940><c> how</c><00:05:12.600><c> it</c><00:05:12.750><c> looked</c><00:05:12.990><c> before</c><00:05:13.590><c> this</c><00:05:14.040><c> change</c>

00:05:15.910 --> 00:05:15.920 align:start position:0%
and how it looked before this change
 

00:05:15.920 --> 00:05:18.920 align:start position:0%
and how it looked before this change
yeah<00:05:16.920><c> this</c><00:05:17.130><c> also</c><00:05:17.490><c> this</c><00:05:17.640><c> is</c><00:05:17.790><c> also</c><00:05:17.970><c> really</c>

00:05:18.920 --> 00:05:18.930 align:start position:0%
yeah this also this is also really
 

00:05:18.930 --> 00:05:21.920 align:start position:0%
yeah this also this is also really
really<00:05:19.110><c> ugly</c><00:05:19.820><c> the</c><00:05:20.820><c> EVM</c><00:05:21.240><c> is</c><00:05:21.330><c> a</c><00:05:21.360><c> stack</c><00:05:21.600><c> machine</c>

00:05:21.920 --> 00:05:21.930 align:start position:0%
really ugly the EVM is a stack machine
 

00:05:21.930 --> 00:05:23.510 align:start position:0%
really ugly the EVM is a stack machine
and<00:05:22.140><c> because</c><00:05:22.380><c> of</c><00:05:22.530><c> that</c><00:05:22.680><c> you</c><00:05:22.890><c> have</c><00:05:23.040><c> these</c><00:05:23.190><c> this</c>

00:05:23.510 --> 00:05:23.520 align:start position:0%
and because of that you have these this
 

00:05:23.520 --> 00:05:29.600 align:start position:0%
and because of that you have these this
pop<00:05:24.270><c> and</c><00:05:24.320><c> to</c><00:05:25.320><c> operations</c><00:05:26.160><c> and</c><00:05:27.920><c> in</c><00:05:28.920><c> the</c><00:05:29.370><c> code</c>

00:05:29.600 --> 00:05:29.610 align:start position:0%
pop and to operations and in the code
 

00:05:29.610 --> 00:05:30.860 align:start position:0%
pop and to operations and in the code
Ranieri<00:05:29.940><c> you</c><00:05:30.030><c> constantly</c><00:05:30.390><c> have</c><00:05:30.540><c> to</c><00:05:30.570><c> keep</c>

00:05:30.860 --> 00:05:30.870 align:start position:0%
Ranieri you constantly have to keep
 

00:05:30.870 --> 00:05:33.110 align:start position:0%
Ranieri you constantly have to keep
track<00:05:31.110><c> which</c><00:05:31.380><c> variable</c><00:05:31.920><c> is</c><00:05:32.010><c> where</c><00:05:32.400><c> on</c><00:05:32.730><c> the</c>

00:05:33.110 --> 00:05:33.120 align:start position:0%
track which variable is where on the
 

00:05:33.120 --> 00:05:34.460 align:start position:0%
track which variable is where on the
stack<00:05:33.360><c> and</c><00:05:33.390><c> because</c><00:05:33.780><c> of</c><00:05:33.870><c> that</c><00:05:33.990><c> we</c><00:05:34.140><c> have</c><00:05:34.290><c> these</c>

00:05:34.460 --> 00:05:34.470 align:start position:0%
stack and because of that we have these
 

00:05:34.470 --> 00:05:36.140 align:start position:0%
stack and because of that we have these
comments<00:05:35.430><c> and</c><00:05:35.550><c> it's</c><00:05:35.700><c> really</c><00:05:36.000><c> really</c>

00:05:36.140 --> 00:05:36.150 align:start position:0%
comments and it's really really
 

00:05:36.150 --> 00:05:37.640 align:start position:0%
comments and it's really really
complicated<00:05:36.720><c> to</c><00:05:36.750><c> understand</c><00:05:37.170><c> what</c><00:05:37.320><c> this</c><00:05:37.440><c> code</c>

00:05:37.640 --> 00:05:37.650 align:start position:0%
complicated to understand what this code
 

00:05:37.650 --> 00:05:41.420 align:start position:0%
complicated to understand what this code
does<00:05:37.680><c> and</c><00:05:38.130><c> also</c><00:05:39.470><c> complicated</c><00:05:40.470><c> to</c><00:05:40.560><c> write</c><00:05:40.710><c> new</c>

00:05:41.420 --> 00:05:41.430 align:start position:0%
does and also complicated to write new
 

00:05:41.430 --> 00:05:51.640 align:start position:0%
does and also complicated to write new
code<00:05:43.100><c> and</c><00:05:46.130><c> this</c><00:05:47.130><c> is</c><00:05:47.340><c> how</c><00:05:48.120><c> it</c><00:05:48.270><c> looks</c><00:05:48.480><c> now</c><00:05:48.570><c> and</c><00:05:50.090><c> it</c>

00:05:51.640 --> 00:05:51.650 align:start position:0%
code and this is how it looks now and it
 

00:05:51.650 --> 00:05:54.530 align:start position:0%
code and this is how it looks now and it
leverages<00:05:52.650><c> a</c><00:05:53.010><c> new</c><00:05:53.550><c> intermediate</c><00:05:54.090><c> language</c><00:05:54.180><c> we</c>

00:05:54.530 --> 00:05:54.540 align:start position:0%
leverages a new intermediate language we
 

00:05:54.540 --> 00:05:57.170 align:start position:0%
leverages a new intermediate language we
introduced<00:05:54.960><c> called</c><00:05:55.170><c> Yulia</c><00:05:55.910><c> Alex</c><00:05:56.910><c> talked</c>

00:05:57.170 --> 00:05:57.180 align:start position:0%
introduced called Yulia Alex talked
 

00:05:57.180 --> 00:05:59.000 align:start position:0%
introduced called Yulia Alex talked
about<00:05:57.420><c> that</c><00:05:57.540><c> I</c><00:05:57.600><c> think</c><00:05:57.800><c> yesterday</c><00:05:58.800><c> or</c><00:05:58.920><c> the</c><00:05:58.980><c> day</c>

00:05:59.000 --> 00:05:59.010 align:start position:0%
about that I think yesterday or the day
 

00:05:59.010 --> 00:06:01.570 align:start position:0%
about that I think yesterday or the day
before<00:05:59.100><c> yesterday</c><00:05:59.370><c> so</c><00:06:00.090><c> I</c><00:06:00.120><c> will</c><00:06:00.330><c> not</c><00:06:00.450><c> go</c><00:06:00.720><c> to</c>

00:06:01.570 --> 00:06:01.580 align:start position:0%
before yesterday so I will not go to
 

00:06:01.580 --> 00:06:05.630 align:start position:0%
before yesterday so I will not go to
into<00:06:02.580><c> 10th</c><00:06:02.760><c> about</c><00:06:03.030><c> that</c><00:06:03.210><c> but</c><00:06:04.080><c> you</c><00:06:05.070><c> see</c><00:06:05.310><c> this</c><00:06:05.460><c> is</c>

00:06:05.630 --> 00:06:05.640 align:start position:0%
into 10th about that but you see this is
 

00:06:05.640 --> 00:06:09.830 align:start position:0%
into 10th about that but you see this is
really<00:06:06.210><c> really</c><00:06:06.590><c> readable</c><00:06:07.670><c> it</c><00:06:08.670><c> has</c><00:06:09.030><c> variables</c>

00:06:09.830 --> 00:06:09.840 align:start position:0%
really really readable it has variables
 

00:06:09.840 --> 00:06:14.300 align:start position:0%
really really readable it has variables
you<00:06:10.500><c> know</c><00:06:10.940><c> what</c><00:06:11.940><c> happens</c><00:06:12.300><c> you</c><00:06:12.390><c> can</c><00:06:12.980><c> use</c><00:06:13.980><c> names</c>

00:06:14.300 --> 00:06:14.310 align:start position:0%
you know what happens you can use names
 

00:06:14.310 --> 00:06:17.990 align:start position:0%
you know what happens you can use names
we<00:06:15.240><c> have</c><00:06:15.360><c> for</c><00:06:15.600><c> loops</c><00:06:15.810><c> and</c><00:06:16.050><c> so</c><00:06:16.470><c> on</c><00:06:16.590><c> and</c><00:06:16.940><c> what</c><00:06:17.940><c> you</c>

00:06:17.990 --> 00:06:18.000 align:start position:0%
we have for loops and so on and what you
 

00:06:18.000 --> 00:06:20.020 align:start position:0%
we have for loops and so on and what you
also<00:06:18.150><c> see</c><00:06:18.240><c> is</c><00:06:18.360><c> you</c><00:06:18.930><c> have</c><00:06:19.080><c> these</c><00:06:19.230><c> angle</c>

00:06:20.020 --> 00:06:20.030 align:start position:0%
also see is you have these angle
 

00:06:20.030 --> 00:06:23.990 align:start position:0%
also see is you have these angle
brackets<00:06:21.030><c> here</c><00:06:21.750><c> and</c><00:06:21.930><c> this</c><00:06:22.800><c> is</c><00:06:22.920><c> because</c><00:06:23.280><c> this</c>

00:06:23.990 --> 00:06:24.000 align:start position:0%
brackets here and this is because this
 

00:06:24.000 --> 00:06:26.810 align:start position:0%
brackets here and this is because this
is<00:06:24.150><c> an</c><00:06:24.270><c> intermediate</c><00:06:24.480><c> language</c><00:06:25.550><c> mixed</c><00:06:26.550><c> with</c><00:06:26.790><c> a</c>

00:06:26.810 --> 00:06:26.820 align:start position:0%
is an intermediate language mixed with a
 

00:06:26.820 --> 00:06:29.300 align:start position:0%
is an intermediate language mixed with a
very<00:06:27.030><c> very</c><00:06:27.510><c> simple</c><00:06:27.990><c> string</c><00:06:28.770><c> templating</c>

00:06:29.300 --> 00:06:29.310 align:start position:0%
very very simple string templating
 

00:06:29.310 --> 00:06:32.810 align:start position:0%
very very simple string templating
engine<00:06:29.640><c> to</c><00:06:30.180><c> make</c><00:06:30.360><c> it</c><00:06:30.510><c> more</c><00:06:30.660><c> flexible</c><00:06:31.730><c> what</c><00:06:32.730><c> you</c>

00:06:32.810 --> 00:06:32.820 align:start position:0%
engine to make it more flexible what you
 

00:06:32.820 --> 00:06:37.330 align:start position:0%
engine to make it more flexible what you
see<00:06:32.970><c> here</c><00:06:33.210><c> is</c><00:06:33.390><c> the</c><00:06:33.780><c> full</c><00:06:35.270><c> function</c><00:06:36.270><c> to</c><00:06:36.450><c> do</c><00:06:36.600><c> any</c>

00:06:37.330 --> 00:06:37.340 align:start position:0%
see here is the full function to do any
 

00:06:37.340 --> 00:06:40.909 align:start position:0%
see here is the full function to do any
encoding<00:06:38.340><c> of</c><00:06:38.460><c> an</c><00:06:38.850><c> of</c><00:06:39.330><c> an</c><00:06:39.690><c> array</c><00:06:39.930><c> into</c><00:06:40.290><c> the</c><00:06:40.620><c> the</c>

00:06:40.909 --> 00:06:40.919 align:start position:0%
encoding of an of an array into the the
 

00:06:40.919 --> 00:06:41.570 align:start position:0%
encoding of an of an array into the the
ABI

00:06:41.570 --> 00:06:41.580 align:start position:0%
ABI
 

00:06:41.580 --> 00:06:44.089 align:start position:0%
ABI
so<00:06:42.120><c> it</c><00:06:42.270><c> does</c><00:06:42.599><c> handle</c><00:06:42.960><c> memory</c><00:06:43.349><c> arrays</c><00:06:43.620><c> call</c><00:06:43.919><c> it</c>

00:06:44.089 --> 00:06:44.099 align:start position:0%
so it does handle memory arrays call it
 

00:06:44.099 --> 00:06:47.749 align:start position:0%
so it does handle memory arrays call it
arrays<00:06:44.400><c> storage</c><00:06:44.909><c> arrays</c><00:06:46.430><c> arrays</c><00:06:47.430><c> of</c><00:06:47.460><c> arrays</c>

00:06:47.749 --> 00:06:47.759 align:start position:0%
arrays storage arrays arrays of arrays
 

00:06:47.759 --> 00:06:49.879 align:start position:0%
arrays storage arrays arrays of arrays
arrays<00:06:48.389><c> of</c><00:06:48.539><c> constant</c><00:06:48.990><c> length</c><00:06:49.139><c> arrays</c><00:06:49.650><c> of</c>

00:06:49.879 --> 00:06:49.889 align:start position:0%
arrays of constant length arrays of
 

00:06:49.889 --> 00:06:52.670 align:start position:0%
arrays of constant length arrays of
dynamic<00:06:50.370><c> length</c><00:06:50.520><c> and</c><00:06:50.729><c> so</c><00:06:50.849><c> on</c><00:06:50.969><c> and</c><00:06:51.469><c> the</c><00:06:52.469><c> way</c><00:06:52.620><c> it</c>

00:06:52.670 --> 00:06:52.680 align:start position:0%
dynamic length and so on and the way it
 

00:06:52.680 --> 00:06:54.050 align:start position:0%
dynamic length and so on and the way it
works<00:06:52.889><c> is</c><00:06:53.039><c> that</c><00:06:53.189><c> for</c><00:06:53.340><c> example</c><00:06:53.370><c> here</c><00:06:53.849><c> at</c><00:06:53.939><c> the</c>

00:06:54.050 --> 00:06:54.060 align:start position:0%
works is that for example here at the
 

00:06:54.060 --> 00:06:57.939 align:start position:0%
works is that for example here at the
top<00:06:54.270><c> we</c><00:06:54.629><c> have</c><00:06:54.659><c> length</c><00:06:55.259><c> equals</c><00:06:55.770><c> length</c><00:06:56.520><c> fun</c><00:06:56.849><c> and</c>

00:06:57.939 --> 00:06:57.949 align:start position:0%
top we have length equals length fun and
 

00:06:57.949 --> 00:07:00.439 align:start position:0%
top we have length equals length fun and
at<00:06:58.949><c> the</c><00:06:59.219><c> time</c><00:06:59.430><c> of</c><00:06:59.460><c> compilation</c><00:06:59.729><c> this</c><00:07:00.240><c> length</c>

00:07:00.439 --> 00:07:00.449 align:start position:0%
at the time of compilation this length
 

00:07:00.449 --> 00:07:02.330 align:start position:0%
at the time of compilation this length
furnace<00:07:00.780><c> report</c><00:07:01.080><c> is</c><00:07:01.199><c> is</c><00:07:01.469><c> replaced</c><00:07:01.949><c> by</c><00:07:02.159><c> the</c>

00:07:02.330 --> 00:07:02.340 align:start position:0%
furnace report is is replaced by the
 

00:07:02.340 --> 00:07:03.950 align:start position:0%
furnace report is is replaced by the
name<00:07:02.580><c> of</c><00:07:02.610><c> the</c><00:07:02.849><c> actual</c><00:07:02.969><c> function</c><00:07:03.509><c> to</c><00:07:03.629><c> retrieve</c>

00:07:03.950 --> 00:07:03.960 align:start position:0%
name of the actual function to retrieve
 

00:07:03.960 --> 00:07:05.270 align:start position:0%
name of the actual function to retrieve
the<00:07:04.139><c> length</c><00:07:04.319><c> of</c><00:07:04.469><c> the</c><00:07:04.590><c> array</c><00:07:04.710><c> which</c><00:07:05.009><c> is</c><00:07:05.189><c> of</c>

00:07:05.270 --> 00:07:05.280 align:start position:0%
the length of the array which is of
 

00:07:05.280 --> 00:07:07.219 align:start position:0%
the length of the array which is of
course<00:07:05.550><c> different</c><00:07:05.789><c> for</c><00:07:06.150><c> static</c><00:07:06.780><c> resized</c><00:07:07.050><c> and</c>

00:07:07.219 --> 00:07:07.229 align:start position:0%
course different for static resized and
 

00:07:07.229 --> 00:07:17.290 align:start position:0%
course different for static resized and
dynamically<00:07:07.590><c> sized</c><00:07:07.860><c> arrays</c><00:07:13.940><c> okay</c><00:07:14.940><c> and</c><00:07:15.800><c> a</c>

00:07:17.290 --> 00:07:17.300 align:start position:0%
dynamically sized arrays okay and a
 

00:07:17.300 --> 00:07:19.520 align:start position:0%
dynamically sized arrays okay and a
language<00:07:18.300><c> becomes</c><00:07:18.900><c> more</c><00:07:19.110><c> and</c><00:07:19.229><c> more</c><00:07:19.319><c> useful</c>

00:07:19.520 --> 00:07:19.530 align:start position:0%
language becomes more and more useful
 

00:07:19.530 --> 00:07:21.529 align:start position:0%
language becomes more and more useful
the<00:07:20.190><c> better</c><00:07:20.370><c> tools</c><00:07:20.639><c> are</c><00:07:20.879><c> available</c><00:07:20.969><c> for</c><00:07:21.330><c> that</c>

00:07:21.529 --> 00:07:21.539 align:start position:0%
the better tools are available for that
 

00:07:21.539 --> 00:07:23.930 align:start position:0%
the better tools are available for that
we<00:07:21.690><c> already</c><00:07:21.810><c> see</c><00:07:22.110><c> that</c><00:07:22.289><c> by</c><00:07:22.620><c> in</c><00:07:23.069><c> the</c><00:07:23.400><c> questions</c>

00:07:23.930 --> 00:07:23.940 align:start position:0%
we already see that by in the questions
 

00:07:23.940 --> 00:07:27.399 align:start position:0%
we already see that by in the questions
that<00:07:24.000><c> were</c><00:07:24.120><c> asked</c><00:07:24.419><c> in</c><00:07:24.449><c> the</c><00:07:24.569><c> previous</c><00:07:24.719><c> talk</c>

00:07:27.399 --> 00:07:27.409 align:start position:0%
 
 

00:07:27.409 --> 00:07:30.170 align:start position:0%
 
remix<00:07:28.409><c> got</c><00:07:28.710><c> gigantic</c><00:07:29.280><c> updates</c><00:07:29.669><c> I</c><00:07:29.849><c> think</c><00:07:30.030><c> yang</c>

00:07:30.170 --> 00:07:30.180 align:start position:0%
remix got gigantic updates I think yang
 

00:07:30.180 --> 00:07:34.040 align:start position:0%
remix got gigantic updates I think yang
will<00:07:30.360><c> talk</c><00:07:30.599><c> about</c><00:07:30.870><c> that</c><00:07:31.080><c> later</c><00:07:31.710><c> today</c><00:07:32.810><c> we</c><00:07:33.810><c> now</c>

00:07:34.040 --> 00:07:34.050 align:start position:0%
will talk about that later today we now
 

00:07:34.050 --> 00:07:39.290 align:start position:0%
will talk about that later today we now
can<00:07:35.210><c> track</c><00:07:36.210><c> variables</c><00:07:36.779><c> have</c><00:07:36.960><c> breakpoints</c><00:07:38.300><c> see</c>

00:07:39.290 --> 00:07:39.300 align:start position:0%
can track variables have breakpoints see
 

00:07:39.300 --> 00:07:42.110 align:start position:0%
can track variables have breakpoints see
references<00:07:40.259><c> of</c><00:07:40.800><c> variables</c><00:07:41.370><c> and</c><00:07:41.550><c> I</c><00:07:41.699><c> think</c><00:07:41.879><c> soon</c>

00:07:42.110 --> 00:07:42.120 align:start position:0%
references of variables and I think soon
 

00:07:42.120 --> 00:07:46.369 align:start position:0%
references of variables and I think soon
can<00:07:42.330><c> also</c><00:07:42.479><c> rename</c><00:07:42.810><c> variables</c><00:07:42.870><c> and</c><00:07:43.620><c> so</c><00:07:43.770><c> on</c><00:07:45.379><c> we</c>

00:07:46.369 --> 00:07:46.379 align:start position:0%
can also rename variables and so on we
 

00:07:46.379 --> 00:07:49.760 align:start position:0%
can also rename variables and so on we
have<00:07:46.590><c> an</c><00:07:46.800><c> way</c><00:07:47.400><c> to</c><00:07:47.460><c> export</c><00:07:48.449><c> the</c><00:07:48.750><c> ast</c><00:07:49.469><c> which</c><00:07:49.620><c> is</c>

00:07:49.760 --> 00:07:49.770 align:start position:0%
have an way to export the ast which is
 

00:07:49.770 --> 00:07:51.589 align:start position:0%
have an way to export the ast which is
the<00:07:49.889><c> result</c><00:07:50.250><c> of</c><00:07:50.370><c> the</c><00:07:50.520><c> of</c><00:07:50.849><c> the</c><00:07:51.000><c> parsing</c><00:07:51.389><c> step</c>

00:07:51.589 --> 00:07:51.599 align:start position:0%
the result of the of the parsing step
 

00:07:51.599 --> 00:07:54.980 align:start position:0%
the result of the of the parsing step
and<00:07:51.990><c> these</c><00:07:52.469><c> this</c><00:07:52.949><c> allows</c><00:07:53.360><c> many</c><00:07:54.360><c> new</c><00:07:54.539><c> features</c>

00:07:54.980 --> 00:07:54.990 align:start position:0%
and these this allows many new features
 

00:07:54.990 --> 00:08:00.589 align:start position:0%
and these this allows many new features
and<00:07:55.199><c> one</c><00:07:55.409><c> of</c><00:07:55.500><c> them</c><00:07:55.680><c> is</c><00:07:55.949><c> a</c><00:07:57.589><c> tool</c><00:07:58.589><c> to</c><00:07:59.009><c> do</c><00:07:59.599><c> code</c>

00:08:00.589 --> 00:08:00.599 align:start position:0%
and one of them is a tool to do code
 

00:08:00.599 --> 00:08:03.800 align:start position:0%
and one of them is a tool to do code
coverage<00:08:00.629><c> not</c><00:08:01.319><c> based</c><00:08:01.589><c> on</c><00:08:02.419><c> syntax</c><00:08:03.419><c> not</c><00:08:03.599><c> just</c>

00:08:03.800 --> 00:08:03.810 align:start position:0%
coverage not based on syntax not just
 

00:08:03.810 --> 00:08:05.420 align:start position:0%
coverage not based on syntax not just
based<00:08:03.990><c> on</c><00:08:04.080><c> lines</c><00:08:04.319><c> but</c><00:08:04.560><c> on</c><00:08:04.680><c> semantics</c><00:08:05.159><c> so</c><00:08:05.279><c> for</c>

00:08:05.420 --> 00:08:05.430 align:start position:0%
based on lines but on semantics so for
 

00:08:05.430 --> 00:08:07.809 align:start position:0%
based on lines but on semantics so for
example<00:08:05.759><c> is</c><00:08:05.940><c> a</c><00:08:05.969><c> less</c><00:08:06.539><c> than</c><00:08:06.750><c> operator</c><00:08:07.020><c> actually</c>

00:08:07.809 --> 00:08:07.819 align:start position:0%
example is a less than operator actually
 

00:08:07.819 --> 00:08:13.040 align:start position:0%
example is a less than operator actually
tested<00:08:08.819><c> to</c><00:08:09.000><c> do</c><00:08:09.300><c> what</c><00:08:09.509><c> it</c><00:08:09.629><c> does</c><00:08:09.810><c> and</c><00:08:11.779><c> then</c><00:08:12.779><c> a</c>

00:08:13.040 --> 00:08:13.050 align:start position:0%
tested to do what it does and then a
 

00:08:13.050 --> 00:08:16.399 align:start position:0%
tested to do what it does and then a
standard<00:08:13.440><c> JSON</c><00:08:13.740><c> i/o</c><00:08:14.039><c> this</c><00:08:14.400><c> is</c><00:08:14.610><c> a</c><00:08:15.029><c> way</c><00:08:15.750><c> to</c><00:08:15.779><c> get</c>

00:08:16.399 --> 00:08:16.409 align:start position:0%
standard JSON i/o this is a way to get
 

00:08:16.409 --> 00:08:17.269 align:start position:0%
standard JSON i/o this is a way to get
more<00:08:16.589><c> fine</c><00:08:16.860><c> control</c>

00:08:17.269 --> 00:08:17.279 align:start position:0%
more fine control
 

00:08:17.279 --> 00:08:19.490 align:start position:0%
more fine control
fine<00:08:17.580><c> fine</c><00:08:18.029><c> grained</c><00:08:18.270><c> control</c><00:08:18.300><c> about</c><00:08:19.259><c> the</c>

00:08:19.490 --> 00:08:19.500 align:start position:0%
fine fine grained control about the
 

00:08:19.500 --> 00:08:24.740 align:start position:0%
fine fine grained control about the
settings<00:08:20.430><c> of</c><00:08:20.610><c> the</c><00:08:20.759><c> compiler</c><00:08:23.300><c> yeah</c><00:08:24.300><c> then</c><00:08:24.509><c> I</c>

00:08:24.740 --> 00:08:24.750 align:start position:0%
settings of the compiler yeah then I
 

00:08:24.750 --> 00:08:27.350 align:start position:0%
settings of the compiler yeah then I
have<00:08:25.229><c> a</c><00:08:25.259><c> very</c><00:08:25.860><c> special</c><00:08:26.460><c> announcement</c><00:08:26.520><c> to</c><00:08:27.029><c> make</c>

00:08:27.350 --> 00:08:27.360 align:start position:0%
have a very special announcement to make
 

00:08:27.360 --> 00:08:31.760 align:start position:0%
have a very special announcement to make
and<00:08:27.990><c> this</c><00:08:28.800><c> is</c><00:08:29.009><c> that</c><00:08:29.599><c> the</c><00:08:30.770><c> solidity</c>

00:08:31.760 --> 00:08:31.770 align:start position:0%
and this is that the solidity
 

00:08:31.770 --> 00:08:34.310 align:start position:0%
and this is that the solidity
documentation<00:08:32.610><c> that</c><00:08:32.640><c> we</c><00:08:33.060><c> only</c><00:08:33.810><c> have</c><00:08:34.140><c> in</c>

00:08:34.310 --> 00:08:34.320 align:start position:0%
documentation that we only have in
 

00:08:34.320 --> 00:08:36.500 align:start position:0%
documentation that we only have in
English<00:08:34.560><c> for</c><00:08:34.740><c> now</c><00:08:34.919><c> is</c><00:08:35.190><c> now</c><00:08:35.399><c> also</c><00:08:35.669><c> available</c><00:08:36.029><c> in</c>

00:08:36.500 --> 00:08:36.510 align:start position:0%
English for now is now also available in
 

00:08:36.510 --> 00:08:38.930 align:start position:0%
English for now is now also available in
Spanish<00:08:36.930><c> so</c><00:08:37.110><c> please</c><00:08:37.349><c> give</c><00:08:37.649><c> a</c><00:08:37.800><c> big</c><00:08:38.640><c> round</c><00:08:38.669><c> of</c>

00:08:38.930 --> 00:08:38.940 align:start position:0%
Spanish so please give a big round of
 

00:08:38.940 --> 00:08:47.300 align:start position:0%
Spanish so please give a big round of
applause<00:08:39.240><c> to</c><00:08:39.269><c> these</c><00:08:39.719><c> five</c><00:08:39.990><c> people</c><00:08:40.229><c> who</c>

00:08:47.300 --> 00:08:47.310 align:start position:0%
 
 

00:08:47.310 --> 00:08:49.530 align:start position:0%
 
these<00:08:48.310><c> five</c><00:08:48.670><c> people</c><00:08:48.850><c> who</c><00:08:48.970><c> did</c><00:08:49.120><c> that</c><00:08:49.240><c> in</c><00:08:49.360><c> their</c>

00:08:49.530 --> 00:08:49.540 align:start position:0%
these five people who did that in their
 

00:08:49.540 --> 00:08:53.010 align:start position:0%
these five people who did that in their
free<00:08:49.750><c> time</c><00:08:49.860><c> just</c><00:08:50.860><c> as</c><00:08:51.790><c> voluntary</c><00:08:52.270><c> contributors</c>

00:08:53.010 --> 00:08:53.020 align:start position:0%
free time just as voluntary contributors
 

00:08:53.020 --> 00:08:56.310 align:start position:0%
free time just as voluntary contributors
I<00:08:54.120><c> think</c><00:08:55.120><c> this</c><00:08:55.240><c> is</c><00:08:55.390><c> really</c><00:08:55.600><c> important</c><00:08:56.050><c> to</c><00:08:56.080><c> make</c>

00:08:56.310 --> 00:08:56.320 align:start position:0%
I think this is really important to make
 

00:08:56.320 --> 00:08:59.360 align:start position:0%
I think this is really important to make
if<00:08:56.560><c> you</c><00:08:56.680><c> remix</c><00:08:56.890><c> esse</c><00:08:57.160><c> below</c><00:08:57.400><c> the</c><00:08:57.610><c> world</c><00:08:57.820><c> and</c>

00:08:59.360 --> 00:08:59.370 align:start position:0%
if you remix esse below the world and
 

00:08:59.370 --> 00:09:02.730 align:start position:0%
if you remix esse below the world and
languages<00:09:00.370><c> like</c><00:09:00.610><c> so</c><00:09:01.060><c> like</c><00:09:01.900><c> like</c><00:09:02.080><c> Chinese</c><00:09:02.470><c> or</c>

00:09:02.730 --> 00:09:02.740 align:start position:0%
languages like so like like Chinese or
 

00:09:02.740 --> 00:09:05.160 align:start position:0%
languages like so like like Chinese or
Russian<00:09:02.770><c> should</c><00:09:03.490><c> also</c><00:09:04.000><c> have</c><00:09:04.420><c> a</c><00:09:04.450><c> their</c><00:09:05.050><c> own</c>

00:09:05.160 --> 00:09:05.170 align:start position:0%
Russian should also have a their own
 

00:09:05.170 --> 00:09:08.130 align:start position:0%
Russian should also have a their own
translation<00:09:05.650><c> of</c><00:09:05.710><c> the</c><00:09:05.830><c> documentation</c><00:09:06.460><c> and</c><00:09:07.140><c> I</c>

00:09:08.130 --> 00:09:08.140 align:start position:0%
translation of the documentation and I
 

00:09:08.140 --> 00:09:10.970 align:start position:0%
translation of the documentation and I
want<00:09:08.380><c> to</c><00:09:08.500><c> spend</c><00:09:08.740><c> the</c><00:09:09.040><c> rest</c><00:09:09.520><c> of</c><00:09:10.090><c> the</c><00:09:10.210><c> talk</c><00:09:10.420><c> on</c>

00:09:10.970 --> 00:09:10.980 align:start position:0%
want to spend the rest of the talk on
 

00:09:10.980 --> 00:09:15.860 align:start position:0%
want to spend the rest of the talk on
formal<00:09:11.980><c> verification</c><00:09:12.130><c> of</c><00:09:12.730><c> solidity</c><00:09:13.180><c> and</c><00:09:13.890><c> I</c>

00:09:15.860 --> 00:09:15.870 align:start position:0%
formal verification of solidity and I
 

00:09:15.870 --> 00:09:19.080 align:start position:0%
formal verification of solidity and I
think<00:09:16.870><c> I</c><00:09:17.050><c> showed</c><00:09:17.320><c> this</c><00:09:17.530><c> slide</c><00:09:17.590><c> to</c><00:09:18.160><c> you</c><00:09:18.370><c> last</c>

00:09:19.080 --> 00:09:19.090 align:start position:0%
think I showed this slide to you last
 

00:09:19.090 --> 00:09:20.330 align:start position:0%
think I showed this slide to you last
year<00:09:19.300><c> in</c><00:09:19.540><c> Shanghai</c>

00:09:20.330 --> 00:09:20.340 align:start position:0%
year in Shanghai
 

00:09:20.340 --> 00:09:24.870 align:start position:0%
year in Shanghai
this<00:09:21.340><c> is</c><00:09:21.550><c> a</c><00:09:21.790><c> smart</c><00:09:22.600><c> contract</c><00:09:22.810><c> and</c><00:09:23.670><c> it</c><00:09:24.670><c> has</c>

00:09:24.870 --> 00:09:24.880 align:start position:0%
this is a smart contract and it has
 

00:09:24.880 --> 00:09:28.950 align:start position:0%
this is a smart contract and it has
comments<00:09:26.010><c> which</c><00:09:27.010><c> allow</c><00:09:27.370><c> a</c><00:09:27.790><c> formal</c><00:09:28.390><c> proof</c><00:09:28.600><c> that</c>

00:09:28.950 --> 00:09:28.960 align:start position:0%
comments which allow a formal proof that
 

00:09:28.960 --> 00:09:31.410 align:start position:0%
comments which allow a formal proof that
the<00:09:29.590><c> the</c><00:09:30.190><c> some</c><00:09:30.400><c> of</c><00:09:30.430><c> the</c><00:09:30.640><c> balances</c><00:09:31.120><c> in</c><00:09:31.150><c> this</c>

00:09:31.410 --> 00:09:31.420 align:start position:0%
the the some of the balances in this
 

00:09:31.420 --> 00:09:35.490 align:start position:0%
the the some of the balances in this
token<00:09:31.950><c> contract</c><00:09:32.950><c> never</c><00:09:33.700><c> changes</c><00:09:34.180><c> and</c><00:09:34.570><c> the</c><00:09:35.320><c> way</c>

00:09:35.490 --> 00:09:35.500 align:start position:0%
token contract never changes and the way
 

00:09:35.500 --> 00:09:37.170 align:start position:0%
token contract never changes and the way
it<00:09:35.560><c> works</c><00:09:35.770><c> is</c><00:09:36.040><c> that</c><00:09:36.070><c> the</c><00:09:36.790><c> smart</c><00:09:37.030><c> contract</c>

00:09:37.170 --> 00:09:37.180 align:start position:0%
it works is that the smart contract
 

00:09:37.180 --> 00:09:39.240 align:start position:0%
it works is that the smart contract
kannst<00:09:37.630><c> gets</c><00:09:37.900><c> translated</c><00:09:38.230><c> by</c><00:09:38.830><c> the</c><00:09:38.860><c> compiler</c>

00:09:39.240 --> 00:09:39.250 align:start position:0%
kannst gets translated by the compiler
 

00:09:39.250 --> 00:09:42.300 align:start position:0%
kannst gets translated by the compiler
into<00:09:39.550><c> a</c><00:09:39.700><c> language</c><00:09:40.210><c> called</c><00:09:40.390><c> y3</c><00:09:40.900><c> and</c><00:09:41.110><c> it</c><00:09:41.860><c> mixes</c>

00:09:42.300 --> 00:09:42.310 align:start position:0%
into a language called y3 and it mixes
 

00:09:42.310 --> 00:09:44.370 align:start position:0%
into a language called y3 and it mixes
this<00:09:42.550><c> translation</c><00:09:43.300><c> with</c><00:09:43.450><c> the</c><00:09:43.720><c> with</c><00:09:44.260><c> the</c>

00:09:44.370 --> 00:09:44.380 align:start position:0%
this translation with the with the
 

00:09:44.380 --> 00:09:49.080 align:start position:0%
this translation with the with the
comments<00:09:44.770><c> you</c><00:09:44.860><c> have</c><00:09:44.890><c> here</c><00:09:45.490><c> and</c><00:09:47.820><c> then</c><00:09:48.820><c> you</c><00:09:48.940><c> run</c>

00:09:49.080 --> 00:09:49.090 align:start position:0%
comments you have here and then you run
 

00:09:49.090 --> 00:09:51.330 align:start position:0%
comments you have here and then you run
an<00:09:49.210><c> external</c><00:09:49.660><c> tool</c><00:09:49.810><c> on</c><00:09:49.990><c> that</c><00:09:50.170><c> to</c><00:09:50.500><c> create</c><00:09:51.220><c> the</c>

00:09:51.330 --> 00:09:51.340 align:start position:0%
an external tool on that to create the
 

00:09:51.340 --> 00:09:54.150 align:start position:0%
an external tool on that to create the
proof<00:09:51.550><c> that</c><00:09:51.790><c> the</c><00:09:52.150><c> balances</c><00:09:52.630><c> are</c><00:09:53.530><c> constant</c><00:09:54.100><c> the</c>

00:09:54.150 --> 00:09:54.160 align:start position:0%
proof that the balances are constant the
 

00:09:54.160 --> 00:09:56.670 align:start position:0%
proof that the balances are constant the
sum<00:09:54.310><c> of</c><00:09:54.340><c> the</c><00:09:54.490><c> balances</c><00:09:54.820><c> are</c><00:09:54.940><c> constant</c><00:09:55.680><c> but</c>

00:09:56.670 --> 00:09:56.680 align:start position:0%
sum of the balances are constant but
 

00:09:56.680 --> 00:10:00.870 align:start position:0%
sum of the balances are constant but
what<00:09:56.830><c> you</c><00:09:56.890><c> see</c><00:09:57.040><c> is</c><00:09:57.100><c> that</c><00:09:59.160><c> there</c><00:10:00.160><c> are</c><00:10:00.310><c> almost</c><00:10:00.550><c> as</c>

00:10:00.870 --> 00:10:00.880 align:start position:0%
what you see is that there are almost as
 

00:10:00.880 --> 00:10:03.870 align:start position:0%
what you see is that there are almost as
many<00:10:00.960><c> lines</c><00:10:01.960><c> of</c><00:10:02.320><c> comments</c><00:10:03.190><c> in</c><00:10:03.340><c> this</c><00:10:03.430><c> code</c><00:10:03.670><c> as</c>

00:10:03.870 --> 00:10:03.880 align:start position:0%
many lines of comments in this code as
 

00:10:03.880 --> 00:10:07.760 align:start position:0%
many lines of comments in this code as
there<00:10:04.120><c> is</c><00:10:04.270><c> code</c><00:10:04.540><c> and</c><00:10:04.860><c> you</c><00:10:05.860><c> also</c><00:10:05.980><c> see</c><00:10:06.160><c> that</c><00:10:06.310><c> the</c>

00:10:07.760 --> 00:10:07.770 align:start position:0%
there is code and you also see that the
 

00:10:07.770 --> 00:10:10.500 align:start position:0%
there is code and you also see that the
these<00:10:08.770><c> comments</c><00:10:09.250><c> use</c><00:10:09.520><c> a</c><00:10:09.820><c> language</c><00:10:10.270><c> that</c><00:10:10.360><c> is</c>

00:10:10.500 --> 00:10:10.510 align:start position:0%
these comments use a language that is
 

00:10:10.510 --> 00:10:13.410 align:start position:0%
these comments use a language that is
slightly<00:10:10.750><c> different</c><00:10:11.170><c> from</c><00:10:11.440><c> solidity</c><00:10:11.860><c> so</c><00:10:12.420><c> it</c>

00:10:13.410 --> 00:10:13.420 align:start position:0%
slightly different from solidity so it
 

00:10:13.420 --> 00:10:16.200 align:start position:0%
slightly different from solidity so it
requires<00:10:13.810><c> you</c><00:10:13.990><c> to</c><00:10:14.140><c> learn</c><00:10:14.290><c> a</c><00:10:14.350><c> new</c><00:10:14.560><c> language</c><00:10:15.210><c> it</c>

00:10:16.200 --> 00:10:16.210 align:start position:0%
requires you to learn a new language it
 

00:10:16.210 --> 00:10:18.330 align:start position:0%
requires you to learn a new language it
requires<00:10:16.630><c> you</c><00:10:16.990><c> to</c><00:10:17.020><c> learn</c><00:10:17.680><c> how</c><00:10:17.890><c> to</c><00:10:17.920><c> use</c><00:10:18.160><c> these</c>

00:10:18.330 --> 00:10:18.340 align:start position:0%
requires you to learn how to use these
 

00:10:18.340 --> 00:10:21.780 align:start position:0%
requires you to learn how to use these
tools<00:10:18.580><c> and</c><00:10:19.000><c> this</c><00:10:19.930><c> is</c><00:10:20.190><c> this</c><00:10:21.190><c> makes</c><00:10:21.430><c> it</c><00:10:21.550><c> very</c>

00:10:21.780 --> 00:10:21.790 align:start position:0%
tools and this is this makes it very
 

00:10:21.790 --> 00:10:24.630 align:start position:0%
tools and this is this makes it very
hard<00:10:22.660><c> to</c><00:10:22.810><c> use</c><00:10:22.950><c> this</c><00:10:23.950><c> formal</c><00:10:24.310><c> verification</c>

00:10:24.630 --> 00:10:24.640 align:start position:0%
hard to use this formal verification
 

00:10:24.640 --> 00:10:27.600 align:start position:0%
hard to use this formal verification
tool<00:10:25.210><c> and</c><00:10:25.450><c> the</c><00:10:26.440><c> harder</c><00:10:26.740><c> it</c><00:10:26.860><c> is</c><00:10:26.890><c> to</c><00:10:27.010><c> use</c><00:10:27.280><c> the</c>

00:10:27.600 --> 00:10:27.610 align:start position:0%
tool and the harder it is to use the
 

00:10:27.610 --> 00:10:31.740 align:start position:0%
tool and the harder it is to use the
easier<00:10:28.180><c> it</c><00:10:28.300><c> is</c><00:10:28.420><c> to</c><00:10:28.660><c> make</c><00:10:29.020><c> mistakes</c><00:10:29.200><c> and</c><00:10:30.750><c> also</c>

00:10:31.740 --> 00:10:31.750 align:start position:0%
easier it is to make mistakes and also
 

00:10:31.750 --> 00:10:37.140 align:start position:0%
easier it is to make mistakes and also
it<00:10:32.320><c> is</c><00:10:32.470><c> easier</c><00:10:32.770><c> for</c><00:10:32.800><c> so</c><00:10:35.460><c> for</c><00:10:36.460><c> Mara</c><00:10:36.670><c> fication</c><00:10:36.910><c> is</c>

00:10:37.140 --> 00:10:37.150 align:start position:0%
it is easier for so for Mara fication is
 

00:10:37.150 --> 00:10:39.150 align:start position:0%
it is easier for so for Mara fication is
only<00:10:37.360><c> useful</c><00:10:37.720><c> if</c><00:10:38.110><c> people</c><00:10:38.380><c> understand</c><00:10:38.800><c> what</c><00:10:39.070><c> is</c>

00:10:39.150 --> 00:10:39.160 align:start position:0%
only useful if people understand what is
 

00:10:39.160 --> 00:10:41.280 align:start position:0%
only useful if people understand what is
actually<00:10:39.580><c> proven</c><00:10:40.270><c> there</c><00:10:40.480><c> so</c><00:10:40.690><c> the</c><00:10:40.810><c> statements</c>

00:10:41.280 --> 00:10:41.290 align:start position:0%
actually proven there so the statements
 

00:10:41.290 --> 00:10:42.510 align:start position:0%
actually proven there so the statements
that<00:10:41.350><c> are</c><00:10:41.440><c> proven</c><00:10:41.800><c> there</c><00:10:41.950><c> have</c><00:10:42.310><c> to</c><00:10:42.430><c> be</c>

00:10:42.510 --> 00:10:42.520 align:start position:0%
that are proven there have to be
 

00:10:42.520 --> 00:10:45.210 align:start position:0%
that are proven there have to be
understood<00:10:42.850><c> by</c><00:10:43.000><c> humans</c><00:10:43.360><c> and</c><00:10:43.890><c> if</c><00:10:44.890><c> that</c><00:10:45.010><c> is</c><00:10:45.130><c> not</c>

00:10:45.210 --> 00:10:45.220 align:start position:0%
understood by humans and if that is not
 

00:10:45.220 --> 00:10:46.860 align:start position:0%
understood by humans and if that is not
possible<00:10:45.280><c> then</c><00:10:45.820><c> nobody</c><00:10:46.180><c> will</c><00:10:46.330><c> use</c><00:10:46.360><c> formal</c>

00:10:46.860 --> 00:10:46.870 align:start position:0%
possible then nobody will use formal
 

00:10:46.870 --> 00:10:48.120 align:start position:0%
possible then nobody will use formal
verification<00:10:46.990><c> and</c><00:10:47.410><c> it's</c><00:10:47.560><c> useless</c><00:10:47.920><c> and</c>

00:10:48.120 --> 00:10:48.130 align:start position:0%
verification and it's useless and
 

00:10:48.130 --> 00:10:50.340 align:start position:0%
verification and it's useless and
because<00:10:48.610><c> of</c><00:10:48.640><c> that</c><00:10:48.850><c> so</c><00:10:49.540><c> yeah</c>

00:10:50.340 --> 00:10:50.350 align:start position:0%
because of that so yeah
 

00:10:50.350 --> 00:10:52.290 align:start position:0%
because of that so yeah
perhaps<00:10:50.890><c> that</c><00:10:51.070><c> approach</c><00:10:51.280><c> was</c><00:10:51.430><c> not</c><00:10:51.580><c> so</c><00:10:51.760><c> great</c>

00:10:52.290 --> 00:10:52.300 align:start position:0%
perhaps that approach was not so great
 

00:10:52.300 --> 00:10:55.880 align:start position:0%
perhaps that approach was not so great
so<00:10:52.480><c> we</c><00:10:52.600><c> took</c><00:10:52.720><c> a</c><00:10:52.780><c> step</c><00:10:52.990><c> back</c><00:10:53.170><c> and</c><00:10:53.440><c> reconsidered</c>

00:10:55.880 --> 00:10:55.890 align:start position:0%
so we took a step back and reconsidered
 

00:10:55.890 --> 00:11:00.270 align:start position:0%
so we took a step back and reconsidered
how<00:10:56.890><c> it</c><00:10:57.070><c> looks</c><00:10:57.100><c> now</c><00:10:57.370><c> is</c><00:10:57.850><c> like</c><00:10:58.660><c> this</c><00:10:59.280><c> we've</c>

00:11:00.270 --> 00:11:00.280 align:start position:0%
how it looks now is like this we've
 

00:11:00.280 --> 00:11:03.510 align:start position:0%
how it looks now is like this we've
replaced<00:11:00.700><c> y3</c><00:11:01.330><c> by</c><00:11:01.630><c> a</c><00:11:02.020><c> tool</c><00:11:02.620><c> called</c><00:11:02.920><c> an</c><00:11:03.130><c> SMT</c>

00:11:03.510 --> 00:11:03.520 align:start position:0%
replaced y3 by a tool called an SMT
 

00:11:03.520 --> 00:11:07.230 align:start position:0%
replaced y3 by a tool called an SMT
solver<00:11:05.070><c> SMT</c><00:11:06.070><c> solvers</c><00:11:06.370><c> are</c><00:11:06.580><c> less</c><00:11:07.000><c> powerful</c>

00:11:07.230 --> 00:11:07.240 align:start position:0%
solver SMT solvers are less powerful
 

00:11:07.240 --> 00:11:12.390 align:start position:0%
solver SMT solvers are less powerful
than<00:11:08.070><c> general</c><00:11:09.810><c> theorem</c><00:11:10.810><c> provers</c><00:11:11.140><c> and</c><00:11:12.070><c> because</c>

00:11:12.390 --> 00:11:12.400 align:start position:0%
than general theorem provers and because
 

00:11:12.400 --> 00:11:14.670 align:start position:0%
than general theorem provers and because
of<00:11:12.520><c> that</c><00:11:12.640><c> the</c><00:11:13.030><c> smart</c><00:11:13.330><c> contract</c><00:11:13.510><c> in</c><00:11:14.230><c> this</c><00:11:14.440><c> smart</c>

00:11:14.670 --> 00:11:14.680 align:start position:0%
of that the smart contract in this smart
 

00:11:14.680 --> 00:11:16.290 align:start position:0%
of that the smart contract in this smart
country<00:11:14.860><c> we</c><00:11:15.040><c> cannot</c><00:11:15.220><c> prove</c><00:11:15.490><c> that</c><00:11:15.550><c> the</c><00:11:15.940><c> sum</c><00:11:16.240><c> of</c>

00:11:16.290 --> 00:11:16.300 align:start position:0%
country we cannot prove that the sum of
 

00:11:16.300 --> 00:11:19.200 align:start position:0%
country we cannot prove that the sum of
all<00:11:16.630><c> balances</c><00:11:17.230><c> is</c><00:11:17.380><c> constant</c><00:11:17.950><c> but</c><00:11:18.850><c> we</c><00:11:18.970><c> can</c>

00:11:19.200 --> 00:11:19.210 align:start position:0%
all balances is constant but we can
 

00:11:19.210 --> 00:11:23.880 align:start position:0%
all balances is constant but we can
prove<00:11:19.480><c> that</c><00:11:21.150><c> the</c><00:11:22.150><c> sum</c><00:11:22.360><c> of</c><00:11:22.420><c> the</c><00:11:22.720><c> two</c><00:11:23.320><c> balances</c>

00:11:23.880 --> 00:11:23.890 align:start position:0%
prove that the sum of the two balances
 

00:11:23.890 --> 00:11:26.400 align:start position:0%
prove that the sum of the two balances
that<00:11:24.010><c> are</c><00:11:24.130><c> modified</c><00:11:24.460><c> is</c><00:11:25.030><c> constant</c><00:11:25.540><c> so</c><00:11:25.810><c> what</c>

00:11:26.400 --> 00:11:26.410 align:start position:0%
that are modified is constant so what
 

00:11:26.410 --> 00:11:28.860 align:start position:0%
that are modified is constant so what
happens<00:11:26.710><c> here</c><00:11:26.890><c> is</c><00:11:27.130><c> we</c><00:11:27.400><c> have</c><00:11:28.240><c> a</c><00:11:28.420><c> require</c>

00:11:28.860 --> 00:11:28.870 align:start position:0%
happens here is we have a require
 

00:11:28.870 --> 00:11:33.630 align:start position:0%
happens here is we have a require
statement<00:11:29.380><c> which</c><00:11:30.070><c> is</c><00:11:31.590><c> yeah</c><00:11:32.590><c> doesn't</c><00:11:33.460><c> have</c>

00:11:33.630 --> 00:11:33.640 align:start position:0%
statement which is yeah doesn't have
 

00:11:33.640 --> 00:11:34.980 align:start position:0%
statement which is yeah doesn't have
much<00:11:33.820><c> to</c><00:11:34.000><c> do</c><00:11:34.120><c> with</c><00:11:34.330><c> the</c><00:11:34.570><c> formal</c><00:11:34.870><c> verification</c>

00:11:34.980 --> 00:11:34.990 align:start position:0%
much to do with the formal verification
 

00:11:34.990 --> 00:11:36.600 align:start position:0%
much to do with the formal verification
this<00:11:35.440><c> is</c><00:11:35.590><c> just</c><00:11:35.800><c> the</c><00:11:35.920><c> regular</c><00:11:36.070><c> solidity</c>

00:11:36.600 --> 00:11:36.610 align:start position:0%
this is just the regular solidity
 

00:11:36.610 --> 00:11:38.640 align:start position:0%
this is just the regular solidity
requirements<00:11:37.180><c> require</c><00:11:37.540><c> statement</c><00:11:37.810><c> and</c><00:11:38.080><c> then</c>

00:11:38.640 --> 00:11:38.650 align:start position:0%
requirements require statement and then
 

00:11:38.650 --> 00:11:40.980 align:start position:0%
requirements require statement and then
we<00:11:38.770><c> store</c><00:11:39.160><c> the</c><00:11:39.640><c> sum</c><00:11:39.970><c> of</c><00:11:40.000><c> the</c><00:11:40.180><c> two</c><00:11:40.300><c> balances</c><00:11:40.780><c> in</c>

00:11:40.980 --> 00:11:40.990 align:start position:0%
we store the sum of the two balances in
 

00:11:40.990 --> 00:11:43.320 align:start position:0%
we store the sum of the two balances in
the<00:11:41.230><c> before</c><00:11:41.590><c> variable</c><00:11:42.130><c> we</c><00:11:42.910><c> perform</c><00:11:43.270><c> the</c>

00:11:43.320 --> 00:11:43.330 align:start position:0%
the before variable we perform the
 

00:11:43.330 --> 00:11:47.190 align:start position:0%
the before variable we perform the
modification<00:11:43.990><c> and</c><00:11:45.150><c> after</c><00:11:46.150><c> that</c><00:11:46.300><c> we</c><00:11:46.930><c> check</c>

00:11:47.190 --> 00:11:47.200 align:start position:0%
modification and after that we check
 

00:11:47.200 --> 00:11:50.700 align:start position:0%
modification and after that we check
that<00:11:47.230><c> before</c><00:11:48.160><c> equals</c><00:11:48.850><c> after</c><00:11:49.410><c> and</c><00:11:50.410><c> this</c><00:11:50.560><c> is</c><00:11:50.680><c> a</c>

00:11:50.700 --> 00:11:50.710 align:start position:0%
that before equals after and this is a
 

00:11:50.710 --> 00:11:53.970 align:start position:0%
that before equals after and this is a
regular<00:11:51.190><c> solidity</c><00:11:51.670><c> assert</c><00:11:52.060><c> so</c><00:11:52.390><c> if</c><00:11:52.990><c> the</c><00:11:53.740><c> sum</c><00:11:53.950><c> of</c>

00:11:53.970 --> 00:11:53.980 align:start position:0%
regular solidity assert so if the sum of
 

00:11:53.980 --> 00:11:56.910 align:start position:0%
regular solidity assert so if the sum of
the<00:11:54.220><c> balances</c><00:11:54.720><c> is</c><00:11:55.720><c> not</c><00:11:55.990><c> the</c><00:11:56.170><c> same</c><00:11:56.380><c> then</c><00:11:56.740><c> this</c>

00:11:56.910 --> 00:11:56.920 align:start position:0%
the balances is not the same then this
 

00:11:56.920 --> 00:11:59.310 align:start position:0%
the balances is not the same then this
will<00:11:57.160><c> throw</c><00:11:57.430><c> an</c><00:11:57.580><c> exception</c><00:11:57.670><c> at</c><00:11:58.030><c> run</c><00:11:58.210><c> time</c><00:11:58.320><c> but</c>

00:11:59.310 --> 00:11:59.320 align:start position:0%
will throw an exception at run time but
 

00:11:59.320 --> 00:12:02.190 align:start position:0%
will throw an exception at run time but
using<00:12:00.160><c> the</c><00:12:00.250><c> SMT</c><00:12:00.610><c> solver</c><00:12:01.030><c> you</c><00:12:01.480><c> also</c><00:12:01.660><c> get</c><00:12:01.990><c> a</c>

00:12:02.190 --> 00:12:02.200 align:start position:0%
using the SMT solver you also get a
 

00:12:02.200 --> 00:12:04.350 align:start position:0%
using the SMT solver you also get a
proof<00:12:02.560><c> at</c><00:12:02.830><c> compile</c><00:12:03.340><c> time</c><00:12:03.370><c> that</c><00:12:04.240><c> this</c>

00:12:04.350 --> 00:12:04.360 align:start position:0%
proof at compile time that this
 

00:12:04.360 --> 00:12:09.060 align:start position:0%
proof at compile time that this
assertion<00:12:04.690><c> will</c><00:12:05.200><c> never</c><00:12:05.380><c> be</c><00:12:05.530><c> triggered</c><00:12:08.040><c> okay</c>

00:12:09.060 --> 00:12:09.070 align:start position:0%
assertion will never be triggered okay
 

00:12:09.070 --> 00:12:11.070 align:start position:0%
assertion will never be triggered okay
more<00:12:09.940><c> specifically</c><00:12:10.360><c> what</c><00:12:10.510><c> happens</c><00:12:10.810><c> is</c><00:12:10.930><c> that</c>

00:12:11.070 --> 00:12:11.080 align:start position:0%
more specifically what happens is that
 

00:12:11.080 --> 00:12:13.680 align:start position:0%
more specifically what happens is that
so<00:12:11.350><c> you</c><00:12:11.410><c> can</c><00:12:11.680><c> use</c><00:12:11.890><c> this</c><00:12:12.130><c> tool</c><00:12:12.370><c> with</c><00:12:13.000><c> require</c>

00:12:13.680 --> 00:12:13.690 align:start position:0%
so you can use this tool with require
 

00:12:13.690 --> 00:12:17.040 align:start position:0%
so you can use this tool with require
statements<00:12:14.380><c> to</c><00:12:15.030><c> have</c><00:12:16.030><c> expressions</c><00:12:16.600><c> that</c><00:12:16.810><c> you</c>

00:12:17.040 --> 00:12:17.050 align:start position:0%
statements to have expressions that you
 

00:12:17.050 --> 00:12:20.640 align:start position:0%
statements to have expressions that you
assume<00:12:17.500><c> to</c><00:12:17.650><c> be</c><00:12:17.680><c> correct</c><00:12:18.070><c> and</c><00:12:18.400><c> then</c><00:12:19.440><c> the</c><00:12:20.440><c> tool</c>

00:12:20.640 --> 00:12:20.650 align:start position:0%
assume to be correct and then the tool
 

00:12:20.650 --> 00:12:23.940 align:start position:0%
assume to be correct and then the tool
proves<00:12:21.220><c> that</c><00:12:21.670><c> there</c><00:12:22.180><c> is</c><00:12:22.350><c> no</c><00:12:23.350><c> assertion</c><00:12:23.650><c> that</c>

00:12:23.940 --> 00:12:23.950 align:start position:0%
proves that there is no assertion that
 

00:12:23.950 --> 00:12:26.340 align:start position:0%
proves that there is no assertion that
fails<00:12:24.220><c> there</c><00:12:25.120><c> is</c><00:12:25.210><c> no</c><00:12:25.510><c> overflow</c><00:12:26.110><c> or</c><00:12:26.320><c> underflow</c>

00:12:26.340 --> 00:12:26.350 align:start position:0%
fails there is no overflow or underflow
 

00:12:26.350 --> 00:12:29.490 align:start position:0%
fails there is no overflow or underflow
in<00:12:26.950><c> your</c><00:12:27.310><c> Matic</c><00:12:27.970><c> operations</c><00:12:28.510><c> no</c><00:12:29.080><c> division</c><00:12:29.410><c> by</c>

00:12:29.490 --> 00:12:29.500 align:start position:0%
in your Matic operations no division by
 

00:12:29.500 --> 00:12:31.440 align:start position:0%
in your Matic operations no division by
zero<00:12:29.710><c> no</c><00:12:30.220><c> constant</c><00:12:30.850><c> conditions</c><00:12:31.210><c> no</c>

00:12:31.440 --> 00:12:31.450 align:start position:0%
zero no constant conditions no
 

00:12:31.450 --> 00:12:33.000 align:start position:0%
zero no constant conditions no
unreachable<00:12:31.810><c> code</c><00:12:32.110><c> and</c><00:12:32.380><c> whatever</c><00:12:32.680><c> we</c><00:12:32.860><c> will</c>

00:12:33.000 --> 00:12:33.010 align:start position:0%
unreachable code and whatever we will
 

00:12:33.010 --> 00:12:35.970 align:start position:0%
unreachable code and whatever we will
come<00:12:33.580><c> up</c><00:12:33.700><c> in</c><00:12:33.790><c> the</c><00:12:33.880><c> future</c><00:12:34.030><c> and</c><00:12:34.720><c> so</c><00:12:35.710><c> let's</c><00:12:35.890><c> take</c>

00:12:35.970 --> 00:12:35.980 align:start position:0%
come up in the future and so let's take
 

00:12:35.980 --> 00:12:40.770 align:start position:0%
come up in the future and so let's take
a<00:12:36.040><c> look</c><00:12:36.220><c> at</c><00:12:36.280><c> a</c><00:12:37.170><c> simpler</c><00:12:38.170><c> example</c><00:12:39.540><c> this</c><00:12:40.540><c> is</c><00:12:40.690><c> the</c>

00:12:40.770 --> 00:12:40.780 align:start position:0%
a look at a simpler example this is the
 

00:12:40.780 --> 00:12:42.420 align:start position:0%
a look at a simpler example this is the
experimental<00:12:41.290><c> feature</c><00:12:41.590><c> and</c><00:12:41.950><c> because</c><00:12:42.310><c> of</c><00:12:42.340><c> that</c>

00:12:42.420 --> 00:12:42.430 align:start position:0%
experimental feature and because of that
 

00:12:42.430 --> 00:12:44.310 align:start position:0%
experimental feature and because of that
you<00:12:42.610><c> need</c><00:12:42.730><c> this</c><00:12:42.910><c> first</c><00:12:43.270><c> line</c><00:12:43.480><c> that</c><00:12:43.780><c> activates</c>

00:12:44.310 --> 00:12:44.320 align:start position:0%
you need this first line that activates
 

00:12:44.320 --> 00:12:45.150 align:start position:0%
you need this first line that activates
the<00:12:44.410><c> SMT</c><00:12:44.830><c> checker</c>

00:12:45.150 --> 00:12:45.160 align:start position:0%
the SMT checker
 

00:12:45.160 --> 00:12:48.900 align:start position:0%
the SMT checker
and<00:12:45.990><c> yeah</c><00:12:46.990><c> the</c><00:12:47.590><c> function</c><00:12:47.920><c> here</c><00:12:48.220><c> it</c><00:12:48.460><c> just</c><00:12:48.610><c> takes</c>

00:12:48.900 --> 00:12:48.910 align:start position:0%
and yeah the function here it just takes
 

00:12:48.910 --> 00:12:52.100 align:start position:0%
and yeah the function here it just takes
two<00:12:49.060><c> numbers</c><00:12:49.090><c> and</c><00:12:49.600><c> adds</c><00:12:49.750><c> them</c><00:12:50.110><c> of</c><00:12:50.940><c> course</c>

00:12:52.100 --> 00:12:52.110 align:start position:0%
two numbers and adds them of course
 

00:12:52.110 --> 00:12:54.450 align:start position:0%
two numbers and adds them of course
there's<00:12:53.110><c> a</c><00:12:53.200><c> problem</c><00:12:53.590><c> because</c><00:12:53.740><c> we</c><00:12:54.250><c> can't</c>

00:12:54.450 --> 00:12:54.460 align:start position:0%
there's a problem because we can't
 

00:12:54.460 --> 00:12:56.010 align:start position:0%
there's a problem because we can't
create<00:12:54.670><c> and</c><00:12:55.000><c> we</c><00:12:55.450><c> can</c><00:12:55.600><c> have</c><00:12:55.690><c> an</c><00:12:55.810><c> arithmetic</c>

00:12:56.010 --> 00:12:56.020 align:start position:0%
create and we can have an arithmetic
 

00:12:56.020 --> 00:12:58.650 align:start position:0%
create and we can have an arithmetic
overflow<00:12:56.410><c> here</c><00:12:56.680><c> in</c><00:12:56.800><c> this</c><00:12:56.950><c> edition</c><00:12:57.280><c> and</c><00:12:57.660><c> this</c>

00:12:58.650 --> 00:12:58.660 align:start position:0%
overflow here in this edition and this
 

00:12:58.660 --> 00:13:00.720 align:start position:0%
overflow here in this edition and this
is<00:12:58.900><c> exactly</c><00:12:59.200><c> what</c><00:12:59.770><c> the</c><00:13:00.070><c> so</c><00:13:00.340><c> if</c><00:13:00.430><c> you</c><00:13:00.490><c> run</c><00:13:00.640><c> the</c>

00:13:00.720 --> 00:13:00.730 align:start position:0%
is exactly what the so if you run the
 

00:13:00.730 --> 00:13:02.160 align:start position:0%
is exactly what the so if you run the
compiler<00:13:01.000><c> on</c><00:13:01.240><c> that</c><00:13:01.420><c> then</c><00:13:01.720><c> this</c><00:13:01.930><c> is</c><00:13:02.050><c> the</c>

00:13:02.160 --> 00:13:02.170 align:start position:0%
compiler on that then this is the
 

00:13:02.170 --> 00:13:06.670 align:start position:0%
compiler on that then this is the
message<00:13:02.320><c> you</c><00:13:02.500><c> will</c><00:13:02.620><c> get</c><00:13:02.910><c> and</c>

00:13:06.670 --> 00:13:06.680 align:start position:0%
 
 

00:13:06.680 --> 00:13:08.290 align:start position:0%
 
the<00:13:07.250><c> great</c><00:13:07.460><c> thing</c><00:13:07.640><c> about</c><00:13:07.670><c> this</c><00:13:07.940><c> isn't</c><00:13:08.090><c> you</c>

00:13:08.290 --> 00:13:08.300 align:start position:0%
the great thing about this isn't you
 

00:13:08.300 --> 00:13:11.080 align:start position:0%
the great thing about this isn't you
solver<00:13:08.570><c> is</c><00:13:08.660><c> that</c><00:13:08.840><c> it</c><00:13:08.990><c> has</c><00:13:09.170><c> so</c><00:13:09.740><c> it's</c><00:13:10.090><c> more</c>

00:13:11.080 --> 00:13:11.090 align:start position:0%
solver is that it has so it's more
 

00:13:11.090 --> 00:13:13.210 align:start position:0%
solver is that it has so it's more
limited<00:13:11.510><c> than</c><00:13:11.660><c> y3</c><00:13:12.380><c> but</c><00:13:12.740><c> it</c><00:13:12.830><c> has</c><00:13:12.950><c> a</c><00:13:12.980><c> feature</c>

00:13:13.210 --> 00:13:13.220 align:start position:0%
limited than y3 but it has a feature
 

00:13:13.220 --> 00:13:14.950 align:start position:0%
limited than y3 but it has a feature
that<00:13:13.370><c> y3</c><00:13:13.880><c> did</c><00:13:14.000><c> not</c><00:13:14.150><c> have</c><00:13:14.360><c> and</c><00:13:14.660><c> this</c><00:13:14.780><c> is</c><00:13:14.840><c> the</c>

00:13:14.950 --> 00:13:14.960 align:start position:0%
that y3 did not have and this is the
 

00:13:14.960 --> 00:13:18.730 align:start position:0%
that y3 did not have and this is the
following<00:13:15.670><c> so</c><00:13:16.670><c> you</c><00:13:16.960><c> if</c><00:13:17.960><c> an</c><00:13:18.140><c> assertion</c><00:13:18.380><c> fails</c>

00:13:18.730 --> 00:13:18.740 align:start position:0%
following so you if an assertion fails
 

00:13:18.740 --> 00:13:20.770 align:start position:0%
following so you if an assertion fails
it<00:13:19.010><c> tells</c><00:13:19.220><c> you</c><00:13:19.340><c> why</c><00:13:19.550><c> it</c><00:13:19.610><c> fails</c><00:13:20.060><c> and</c><00:13:20.360><c> I</c><00:13:20.600><c> think</c>

00:13:20.770 --> 00:13:20.780 align:start position:0%
it tells you why it fails and I think
 

00:13:20.780 --> 00:13:22.120 align:start position:0%
it tells you why it fails and I think
this<00:13:20.900><c> is</c><00:13:21.020><c> really</c><00:13:21.650><c> important</c><00:13:22.040><c> because</c>

00:13:22.120 --> 00:13:22.130 align:start position:0%
this is really important because
 

00:13:22.130 --> 00:13:24.460 align:start position:0%
this is really important because
otherwise<00:13:22.400><c> people</c><00:13:22.790><c> say</c><00:13:23.030><c> ah</c><00:13:23.060><c> I</c><00:13:23.570><c> don't</c><00:13:23.630><c> know</c><00:13:23.750><c> it</c>

00:13:24.460 --> 00:13:24.470 align:start position:0%
otherwise people say ah I don't know it
 

00:13:24.470 --> 00:13:26.560 align:start position:0%
otherwise people say ah I don't know it
doesn't<00:13:24.680><c> work</c><00:13:24.800><c> but</c><00:13:25.220><c> okay</c><00:13:26.060><c> let's</c><00:13:26.270><c> just</c><00:13:26.450><c> let's</c>

00:13:26.560 --> 00:13:26.570 align:start position:0%
doesn't work but okay let's just let's
 

00:13:26.570 --> 00:13:29.050 align:start position:0%
doesn't work but okay let's just let's
just<00:13:26.900><c> comment</c><00:13:27.770><c> it</c><00:13:27.830><c> out</c><00:13:27.950><c> or</c><00:13:28.250><c> whatever</c><00:13:28.550><c> throw</c>

00:13:29.050 --> 00:13:29.060 align:start position:0%
just comment it out or whatever throw
 

00:13:29.060 --> 00:13:30.100 align:start position:0%
just comment it out or whatever throw
something<00:13:29.390><c> at</c><00:13:29.510><c> it</c><00:13:29.540><c> so</c><00:13:29.720><c> that</c><00:13:29.840><c> it</c><00:13:29.930><c> doesn't</c>

00:13:30.100 --> 00:13:30.110 align:start position:0%
something at it so that it doesn't
 

00:13:30.110 --> 00:13:32.470 align:start position:0%
something at it so that it doesn't
complain<00:13:30.440><c> anymore</c><00:13:30.680><c> but</c><00:13:31.340><c> this</c><00:13:31.460><c> tells</c><00:13:32.150><c> you</c><00:13:32.300><c> why</c>

00:13:32.470 --> 00:13:32.480 align:start position:0%
complain anymore but this tells you why
 

00:13:32.480 --> 00:13:37.360 align:start position:0%
complain anymore but this tells you why
it<00:13:32.540><c> fails</c><00:13:32.840><c> and</c><00:13:34.360><c> kind</c><00:13:35.360><c> of</c><00:13:35.710><c> forces</c><00:13:36.710><c> you</c><00:13:36.950><c> to</c><00:13:36.980><c> think</c>

00:13:37.360 --> 00:13:37.370 align:start position:0%
it fails and kind of forces you to think
 

00:13:37.370 --> 00:13:40.000 align:start position:0%
it fails and kind of forces you to think
about<00:13:38.090><c> this</c><00:13:38.390><c> edition</c><00:13:38.870><c> and</c><00:13:39.140><c> think</c><00:13:39.530><c> about</c><00:13:39.740><c> why</c>

00:13:40.000 --> 00:13:40.010 align:start position:0%
about this edition and think about why
 

00:13:40.010 --> 00:13:42.420 align:start position:0%
about this edition and think about why
it<00:13:40.070><c> might</c><00:13:40.280><c> create</c><00:13:40.730><c> an</c><00:13:41.000><c> overflow</c><00:13:41.420><c> and</c><00:13:41.630><c> then</c>

00:13:42.420 --> 00:13:42.430 align:start position:0%
it might create an overflow and then
 

00:13:42.430 --> 00:13:45.340 align:start position:0%
it might create an overflow and then
take<00:13:43.430><c> the</c><00:13:43.550><c> necessary</c><00:13:43.700><c> steps</c><00:13:44.060><c> to</c><00:13:44.480><c> prevent</c><00:13:44.990><c> the</c>

00:13:45.340 --> 00:13:45.350 align:start position:0%
take the necessary steps to prevent the
 

00:13:45.350 --> 00:13:49.290 align:start position:0%
take the necessary steps to prevent the
overflow<00:13:45.800><c> before</c><00:13:46.190><c> it</c><00:13:46.280><c> happens</c><00:13:46.610><c> there</c><00:13:47.600><c> are</c><00:13:48.070><c> so</c>

00:13:49.290 --> 00:13:49.300 align:start position:0%
overflow before it happens there are so
 

00:13:49.300 --> 00:13:52.060 align:start position:0%
overflow before it happens there are so
currently<00:13:50.300><c> what</c><00:13:50.480><c> people</c><00:13:50.750><c> often</c><00:13:50.990><c> do</c><00:13:51.110><c> is</c><00:13:51.350><c> create</c>

00:13:52.060 --> 00:13:52.070 align:start position:0%
currently what people often do is create
 

00:13:52.070 --> 00:13:54.280 align:start position:0%
currently what people often do is create
runtime<00:13:52.550><c> checks</c><00:13:52.880><c> about</c><00:13:53.330><c> overflow</c><00:13:53.810><c> at</c><00:13:54.020><c> runtime</c>

00:13:54.280 --> 00:13:54.290 align:start position:0%
runtime checks about overflow at runtime
 

00:13:54.290 --> 00:13:57.430 align:start position:0%
runtime checks about overflow at runtime
checks<00:13:54.650><c> about</c><00:13:54.860><c> overflow</c><00:13:55.280><c> in</c><00:13:55.720><c> arithmetics</c><00:13:56.720><c> but</c>

00:13:57.430 --> 00:13:57.440 align:start position:0%
checks about overflow in arithmetics but
 

00:13:57.440 --> 00:14:00.910 align:start position:0%
checks about overflow in arithmetics but
this<00:13:58.400><c> can</c><00:13:58.820><c> be</c><00:13:59.000><c> really</c><00:13:59.270><c> dangerous</c><00:13:59.420><c> because</c><00:13:59.930><c> if</c>

00:14:00.910 --> 00:14:00.920 align:start position:0%
this can be really dangerous because if
 

00:14:00.920 --> 00:14:03.130 align:start position:0%
this can be really dangerous because if
you<00:14:01.190><c> end</c><00:14:01.460><c> up</c><00:14:01.580><c> in</c><00:14:01.670><c> a</c><00:14:01.730><c> situation</c><00:14:01.940><c> where</c><00:14:02.510><c> you</c><00:14:02.720><c> you</c>

00:14:03.130 --> 00:14:03.140 align:start position:0%
you end up in a situation where you you
 

00:14:03.140 --> 00:14:05.290 align:start position:0%
you end up in a situation where you you
have<00:14:03.170><c> an</c><00:14:03.620><c> overflow</c><00:14:03.860><c> because</c><00:14:04.340><c> of</c><00:14:04.490><c> some</c><00:14:04.760><c> yeah</c>

00:14:05.290 --> 00:14:05.300 align:start position:0%
have an overflow because of some yeah
 

00:14:05.300 --> 00:14:08.230 align:start position:0%
have an overflow because of some yeah
internal<00:14:06.280><c> mechanism</c><00:14:07.280><c> of</c><00:14:07.370><c> the</c><00:14:07.700><c> smart</c><00:14:07.910><c> contract</c>

00:14:08.230 --> 00:14:08.240 align:start position:0%
internal mechanism of the smart contract
 

00:14:08.240 --> 00:14:10.240 align:start position:0%
internal mechanism of the smart contract
then<00:14:08.390><c> it</c><00:14:08.510><c> will</c><00:14:08.660><c> be</c><00:14:08.810><c> the</c><00:14:09.290><c> the</c><00:14:09.920><c> smart</c><00:14:10.130><c> contract</c>

00:14:10.240 --> 00:14:10.250 align:start position:0%
then it will be the the smart contract
 

00:14:10.250 --> 00:14:11.740 align:start position:0%
then it will be the the smart contract
will<00:14:10.550><c> be</c><00:14:10.580><c> stuck</c><00:14:10.850><c> because</c><00:14:11.210><c> it</c><00:14:11.360><c> will</c><00:14:11.480><c> always</c>

00:14:11.740 --> 00:14:11.750 align:start position:0%
will be stuck because it will always
 

00:14:11.750 --> 00:14:13.150 align:start position:0%
will be stuck because it will always
throw<00:14:11.960><c> this</c><00:14:12.230><c> exception</c><00:14:12.710><c> because</c><00:14:12.860><c> of</c><00:14:13.070><c> the</c>

00:14:13.150 --> 00:14:13.160 align:start position:0%
throw this exception because of the
 

00:14:13.160 --> 00:14:15.370 align:start position:0%
throw this exception because of the
overflow<00:14:13.370><c> and</c><00:14:13.730><c> you</c><00:14:14.180><c> perhaps</c><00:14:14.540><c> can't</c><00:14:14.900><c> get</c><00:14:15.080><c> the</c>

00:14:15.370 --> 00:14:15.380 align:start position:0%
overflow and you perhaps can't get the
 

00:14:15.380 --> 00:14:18.190 align:start position:0%
overflow and you perhaps can't get the
money<00:14:15.560><c> out</c><00:14:15.740><c> or</c><00:14:15.980><c> whatever</c><00:14:16.390><c> but</c><00:14:17.390><c> if</c><00:14:17.570><c> you</c><00:14:17.720><c> already</c>

00:14:18.190 --> 00:14:18.200 align:start position:0%
money out or whatever but if you already
 

00:14:18.200 --> 00:14:20.830 align:start position:0%
money out or whatever but if you already
get<00:14:18.770><c> the</c><00:14:18.950><c> warning</c><00:14:19.190><c> at</c><00:14:19.940><c> compile</c><00:14:20.360><c> time</c><00:14:20.390><c> before</c>

00:14:20.830 --> 00:14:20.840 align:start position:0%
get the warning at compile time before
 

00:14:20.840 --> 00:14:22.030 align:start position:0%
get the warning at compile time before
you<00:14:20.900><c> deploy</c><00:14:21.170><c> your</c><00:14:21.320><c> contract</c><00:14:21.680><c> you</c><00:14:21.710><c> can</c><00:14:21.860><c> think</c>

00:14:22.030 --> 00:14:22.040 align:start position:0%
you deploy your contract you can think
 

00:14:22.040 --> 00:14:23.860 align:start position:0%
you deploy your contract you can think
about<00:14:22.100><c> why</c><00:14:22.580><c> it</c><00:14:22.640><c> happens</c><00:14:23.090><c> and</c><00:14:23.210><c> prevent</c><00:14:23.690><c> this</c>

00:14:23.860 --> 00:14:23.870 align:start position:0%
about why it happens and prevent this
 

00:14:23.870 --> 00:14:25.570 align:start position:0%
about why it happens and prevent this
from<00:14:24.350><c> happening</c><00:14:24.590><c> in</c><00:14:24.920><c> the</c><00:14:25.010><c> first</c><00:14:25.160><c> place</c><00:14:25.250><c> and</c>

00:14:25.570 --> 00:14:25.580 align:start position:0%
from happening in the first place and
 

00:14:25.580 --> 00:14:27.070 align:start position:0%
from happening in the first place and
how<00:14:25.760><c> are</c><00:14:25.820><c> you</c><00:14:25.940><c> prevented</c><00:14:26.360><c> this</c><00:14:26.450><c> like</c><00:14:26.660><c> this</c><00:14:26.810><c> so</c>

00:14:27.070 --> 00:14:27.080 align:start position:0%
how are you prevented this like this so
 

00:14:27.080 --> 00:14:30.940 align:start position:0%
how are you prevented this like this so
you<00:14:27.830><c> had</c><00:14:27.950><c> a</c><00:14:27.980><c> require</c><00:14:28.340><c> statement</c><00:14:28.870><c> which</c><00:14:29.950><c> of</c>

00:14:30.940 --> 00:14:30.950 align:start position:0%
you had a require statement which of
 

00:14:30.950 --> 00:14:32.740 align:start position:0%
you had a require statement which of
course<00:14:31.220><c> in</c><00:14:31.370><c> the</c><00:14:31.460><c> end</c><00:14:31.580><c> has</c><00:14:31.730><c> the</c><00:14:31.760><c> same</c><00:14:32.090><c> effect</c><00:14:32.510><c> as</c>

00:14:32.740 --> 00:14:32.750 align:start position:0%
course in the end has the same effect as
 

00:14:32.750 --> 00:14:35.020 align:start position:0%
course in the end has the same effect as
if<00:14:32.840><c> you</c><00:14:33.350><c> would</c><00:14:33.500><c> just</c><00:14:33.650><c> check</c><00:14:34.400><c> if</c><00:14:34.610><c> there</c><00:14:34.850><c> is</c><00:14:34.940><c> an</c>

00:14:35.020 --> 00:14:35.030 align:start position:0%
if you would just check if there is an
 

00:14:35.030 --> 00:14:38.740 align:start position:0%
if you would just check if there is an
overflow<00:14:35.240><c> but</c><00:14:35.960><c> the</c><00:14:36.320><c> benefit</c><00:14:36.980><c> is</c><00:14:37.010><c> that</c><00:14:37.400><c> you</c><00:14:38.300><c> see</c>

00:14:38.740 --> 00:14:38.750 align:start position:0%
overflow but the benefit is that you see
 

00:14:38.750 --> 00:14:40.210 align:start position:0%
overflow but the benefit is that you see
that<00:14:38.780><c> there</c><00:14:39.080><c> isn't</c><00:14:39.230><c> there's</c><00:14:39.740><c> an</c><00:14:39.860><c> additional</c>

00:14:40.210 --> 00:14:40.220 align:start position:0%
that there isn't there's an additional
 

00:14:40.220 --> 00:14:42.850 align:start position:0%
that there isn't there's an additional
condition<00:14:40.700><c> that</c><00:14:41.210><c> is</c><00:14:41.540><c> present</c><00:14:42.470><c> about</c><00:14:42.620><c> these</c>

00:14:42.850 --> 00:14:42.860 align:start position:0%
condition that is present about these
 

00:14:42.860 --> 00:14:45.610 align:start position:0%
condition that is present about these
numbers<00:14:43.100><c> a</c><00:14:43.370><c> and</c><00:14:43.400><c> B</c><00:14:43.670><c> and</c><00:14:44.150><c> the</c><00:14:44.840><c> SMT</c><00:14:45.200><c> solver</c><00:14:45.470><c> will</c>

00:14:45.610 --> 00:14:45.620 align:start position:0%
numbers a and B and the SMT solver will
 

00:14:45.620 --> 00:14:48.220 align:start position:0%
numbers a and B and the SMT solver will
now<00:14:45.770><c> see</c><00:14:46.250><c> the</c><00:14:46.280><c> require</c><00:14:46.760><c> statement</c><00:14:47.090><c> take</c><00:14:47.990><c> these</c>

00:14:48.220 --> 00:14:48.230 align:start position:0%
now see the require statement take these
 

00:14:48.230 --> 00:14:50.920 align:start position:0%
now see the require statement take these
conditions<00:14:48.890><c> into</c><00:14:49.370><c> account</c><00:14:49.700><c> and</c><00:14:50.090><c> then</c><00:14:50.630><c> check</c>

00:14:50.920 --> 00:14:50.930 align:start position:0%
conditions into account and then check
 

00:14:50.930 --> 00:14:52.360 align:start position:0%
conditions into account and then check
again<00:14:50.960><c> whether</c><00:14:51.530><c> the</c><00:14:51.710><c> overflow</c><00:14:51.980><c> will</c><00:14:52.100><c> happen</c>

00:14:52.360 --> 00:14:52.370 align:start position:0%
again whether the overflow will happen
 

00:14:52.370 --> 00:14:55.270 align:start position:0%
again whether the overflow will happen
and<00:14:52.490><c> of</c><00:14:52.610><c> course</c><00:14:52.850><c> it</c><00:14:53.000><c> sees</c><00:14:53.180><c> that</c><00:14:53.360><c> a</c><00:14:53.630><c> number</c><00:14:54.280><c> less</c>

00:14:55.270 --> 00:14:55.280 align:start position:0%
and of course it sees that a number less
 

00:14:55.280 --> 00:14:57.130 align:start position:0%
and of course it sees that a number less
than<00:14:55.310><c> 2</c><00:14:55.610><c> to</c><00:14:55.730><c> the</c><00:14:55.820><c> 100</c><00:14:56.480><c> plus</c><00:14:56.630><c> the</c><00:14:56.780><c> number</c><00:14:57.020><c> less</c>

00:14:57.130 --> 00:14:57.140 align:start position:0%
than 2 to the 100 plus the number less
 

00:14:57.140 --> 00:14:59.350 align:start position:0%
than 2 to the 100 plus the number less
than<00:14:57.170><c> 2</c><00:14:57.440><c> to</c><00:14:57.560><c> the</c><00:14:57.590><c> 100</c><00:14:58.280><c> will</c><00:14:58.490><c> be</c><00:14:58.520><c> less</c><00:14:58.790><c> than</c><00:14:59.000><c> 2</c><00:14:59.210><c> to</c>

00:14:59.350 --> 00:14:59.360 align:start position:0%
than 2 to the 100 will be less than 2 to
 

00:14:59.360 --> 00:15:07.300 align:start position:0%
than 2 to the 100 will be less than 2 to
1356<00:15:01.330><c> ok</c><00:15:05.440><c> yeah</c><00:15:06.440><c> let's</c><00:15:06.710><c> take</c><00:15:07.070><c> a</c><00:15:07.100><c> look</c><00:15:07.250><c> at</c>

00:15:07.300 --> 00:15:07.310 align:start position:0%
1356 ok yeah let's take a look at
 

00:15:07.310 --> 00:15:10.600 align:start position:0%
1356 ok yeah let's take a look at
another<00:15:07.400><c> example</c><00:15:08.050><c> this</c><00:15:09.050><c> is</c><00:15:09.350><c> taken</c><00:15:09.860><c> this</c><00:15:10.310><c> is</c><00:15:10.460><c> an</c>

00:15:10.600 --> 00:15:10.610 align:start position:0%
another example this is taken this is an
 

00:15:10.610 --> 00:15:12.130 align:start position:0%
another example this is taken this is an
actual<00:15:11.030><c> example</c><00:15:11.150><c> from</c><00:15:11.480><c> the</c><00:15:11.630><c> underhanded</c>

00:15:12.130 --> 00:15:12.140 align:start position:0%
actual example from the underhanded
 

00:15:12.140 --> 00:15:14.680 align:start position:0%
actual example from the underhanded
solidity<00:15:12.530><c> coding</c><00:15:13.130><c> contest</c><00:15:13.520><c> where</c><00:15:14.210><c> there</c><00:15:14.510><c> was</c>

00:15:14.680 --> 00:15:14.690 align:start position:0%
solidity coding contest where there was
 

00:15:14.690 --> 00:15:17.560 align:start position:0%
solidity coding contest where there was
a<00:15:14.800><c> loop</c><00:15:15.800><c> that</c><00:15:16.190><c> used</c><00:15:16.490><c> an</c><00:15:16.640><c> unsigned</c><00:15:17.030><c> variable</c>

00:15:17.560 --> 00:15:17.570 align:start position:0%
a loop that used an unsigned variable
 

00:15:17.570 --> 00:15:20.120 align:start position:0%
a loop that used an unsigned variable
and<00:15:17.780><c> decreased</c><00:15:18.350><c> it</c><00:15:18.530><c> but</c><00:15:18.770><c> checked</c><00:15:19.070><c> against</c>

00:15:20.120 --> 00:15:20.130 align:start position:0%
and decreased it but checked against
 

00:15:20.130 --> 00:15:22.910 align:start position:0%
and decreased it but checked against
equaling<00:15:20.640><c> zero</c><00:15:20.880><c> and</c><00:15:21.150><c> of</c><00:15:21.570><c> course</c><00:15:21.840><c> this</c><00:15:22.620><c> loop</c>

00:15:22.910 --> 00:15:22.920 align:start position:0%
equaling zero and of course this loop
 

00:15:22.920 --> 00:15:25.670 align:start position:0%
equaling zero and of course this loop
condition<00:15:23.160><c> is</c><00:15:23.400><c> always</c><00:15:23.820><c> true</c><00:15:24.470><c> that's</c><00:15:25.470><c> of</c>

00:15:25.670 --> 00:15:25.680 align:start position:0%
condition is always true that's of
 

00:15:25.680 --> 00:15:28.580 align:start position:0%
condition is always true that's of
course<00:15:25.890><c> something</c><00:15:26.280><c> that</c><00:15:27.240><c> can</c><00:15:27.480><c> be</c><00:15:27.720><c> detected</c>

00:15:28.580 --> 00:15:28.590 align:start position:0%
course something that can be detected
 

00:15:28.590 --> 00:15:30.860 align:start position:0%
course something that can be detected
from<00:15:28.770><c> the</c><00:15:29.070><c> type</c><00:15:29.370><c> of</c><00:15:29.400><c> of</c><00:15:29.940><c> the</c><00:15:30.150><c> variable</c><00:15:30.600><c> alone</c>

00:15:30.860 --> 00:15:30.870 align:start position:0%
from the type of of the variable alone
 

00:15:30.870 --> 00:15:32.780 align:start position:0%
from the type of of the variable alone
and<00:15:31.200><c> you</c><00:15:31.440><c> don't</c><00:15:31.620><c> really</c><00:15:31.860><c> need</c><00:15:32.040><c> an</c><00:15:32.160><c> SMT</c><00:15:32.550><c> checker</c>

00:15:32.780 --> 00:15:32.790 align:start position:0%
and you don't really need an SMT checker
 

00:15:32.790 --> 00:15:37.970 align:start position:0%
and you don't really need an SMT checker
but<00:15:33.180><c> yeah</c><00:15:34.020><c> I</c><00:15:35.900><c> this</c><00:15:36.900><c> was</c><00:15:37.170><c> a</c><00:15:37.200><c> simple</c><00:15:37.470><c> example</c><00:15:37.950><c> to</c>

00:15:37.970 --> 00:15:37.980 align:start position:0%
but yeah I this was a simple example to
 

00:15:37.980 --> 00:15:40.900 align:start position:0%
but yeah I this was a simple example to
present<00:15:38.310><c> here</c><00:15:38.490><c> and</c><00:15:38.670><c> it</c><00:15:39.540><c> can</c><00:15:39.840><c> do</c><00:15:40.080><c> much</c><00:15:40.470><c> more</c>

00:15:40.900 --> 00:15:40.910 align:start position:0%
present here and it can do much more
 

00:15:40.910 --> 00:15:45.920 align:start position:0%
present here and it can do much more
complicated<00:15:41.910><c> conditions</c><00:15:42.600><c> and</c><00:15:44.720><c> yes</c><00:15:45.720><c> this</c><00:15:45.870><c> is</c>

00:15:45.920 --> 00:15:45.930 align:start position:0%
complicated conditions and yes this is
 

00:15:45.930 --> 00:15:50.450 align:start position:0%
complicated conditions and yes this is
what<00:15:46.050><c> we'll</c><00:15:46.350><c> see</c><00:15:46.620><c> next</c><00:15:46.650><c> and</c><00:15:48.590><c> yeah</c><00:15:49.590><c> this</c><00:15:49.740><c> talk</c>

00:15:50.450 --> 00:15:50.460 align:start position:0%
what we'll see next and yeah this talk
 

00:15:50.460 --> 00:15:54.500 align:start position:0%
what we'll see next and yeah this talk
was<00:15:50.700><c> quite</c><00:15:51.330><c> dry</c><00:15:52.290><c> about</c><00:15:53.120><c> programming</c><00:15:54.120><c> language</c>

00:15:54.500 --> 00:15:54.510 align:start position:0%
was quite dry about programming language
 

00:15:54.510 --> 00:15:56.840 align:start position:0%
was quite dry about programming language
theory<00:15:54.900><c> so</c><00:15:55.140><c> I</c><00:15:55.170><c> would</c><00:15:55.440><c> like</c><00:15:55.560><c> to</c><00:15:55.710><c> end</c><00:15:55.890><c> it</c><00:15:56.100><c> with</c><00:15:56.700><c> an</c>

00:15:56.840 --> 00:15:56.850 align:start position:0%
theory so I would like to end it with an
 

00:15:56.850 --> 00:16:02.330 align:start position:0%
theory so I would like to end it with an
exciting<00:15:57.330><c> math</c><00:15:57.540><c> puzzle</c><00:15:59.090><c> so</c><00:16:00.090><c> here</c><00:16:00.540><c> we</c><00:16:00.720><c> have</c><00:16:01.340><c> a</c>

00:16:02.330 --> 00:16:02.340 align:start position:0%
exciting math puzzle so here we have a
 

00:16:02.340 --> 00:16:06.770 align:start position:0%
exciting math puzzle so here we have a
circle<00:16:03.330><c> plus</c><00:16:03.510><c> circle</c><00:16:03.960><c> equals</c><00:16:04.260><c> 10</c><00:16:05.780><c> circle</c>

00:16:06.770 --> 00:16:06.780 align:start position:0%
circle plus circle equals 10 circle
 

00:16:06.780 --> 00:16:08.450 align:start position:0%
circle plus circle equals 10 circle
times<00:16:06.990><c> square</c><00:16:07.380><c> plus</c><00:16:07.620><c> square</c><00:16:07.710><c> equals</c><00:16:08.160><c> 12</c>

00:16:08.450 --> 00:16:08.460 align:start position:0%
times square plus square equals 12
 

00:16:08.460 --> 00:16:11.570 align:start position:0%
times square plus square equals 12
Circle<00:16:09.120><c> Times</c><00:16:09.390><c> Square</c><00:16:09.900><c> minus</c><00:16:10.740><c> triangle</c><00:16:11.190><c> times</c>

00:16:11.570 --> 00:16:11.580 align:start position:0%
Circle Times Square minus triangle times
 

00:16:11.580 --> 00:16:14.440 align:start position:0%
Circle Times Square minus triangle times
circle<00:16:12.150><c> equals</c><00:16:12.510><c> circle</c><00:16:12.930><c> or</c><00:16:13.200><c> what</c><00:16:13.440><c> is</c><00:16:13.560><c> triangle</c>

00:16:14.440 --> 00:16:14.450 align:start position:0%
circle equals circle or what is triangle
 

00:16:14.450 --> 00:16:25.490 align:start position:0%
circle equals circle or what is triangle
any<00:16:15.450><c> guesses</c><00:16:20.090><c> so</c><00:16:21.090><c> yeah</c><00:16:23.780><c> easiest</c><00:16:24.780><c> pie</c><00:16:25.080><c> we</c><00:16:25.320><c> just</c>

00:16:25.490 --> 00:16:25.500 align:start position:0%
any guesses so yeah easiest pie we just
 

00:16:25.500 --> 00:16:28.370 align:start position:0%
any guesses so yeah easiest pie we just
write<00:16:25.680><c> a</c><00:16:25.920><c> small</c><00:16:26.220><c> solidity</c><00:16:26.790><c> program</c><00:16:27.330><c> that</c><00:16:27.630><c> is</c>

00:16:28.370 --> 00:16:28.380 align:start position:0%
write a small solidity program that is
 

00:16:28.380 --> 00:16:33.440 align:start position:0%
write a small solidity program that is
equivalent<00:16:28.890><c> to</c><00:16:29.060><c> this</c><00:16:30.060><c> puzzle</c><00:16:30.630><c> and</c><00:16:32.150><c> we</c><00:16:33.150><c> add</c><00:16:33.300><c> the</c>

00:16:33.440 --> 00:16:33.450 align:start position:0%
equivalent to this puzzle and we add the
 

00:16:33.450 --> 00:16:36.080 align:start position:0%
equivalent to this puzzle and we add the
conditions<00:16:33.900><c> as</c><00:16:34.190><c> require</c><00:16:35.190><c> conditions</c><00:16:35.730><c> and</c>

00:16:36.080 --> 00:16:36.090 align:start position:0%
conditions as require conditions and
 

00:16:36.090 --> 00:16:38.030 align:start position:0%
conditions as require conditions and
then<00:16:36.300><c> at</c><00:16:36.900><c> the</c><00:16:37.020><c> end</c><00:16:37.050><c> of</c><00:16:37.230><c> search</c><00:16:37.440><c> falls</c><00:16:37.740><c> so</c>

00:16:38.030 --> 00:16:38.040 align:start position:0%
then at the end of search falls so
 

00:16:38.040 --> 00:16:39.890 align:start position:0%
then at the end of search falls so
assert<00:16:38.340><c> false</c><00:16:38.580><c> sounds</c><00:16:39.000><c> weird</c><00:16:39.360><c> why</c><00:16:39.630><c> would</c><00:16:39.810><c> we</c>

00:16:39.890 --> 00:16:39.900 align:start position:0%
assert false sounds weird why would we
 

00:16:39.900 --> 00:16:43.850 align:start position:0%
assert false sounds weird why would we
do<00:16:40.020><c> that</c><00:16:40.050><c> and</c><00:16:40.470><c> the</c><00:16:41.310><c> reason</c><00:16:41.580><c> is</c><00:16:41.730><c> if</c><00:16:42.720><c> the</c><00:16:43.470><c> SMT</c>

00:16:43.850 --> 00:16:43.860 align:start position:0%
do that and the reason is if the SMT
 

00:16:43.860 --> 00:16:48.200 align:start position:0%
do that and the reason is if the SMT
checker<00:16:45.560><c> can</c><00:16:46.560><c> prove</c><00:16:46.920><c> so</c><00:16:47.220><c> a</c><00:16:47.430><c> failing</c><00:16:48.030><c> assertion</c>

00:16:48.200 --> 00:16:48.210 align:start position:0%
checker can prove so a failing assertion
 

00:16:48.210 --> 00:16:50.840 align:start position:0%
checker can prove so a failing assertion
so<00:16:48.990><c> assert</c><00:16:49.410><c> false</c><00:16:49.620><c> is</c><00:16:49.800><c> not</c><00:16:49.950><c> bad</c><00:16:50.100><c> it's</c><00:16:50.370><c> only</c><00:16:50.550><c> bad</c>

00:16:50.840 --> 00:16:50.850 align:start position:0%
so assert false is not bad it's only bad
 

00:16:50.850 --> 00:16:55.970 align:start position:0%
so assert false is not bad it's only bad
if<00:16:51.090><c> it's</c><00:16:51.300><c> actually</c><00:16:51.690><c> reachable</c><00:16:52.320><c> code</c><00:16:52.580><c> so</c><00:16:54.980><c> false</c>

00:16:55.970 --> 00:16:55.980 align:start position:0%
if it's actually reachable code so false
 

00:16:55.980 --> 00:16:57.860 align:start position:0%
if it's actually reachable code so false
assertion<00:16:56.820><c> will</c><00:16:57.090><c> not</c><00:16:57.210><c> be</c><00:16:57.330><c> triggered</c><00:16:57.630><c> if</c><00:16:57.750><c> it's</c>

00:16:57.860 --> 00:16:57.870 align:start position:0%
assertion will not be triggered if it's
 

00:16:57.870 --> 00:16:58.400 align:start position:0%
assertion will not be triggered if it's
not<00:16:58.020><c> reachable</c>

00:16:58.400 --> 00:16:58.410 align:start position:0%
not reachable
 

00:16:58.410 --> 00:17:00.500 align:start position:0%
not reachable
so<00:16:58.830><c> the</c><00:16:58.980><c> SMT</c><00:16:59.400><c> checker</c><00:16:59.640><c> has</c><00:16:59.850><c> to</c><00:17:00.030><c> prove</c><00:17:00.270><c> to</c><00:17:00.480><c> us</c>

00:17:00.500 --> 00:17:00.510 align:start position:0%
so the SMT checker has to prove to us
 

00:17:00.510 --> 00:17:02.960 align:start position:0%
so the SMT checker has to prove to us
that<00:17:00.990><c> this</c><00:17:01.500><c> assert</c><00:17:02.160><c> false</c><00:17:02.430><c> is</c><00:17:02.610><c> actually</c>

00:17:02.960 --> 00:17:02.970 align:start position:0%
that this assert false is actually
 

00:17:02.970 --> 00:17:05.179 align:start position:0%
that this assert false is actually
reachable<00:17:03.420><c> and</c><00:17:03.600><c> it's</c><00:17:04.020><c> reachable</c><00:17:04.380><c> if</c><00:17:04.560><c> all</c><00:17:04.829><c> the</c>

00:17:05.179 --> 00:17:05.189 align:start position:0%
reachable and it's reachable if all the
 

00:17:05.189 --> 00:17:07.130 align:start position:0%
reachable and it's reachable if all the
three<00:17:05.400><c> require</c><00:17:06.180><c> conditions</c><00:17:06.660><c> above</c><00:17:06.930><c> are</c><00:17:07.110><c> true</c>

00:17:07.130 --> 00:17:07.140 align:start position:0%
three require conditions above are true
 

00:17:07.140 --> 00:17:10.100 align:start position:0%
three require conditions above are true
and<00:17:08.060><c> of</c><00:17:09.060><c> course</c><00:17:09.300><c> it</c><00:17:09.480><c> doesn't</c><00:17:09.630><c> just</c><00:17:09.900><c> tell</c><00:17:10.079><c> us</c>

00:17:10.100 --> 00:17:10.110 align:start position:0%
and of course it doesn't just tell us
 

00:17:10.110 --> 00:17:12.319 align:start position:0%
and of course it doesn't just tell us
that<00:17:10.230><c> is</c><00:17:10.439><c> reachable</c><00:17:10.770><c> it</c><00:17:11.250><c> tells</c><00:17:11.520><c> us</c><00:17:11.670><c> how</c><00:17:12.089><c> it's</c>

00:17:12.319 --> 00:17:12.329 align:start position:0%
that is reachable it tells us how it's
 

00:17:12.329 --> 00:17:14.809 align:start position:0%
that is reachable it tells us how it's
reachable<00:17:12.630><c> so</c><00:17:12.900><c> what</c><00:17:13.170><c> are</c><00:17:13.319><c> the</c><00:17:13.439><c> exact</c><00:17:14.430><c> inputs</c>

00:17:14.809 --> 00:17:14.819 align:start position:0%
reachable so what are the exact inputs
 

00:17:14.819 --> 00:17:17.720 align:start position:0%
reachable so what are the exact inputs
to<00:17:15.060><c> get</c><00:17:15.689><c> this</c><00:17:15.839><c> failing</c><00:17:16.199><c> assert</c><00:17:16.500><c> and</c><00:17:16.770><c> we</c><00:17:17.579><c> see</c>

00:17:17.720 --> 00:17:17.730 align:start position:0%
to get this failing assert and we see
 

00:17:17.730 --> 00:17:26.430 align:start position:0%
to get this failing assert and we see
that<00:17:17.910><c> triangle</c><00:17:18.600><c> this</c><00:17:18.839><c> one</c>

00:17:26.430 --> 00:17:26.440 align:start position:0%
 
 

00:17:26.440 --> 00:17:27.699 align:start position:0%
 
okay

00:17:27.699 --> 00:17:27.709 align:start position:0%
okay
 

00:17:27.709 --> 00:17:30.070 align:start position:0%
okay
this<00:17:28.040><c> kind</c><00:17:28.910><c> of</c><00:17:28.970><c> shows</c><00:17:29.120><c> the</c><00:17:29.300><c> power</c><00:17:29.510><c> of</c><00:17:29.570><c> the</c><00:17:29.780><c> SMT</c>

00:17:30.070 --> 00:17:30.080 align:start position:0%
this kind of shows the power of the SMT
 

00:17:30.080 --> 00:17:33.340 align:start position:0%
this kind of shows the power of the SMT
so<00:17:30.260><c> we</c><00:17:30.530><c> don't</c><00:17:30.920><c> really</c><00:17:31.600><c> know</c><00:17:32.600><c> yet</c><00:17:32.930><c> so</c><00:17:33.080><c> it's</c><00:17:33.200><c> not</c>

00:17:33.340 --> 00:17:33.350 align:start position:0%
so we don't really know yet so it's not
 

00:17:33.350 --> 00:17:34.960 align:start position:0%
so we don't really know yet so it's not
it's<00:17:33.680><c> still</c><00:17:33.800><c> experimental</c><00:17:34.130><c> and</c><00:17:34.460><c> not</c><00:17:34.640><c> fully</c>

00:17:34.960 --> 00:17:34.970 align:start position:0%
it's still experimental and not fully
 

00:17:34.970 --> 00:17:36.520 align:start position:0%
it's still experimental and not fully
finished<00:17:35.270><c> yet</c><00:17:35.450><c> we</c><00:17:35.660><c> don't</c><00:17:35.780><c> know</c><00:17:35.930><c> how</c><00:17:36.260><c> it</c><00:17:36.380><c> will</c>

00:17:36.520 --> 00:17:36.530 align:start position:0%
finished yet we don't know how it will
 

00:17:36.530 --> 00:17:39.010 align:start position:0%
finished yet we don't know how it will
behave<00:17:36.680><c> and</c><00:17:36.980><c> very</c><00:17:37.160><c> complicated</c><00:17:38.020><c> contracts</c>

00:17:39.010 --> 00:17:39.020 align:start position:0%
behave and very complicated contracts
 

00:17:39.020 --> 00:17:42.580 align:start position:0%
behave and very complicated contracts
but<00:17:39.490><c> yeah</c><00:17:40.490><c> we're</c><00:17:40.850><c> we're</c><00:17:41.810><c> optimistic</c><00:17:42.140><c> and</c>

00:17:42.580 --> 00:17:42.590 align:start position:0%
but yeah we're we're optimistic and
 

00:17:42.590 --> 00:17:45.190 align:start position:0%
but yeah we're we're optimistic and
let's<00:17:43.340><c> see</c><00:17:43.460><c> how</c><00:17:43.580><c> it</c><00:17:43.670><c> goes</c><00:17:43.790><c> thanks</c><00:17:44.780><c> you</c><00:17:44.870><c> thank</c>

00:17:45.190 --> 00:17:45.200 align:start position:0%
let's see how it goes thanks you thank
 

00:17:45.200 --> 00:17:54.940 align:start position:0%
let's see how it goes thanks you thank
you<00:17:45.230><c> for</c><00:17:45.350><c> your</c><00:17:45.440><c> attention</c>

00:17:54.940 --> 00:17:54.950 align:start position:0%
 
 

00:17:54.950 --> 00:18:02.529 align:start position:0%
 
[Music]