program many things can usually still go
wrong like we say a cosmic ray can hit
your memory and a bit flips that can
happen well maybe you can use some
service or crowd and so on and then when
you use remote machines there are
administrators with physical access so
they can do bad stuff and what a machine
itself might have bugs and a cat might
break a cable router cables stuff like
that so there are many many RC
uninteresting reasons for program errors
but a single cosmic ray particle
whatever cannot probably break the
atrium network because that can only
affect one node and if that I mean for
cosmic rays to cause a serious trouble
where thousands of particles must arrive
at yes and they needed to hit
simultaneously the same a memory cell in
many many different machines and so on
so it's name is kind of resistant to
many uninteresting features so bug free
programming makes sense in this room the
same there because in other places
before you remove all bugs perfectly
your weakest link is no longer
programming programming errors there are
some other non interesting visions but
to worry about what in Israel you can
still well you it's really really
difficult to get get other weakest links
so here my aim is to match what happens
and how a program looks and yes I want
to talk I have to talk about what
happens
in contracts this is just one mental
model it's just one way of thinking
about it but will some something cause
your contract first with an input on the
SEO contract as some states state and
something happens and an output is
produced something might contain coding
other contracts or sending in so
whatever but an output comes out and
there will be a contract state after the
core is there other hospitals were
category theories here Wow cool
yes greetings I stole your ideas and
then so this is my mental picture so and
I translate that literally into program
syntax so on the Left this is what my
contract here should do where it starts
as a contract a and when somebody calls
function if I want to call function if
that's the input when that input comes
in zero is returned and it becomes
contract B and when it's caught again it
returns one and it becomes contract see
when contracted C is called it returns 3
becomes contract a and so on and that's
kind of literally reproduced here as a
text and well when the contract a is
called with f as the specifier then it
returns 0 and then become B & B returns
1 and becomes G and she returns then
becomes a that's kind of straight word
and then well so I did I did it it I did
it with three different states but
that's very small state space well maybe
a contract should hold numbers so when
you call it each time you call it the
account increments and it returns the
previous counter number that's kind of
implementable so instead of having just
one alphabet
I say it again so many contracts define
game so here I'm showing stage for
contract called vault it's like all
right it's a personal wallet but it's
trying to solve is well somebody might
steal your private key so the solution
here is involved different kinds of kids
one is called the vault key the other is
called the recovery key by the way dia
this idea comes from III people and so
it was an example for a new Bitcoin
script primitive but well from there
people implemented in Israel and so on
stuff happened I'm taking these ideas so
the vault key is your usual key to get
your money out of the wallet
can core unboard function with the abort
key and then your contract enters a
special state you have to wait for like
three weeks or four weeks some some
amount of time written in a program and
after that you can call another function
called redeem and then a payout happens
to the address specified in the unboard
core why did eight weeks because well
when somebody steals your border key and
the course this on board
well you can check the contract every
week and then if somebody else is trying
to get your money you can reach your
more important key called the recovery
key and you can call recover and you can
cancel this and world core and moreover
you can change this border key so you
can create a new key as you have new
vault key and then the attackers
attacker cannot do anything about with
this old boat key anymore so that's the
idea
and then well when you are really really
under key the attacker can still both
his vault key and the recovery key then
what would happen is both parties try to
withdraw the money but both party
buddies keep canceling the other party's
request so it that would become become a
stalemate to make it as priests explicit
days destroy method and when anybody
with the recovery key holds the destroy
method the contract enter enters the
destroyed state and from this destroyed
state nobody can get anything out of
this contract this kind of cancels this
notifies the incentives to steal any of
these kids at most I mean we've used
student both kids you will
probably get nothing
that kind of chases thieves away that's
the idea when you implement it in 3d you
can do that and then you want to check
if this contract if this code matches
the state diagram I drew for checking
that first I have to identify what
solidity state correspond the states in
boxing's in the state diagram so in this
case it's easy there are only three
states when destroyed boolean is true
it's destroyed otherwise amount is zero
it's the normal state if this number is
not zero it's unbolting waiting state
this is not hard but it certainly
requires human judgment and then after
that after that everything can be done
kind of automatically because this
involves no loops but for doing that
first you have to look at the
constructor okay it returns the usual
state not to any other state that's good
and then you have to read the rest of
the program three times because starting
from the usual state well which function
can be colder you have to check all
interface functions because they
anything can be called from anything can
be called on any state by default so you
have to check whatever happens from each
state for each function and then the
default function is called the state
doesn't change so from usual it stays
usual okay
when unboard is called so the state can
become unbolting but if the argument
amount is zero it can stay in usual
that's not wrong in the state diagram so
I put a question mark and then if you
when medium function is called it
doesn't do anything then when I know it
touched something it does something
actually it sends you know it sends some
zero amount of visa to somebody and
becomes user so it's again questionable
behavior and when we cover is called no
it doesn't do anything so that's good
and when this choice is called it
becomes destroyed that's good as
specified in the diagram and I have to
do it like three times when the contract
is in unbolting state that means
destroyed is forest and unbolted amount
is not zero yes you can call this on
board again well I know okay well you
can call the default function that's
fine
you can call so call the unbolt function
again that was not join the diagram is
that fine or not I have to think again
when we deem function is yes this can
become user that's fine as specified and
when we cover is code it goes back to
usual canceled in this waiting request
that's fine
when this joy is called it becomes
destroyed that's fine and then the rest
is kind of easy because everything every
every interface function is prefixed
with this modifier not destroyed not
destroyed so the core is aborted nothing
can happen from destroyed that that was
the easy case but anyway I had to read
the program three times because of the
state of diagram hardest
boxes that's not efficient
so essentially viewing a program takes
at least the number of states times the
number of kinds this is not only for
human reviewers but also for any
automatic methods that's not good and
when you try to check the same thing for
a bamboo program it's easier that's my
claim you have five arrows in the state
diagram and you have five become rages
in the program
so essentially you need to check which
one corresponds to which and from the
user state there are arrows going up out
one is going to important when the other
is going to destroy and the yes man is
going to unload and the other is going
to destroyed from the unbolting state
there are three arrows going out on the
yes there are three becomes raises so
it's much easier to check the program
corresponds to the state diagram um it's
kind of cheating because I chose this
format of presenting states and I chose
the syntax of writing programs it's kind
of obvious interesting thing is how far
I can keep this discipline they want
want more features and along the way how
much I can keep this kind of discipline
that there we are a challenge but I
needed to write something useful so I'm
already adding some features I don't
like that I don't I I generally don't
like to add stuff to this world which is
already a mess but I wanted other
features so sometimes I wanted to call
other addresses
but I didn't want three entrance so
currently whenever you call something
you have to specify what happens in the
entrance in case of the entrance and
currently only abort is supported so
whenever when whenever your contract
causes something and that thing calls
back that about eventually I want to
write something else here but you can
create a contract that's a deliberate
choice because I contract simple so I
think I added there is I want you to
implement the ERC 20 and it's kind of it
seemed to necessary to add some kinds of
arrays I didn't like that because here
you have an assignment you can modify a
particular storage location here I don't
like this at all
when you don't have a race bamboo has no
assignment at all because I mean
everything in the storage just appear
appears in this becomes phrase here I'm
introducing side-effects I don't like it
at all but ok where people want to use
tokens and the tokens kind of essential
feature to control implement ripped
economic mechanisms so I'm not quite
happy I'm not completely happy about
adding this but I did what's missing
language specification and independently
interpreter these come first because
whenever I have a chance I keep
complaining that solidity program has no
meaning until it's compiled into EVM
bytecode
I really have no specification you know
the okay does the documentation but it
doesn't tell you if your program is
executed from from top-down or bottom-up
if you believe it's executed from top
down you're just you know imagining that
and you don't know what how many other
things you just assuming so I I say this
always and this applies to the bamboo as
well currently I'm not happy so I want
I'm writing specification and also an
independent interpreter I know this man
is not in progress language
specification is in progress but okay
well if I done the K framework I can do
this at the same time so maybe I should
just talk to these guys
I don't want to add many features may be
the most prior one is coring externally
defined the contracts once this is done
the language is kind of usable so maybe
I should have delayed this until the
other parts were done so here's the
famous phrase by Simon Payton just avoid
a success at all costs
yes I stole this race from the Husker
community but this is kind of ambiguous
success at all costs avoid at all cost
I haven't decided yet here's how you can
help like you right okay
please talk to me thank you very much
[Music]