[Music]
hello everyone uh my name is Robert this
is Jack and uh we're currently working
on our Master CIS in computer science
and uh we're working on a new
programming language for the evm and so
we're here to talk about how smart
contracts can be a perfect fit for a
dependently typed functional language
and why we want to do this uh we will
also have a small example of uh how an
expressive type system can help in
contract
development so when you deploy a smart
contract to production uh you want to be
really sure that it behaves precisely as
you intended to um so the more the
compilator can catch for you the better
so we also want to give developers high
level abstraction uh of standard
behavior and common patterns stuff like
high level cryptography and boiler plate
for errors and
cleanup and I hope that after hearing
Greg this morning uh you can appreciate
that a language that allows for
compositionality of combinators and
functions can be really powerful lll is
functional but it's way too low level
for a lot of purposes uh so without
further ado Jack will now present two
types of errors that programmers usually
make when they start developing smart
contracts and how we can catch them at
compile
time right so we look at a simple
example game of rock paper scissors
that's played for money uh joining costs
10 ether and the price is 20 because
there's two
players uh and I hope you know the rules
but it doesn't really matter if you
don't
uh and here is a small example of uh how
the function that lets players join the
game could
look it's very
straightforward um it's the game can
only be be joined if it isn't full uh
the player has to pay the fee and if
both of those are okay we just save the
move and the address of the player and
yeah the move is just represent this Z
one or two for simp
uh so this for a regular programmer this
would seem quite reasonable but there
are actually a few bugs here um so what
happens if a third player attempts to
join the
game he would lose all his ether and
there's no way to retrieve
it so let's fix
this um this is better but there is one
problem
left uh since the blockchain is trans
arent the first player will reveal his
move to the second
player we'll not solve this now but keep
it in mind later so just a quick recap
there's two uh classes of error that
we're focusing on that's very common for
developers that's getting into smart
contract
development uh what we what we're trying
to do is to use an expressive type
system to help identify and solve
this and to to do this we are including
both ether flow and cryptography
directly in the type
system so if we want to encode ether
flow in the type system what can we do
well we can start with including the
transaction value in the type signature
like
this and as you can see we we have also
put a precondition on the value saying
that this function requires at least 10
ethers to be executed
uh otherwise the transaction is
considered invalid for our purposes and
all ether is automat automatically
returned to the
sender and this is certainly neat but it
doesn't solve our problem our problem
problems uh but as you can see we
actually already know uh the functions
result success and the transaction value
value this is actually enough
information for us to specify spe ify
how the function should should handle
ether in all execution
pths so we just take the return value
and do a conditional check on it that's
the question mark and colon there as you
probably recognize from imperative
language
languages uh if the player was able to
join the game we should say we should
save 10 ether and return the return the
rest and if the player wasn't able to
join the game then we should send back
everything and don't save
anything now this type signature
actually causes the problematic
implementation from before to be a type
error that's catched at compile time
this is quite amazing because it allows
us
to uh eliminate a large class of bugs
without doing any testing or formal ver
formal verification
whatsoever this technique can actually
also be used for by contract developers
uh to specify the behaviors of their
contracts but that requires a little
more a little more work on the part of
the developer so we won't go into
this uh but we still have the problem
that uh the move is disclosed when it
shouldn't
be the way to solve this is to use
cryptographic commitments they basically
allow you to commit to a value and then
reveal it at a later
time but Developers shouldn't Implement
their own crypto each and every time
it's tedious and very error
prone so the way we solve this is by
annotating the types of secret values as
you can see there with
commit um this indicates to the compiler
that this value should be treated as a
commitment and the compiler will
automatically generate a function for
the sender to review it at a at a later
time when it has been revealed it can be
accessed in Code by using the standard
Library open function which takes any
commitment and Returns the and Returns
the value if it hadn't been revealed
previous to calling
open uh then open will fail return all e
to the sender and abort
execution uh so our final type correct
implementation would look like this note
that we are forced to explicitly save
all ether that we want to keep because
otherwise it was wouldn't
compile and now Robert will talk about
how we intend to implement
this thank you so some of you might have
noticed that the syntax we have used is
very similar to ascal and when we first
started looking at this we had the idea
of of making hll on the blockchain
basically but the more we looked at U
these problems and how they could be
solved we realized that dependent types
would be really cool to do this uh also
haskill is lazily evaluated which
becomes prohibit expensive in real life
on the evm as it is now and then we
found
Idris uh Idris is very similar to hcll
but it has some key difference
uh first of which it is dependently
typed uh and it has side effects is
model with Al algebraic effects so these
two things combined is what allows us to
have the neat uh uh expressiveness in
the type signatures that we saw
before and Idris is also strictly
evaluated from the GetGo so we don't
need to have make any changes there and
as a nice bonus we don't have to venture
down into the murky depths of the GHC
API if you're familiar with
that um so I hope we have shown how
dependent types and algebraic effects
can be used together to define the flow
of ether throughout execution of a
contract and we'll see how we have seen
how high level type annotations can
ensure that secret information stays
secret until it's supposed to be
revealed and we have a language where
compositionality can can be achieved in
a natural
way so where are we currently with this
well we still have a long way to go
before it's actually usable in practice
to create working smart contract bite
code uh we have created models for how
we want stuff to look for the developer
and made sure that all the properties we
want to enforce can be enforced using
addresses type system and we have just
recently started looking at uh how we
can create a code generator that will
take that will go from midis to lll um
in a similar way the serpent does it
today and that's it for us thank you
[Music]