when you design a programming language
you have to make compromises constantly
there are people who request features
and of course features are nice but with
each new feature the language gets more
complicated and thus easier harder to
understand and it's easier to make a
mistake the more complicated the
language is so you have the constant
balance between functionality and safety
of course there are features that are
safe but yeah that's the compromise you
have to find and this has not been the
case for general-purpose programming
languages for several years now but in
blockchain there's always the factor of
cost so smart contracts have to be very
cheap to execute and that also limits
the features you can add in a language
back in the days when solidity was
started the initial goal was to create a
usable high language high-level language
as fast as possible and I think we
succeeded in that but of course we made
some decisions we now yeah which turned
out to be not that not to be the best
decisions and now is the time to change
them and solidity is still a language
that changes and that allows us to make
the necessary changes to the design and
yeah the the path you want to go is we
want to keep features that are
relatively safe and we they look like
high-level features but most of them are
actually quite low level so we want to
have features that that look like here
look look like high level features but
are still cheap and we want to remove
everything that
can surprise users or has some semantic
involved and then a third factor is we
are adding formal verification tools
that are easy to use and this I would
like to stress this easy-to-use part
because that is essential and we will
see that later in the talk and then if
there is not enough for you we provide
direct way to access very very low level
features of the etherium virtual machine
and the important point is here that we
remove everything that is kind of
intermediate level so for example
address dot call will be removed in the
future because it has some magic some
some unexpected things involved that we
would like to avoid so if you want to do
such low-level things you have to go all
the way down to the human virtual
machine ok this is kind of the the path
we want to take now let's talk about
some new features we added in the last
year this contract here is a simple
database that stores people by an
identifier a name and some flag that
says whether they are owner of something
and you have a function there which
allows you to add one person to the
database it already looks quite
repetitive and but it gets even more
complicated if you want to add a
function that can append a list of
people into that database the problem
many people run into is that you kind of
have to create an array out of these
three things here and what you usually
do is that you add three parameters
which are each an array this of course
creates the problem that you have to
check that all of them have the same
length because you have an ID that
corresponds to name and this flag this
looks really really ugly but fortunately
now what you can do now is hope sorry
what you can do now is this and we added
structs as a central feature to the ABI
which allows you to actually put just
we passed this truck from JavaScript
into the contract and remove all this
these weird repetitions and of course
you can also return an array of structs
so this is not this is not yet available
but yeah thanks so we hope to get that
fully functional by the end of the year
so and the way we the way what this this
was possible while was through a change
in the compiler itself so we we could
have done that the old way but we
decided to do a full rewrite of the ABI
encoder and decoder and this is a
snippet of the solidity code generator
and how it looked before this change
yeah this also this is also really
really ugly the EVM is a stack machine
and because of that you have these this
pop and to operations and in the code
Ranieri you constantly have to keep
track which variable is where on the
stack and because of that we have these
comments and it's really really
complicated to understand what this code
does and also complicated to write new
code and this is how it looks now and it
leverages a new intermediate language we
introduced called Yulia Alex talked
about that I think yesterday or the day
before yesterday so I will not go to
into 10th about that but you see this is
really really readable it has variables
you know what happens you can use names
we have for loops and so on and what you
also see is you have these angle
brackets here and this is because this
is an intermediate language mixed with a
very very simple string templating
engine to make it more flexible what you
see here is the full function to do any
encoding of an of an array into the the
ABI
so it does handle memory arrays call it
arrays storage arrays arrays of arrays
arrays of constant length arrays of
dynamic length and so on and the way it
works is that for example here at the
top we have length equals length fun and
at the time of compilation this length
furnace report is is replaced by the
name of the actual function to retrieve
the length of the array which is of
course different for static resized and
dynamically sized arrays okay and a
language becomes more and more useful
the better tools are available for that
we already see that by in the questions
that were asked in the previous talk
remix got gigantic updates I think yang
will talk about that later today we now
can track variables have breakpoints see
references of variables and I think soon
can also rename variables and so on we
have an way to export the ast which is
the result of the of the parsing step
and these this allows many new features
and one of them is a tool to do code
coverage not based on syntax not just
based on lines but on semantics so for
example is a less than operator actually
tested to do what it does and then a
standard JSON i/o this is a way to get
more fine control
fine fine grained control about the
settings of the compiler yeah then I
have a very special announcement to make
and this is that the solidity
documentation that we only have in
English for now is now also available in
Spanish so please give a big round of
applause to these five people who
these five people who did that in their
free time just as voluntary contributors
I think this is really important to make
if you remix esse below the world and
languages like so like like Chinese or
Russian should also have a their own
translation of the documentation and I
want to spend the rest of the talk on
formal verification of solidity and I
think I showed this slide to you last
year in Shanghai
this is a smart contract and it has
comments which allow a formal proof that
the the some of the balances in this
token contract never changes and the way
it works is that the smart contract
kannst gets translated by the compiler
into a language called y3 and it mixes
this translation with the with the
comments you have here and then you run
an external tool on that to create the
proof that the balances are constant the
sum of the balances are constant but
what you see is that there are almost as
many lines of comments in this code as
there is code and you also see that the
these comments use a language that is
slightly different from solidity so it
requires you to learn a new language it
requires you to learn how to use these
tools and this is this makes it very
hard to use this formal verification
tool and the harder it is to use the
easier it is to make mistakes and also
it is easier for so for Mara fication is
only useful if people understand what is
actually proven there so the statements
that are proven there have to be
understood by humans and if that is not
possible then nobody will use formal
verification and it's useless and
because of that so yeah
perhaps that approach was not so great
so we took a step back and reconsidered
how it looks now is like this we've
replaced y3 by a tool called an SMT
solver SMT solvers are less powerful
than general theorem provers and because
of that the smart contract in this smart
country we cannot prove that the sum of
all balances is constant but we can
prove that the sum of the two balances
that are modified is constant so what
happens here is we have a require
statement which is yeah doesn't have
much to do with the formal verification
this is just the regular solidity
requirements require statement and then
we store the sum of the two balances in
the before variable we perform the
modification and after that we check
that before equals after and this is a
regular solidity assert so if the sum of
the balances is not the same then this
will throw an exception at run time but
using the SMT solver you also get a
proof at compile time that this
assertion will never be triggered okay
more specifically what happens is that
so you can use this tool with require
statements to have expressions that you
assume to be correct and then the tool
proves that there is no assertion that
fails there is no overflow or underflow
in your Matic operations no division by
zero no constant conditions no
unreachable code and whatever we will
come up in the future and so let's take
a look at a simpler example this is the
experimental feature and because of that
you need this first line that activates
the SMT checker
and yeah the function here it just takes
two numbers and adds them of course
there's a problem because we can't
create and we can have an arithmetic
overflow here in this edition and this
is exactly what the so if you run the
compiler on that then this is the
message you will get and
the great thing about this isn't you
solver is that it has so it's more
limited than y3 but it has a feature
that y3 did not have and this is the
following so you if an assertion fails
it tells you why it fails and I think
this is really important because
otherwise people say ah I don't know it
doesn't work but okay let's just let's
just comment it out or whatever throw
something at it so that it doesn't
complain anymore but this tells you why
it fails and kind of forces you to think
about this edition and think about why
it might create an overflow and then
take the necessary steps to prevent the
overflow before it happens there are so
currently what people often do is create
runtime checks about overflow at runtime
checks about overflow in arithmetics but
this can be really dangerous because if
you end up in a situation where you you
have an overflow because of some yeah
internal mechanism of the smart contract
then it will be the the smart contract
will be stuck because it will always
throw this exception because of the
overflow and you perhaps can't get the
money out or whatever but if you already
get the warning at compile time before
you deploy your contract you can think
about why it happens and prevent this
from happening in the first place and
how are you prevented this like this so
you had a require statement which of
course in the end has the same effect as
if you would just check if there is an
overflow but the benefit is that you see
that there isn't there's an additional
condition that is present about these
numbers a and B and the SMT solver will
now see the require statement take these
conditions into account and then check
again whether the overflow will happen
and of course it sees that a number less
than 2 to the 100 plus the number less
than 2 to the 100 will be less than 2 to
1356 ok yeah let's take a look at
another example this is taken this is an
actual example from the underhanded
solidity coding contest where there was
a loop that used an unsigned variable
and decreased it but checked against
equaling zero and of course this loop
condition is always true that's of
course something that can be detected
from the type of of the variable alone
and you don't really need an SMT checker
but yeah I this was a simple example to
present here and it can do much more
complicated conditions and yes this is
what we'll see next and yeah this talk
was quite dry about programming language
theory so I would like to end it with an
exciting math puzzle so here we have a
circle plus circle equals 10 circle
times square plus square equals 12
Circle Times Square minus triangle times
circle equals circle or what is triangle
any guesses so yeah easiest pie we just
write a small solidity program that is
equivalent to this puzzle and we add the
conditions as require conditions and
then at the end of search falls so
assert false sounds weird why would we
do that and the reason is if the SMT
checker can prove so a failing assertion
so assert false is not bad it's only bad
if it's actually reachable code so false
assertion will not be triggered if it's
not reachable
so the SMT checker has to prove to us
that this assert false is actually
reachable and it's reachable if all the
three require conditions above are true
and of course it doesn't just tell us
that is reachable it tells us how it's
reachable so what are the exact inputs
to get this failing assert and we see
that triangle this one
okay
this kind of shows the power of the SMT
so we don't really know yet so it's not
it's still experimental and not fully
finished yet we don't know how it will
behave and very complicated contracts
but yeah we're we're optimistic and
let's see how it goes thanks you thank
you for your attention
[Music]