[Applause]
and has a copy of the slides and is all
the codes that will be raining today if
you watch all along and you can start
from the initial version
where we've written the entire reach
part of the program and it will switch
and then the final code will be the I
don't want this our target for the end
of the day so if you wanted to run a
business how to use the English right
now we have dr. and dr. compose result
and of course how about music music so
you want to go to this site and then
from the base directory villain Tuesday
final write in Greenville run then that
will make sure that you have all these
velvet if you want to all along if you
don't want to follow a just do this
later and there will be value and
experiencing the rest of the show
our team is because we were able to
attend and then maintain McCarthy so
Christmas Carol entrepreneur's had a lot
of experience in the space and my
background is that I am a research
professor at the University of
Massachusetts well and I'm also one of
the developers of the record program
language so a racket is a list based
language that's very popular as far as
list based programming languages go it's
commonly used at a lot of colleges
universities and my research has mostly
focused on doing verification of
programs for calls and there
so the reader product the reader project
really represented the culmination of my
research now our goal as an organization
is to try to dramatically lower the
barrier to entry to watch so we think
that there's a huge amount of potential
in the space but right now it's just too
complicated to build real apps and our
goal is by building something here oh no
that's 40 miles now its pipeline is that
we want to solve three problems we want
to abstract over the decentralisation
important right now
here it is extremely productive is
probably there are many people who
believe that there's problems with
aetherium and other and other platforms
but it's too risky to invest their time
if you rate your product and reach and
you will be able to compile to different
platforms we are trying to we're trying
to live up to the rate was running many
business the next thing we want to solve
is that we want to make sure that the
that the depth that people rank are
trustworthy
so a major important what we'll be
talking about later is the way that
is integral to the operation of compiler
and the way that we've progressed
finally part of being trustworthy is
ensuring that there is consistency
between the expectations of contracts
and expectations of compliance and it
needs to realize that in the recent
languages that it is not a smart
contract English is a bounty which we're
going to break their program in this one
because you get the clients that will
and there's a guarantee the verities now
there are some interesting techniques
that we use design and I'll talk a
little bit about that before we focus on
trade now one of the ways that we get
the abstraction of being able to provide
to go to many defensive centralisation
platforms is that we have a very
straightforward constraint model of what
working provides all right is that we're
thinking of the bunting as providing
common knowledge about a monotonically
and those those attitudes might say they
really like constrain all the ways that
we look at contractor plans to provide
the contract is this repository of
knowledge and the clients react to that
information and attempt to add things to
it if necessary and so what our main
feature is another principle that we use
inside of reach
is that the reach language performs a
lot of sophisticated analysis on your
code at the most basic level we have a
sound tasting as you can expect in the
modern language in addition to that
however we have announced these that are
particular to the needs of deaths as a
one little example one of it we'll see
later is the way that reached uses
information flow security to guarantee
this information that is known only to
it does not share without being
explicitly transplant now the way that
we do verification is that we take the
program written in reach and be
converted into an estimating problems
SMT is one of the classic problems with
either science and there are many
extremely reliable on an apparent
purpose legacy that can plug not I think
discharge and so a major part of the way
that the structure it is to make is that
we can produce as our goal is to provide
any during the process so if that means
that they have to be able to discharge
all the publications automatically and
the only way that we can do that is have
any ideas now we have a lot of different
kinds of properties that can be
expressed inside of these programs at
the highest level we have basic systems
level property relation between all
counts think of like if you're
programming the C program you never want
to have a nullpointerexception and you
don't actually need to know anything
about the program that you're running to
know that it should have that property
so slim early part of reaches tool
automatically synthesized companies like
this would make sense for all others on
the other hand we also have the ability
to break down particular properties of
relevance or one application in the same
way that when you're writing the C
program you'll have a custom assertion
they make sense program so we have the
same letter instead of reach and again
we'll talk about this later now the next
thing is that as I mentioned the reach
language provides specifies the entire
program we use a process called any
collector Junction to extract each of
the individual pieces of the program out
again I'll talk about this in a moment
so that's kind of a roadmap of where I
want to go and the switching dive down
now what does they actually want one
thing which is that reach is the
culmination sorry is the revolution of
another DSL that I've worked on
previously another company making
open-source products called a blacklist
and that other language is called
integrity and the library is also
available and has diverged development
different features in the electric 11
language as the reason language and I
very happy to talk to anyone about what
those differences are but I want to make
sure that I acknowledge they so now what
I'm doing is I'm going to switch and go
over to the repository so in the
repository we go into the initial
directory and this is the code that will
be working on health can you open this
there's been a lot of order fix stuff
that's to make it so that it can run
effectively let me just comment a tiny
bit about this before we open I'm going
to clarify so we need installation to
make it to us as easy as possible for
all look it is everything is entirely
talked arrest
so these run the application certainly
when you compile them even it compiles
it into a docker container that you can
that money that docker container is
automatically configured to a
testamental but it also so you don't
need to worry about that party testing
similarly you don't need to download any
download or install anything like a
regional pilot the regional pilot is the
shelter of redundant bottom which is
eight lines it configures
so there's a lot here that's gonna make
some of those things all together but we
are going to be inside this file right
here multi-state not our name that's
gonna be our meter man here's what we're
going to start off this so in the rich
language you are writing in a subset
observers so the syntax is exactly the
same syntax as JavaScript almost all
normal JavaScript features are available
and they mean roughly the same thing
that there are many so for example let's
start by talking about what we're going
to build and what the overall model of
engagement is we're going to build today
is an abstraction of a multi signature
wallet the key idea of a visual wallet
is that many people collaborate to pool
funds and then when they extract those
funds other people have a say on whether
or not the extracting happens so we're
going to distract that idea to two
accounts a parent and a child
the parent makes a deposit on behalf of
the channel and the child can attempt to
sedate withdraws it must be explicitly
approved by the parent so this is not a
product that when we're done today we're
going to launch and become blocked and
leaners this is an abstraction of what
kinds of problems people
to solve it on the blockchain and it's
small enough that we can do it in
minutes 30 minutes all right so the
first thing that we want to do is you
want to specify that this protocol
involves two different part participants
a child and the parent
it's either each language one of these
you do is you specify each one of the
parties and then we'll write one program
in this main function and this main
function is going to include the
behavior of all the participants as well
as all of the smart contracts so the
first thing that we'll do is we'll have
the child and attach to the contract
we'll do that by having the child make a
publication now the end of watching is
there's this monotonically increasing
data structure of the history all events
or attitudes in this case we think about
that as being a publication to all of
the other parties so when we call child
publish we're saying that it's the
child's responsibility we'll publish
this information now it turns out that
there's actually nothing
originally it's just the way that
they're in now every time when you
expect to see a message on in the
vertical we have the same what would
happen if the person who's supposed to
do this didn't do it
what if they what if they time on prices
and so we always specify what would
happen in the case of the time out and
typos are expressed in terms of how many
blocks you're willing to wait for an
accession so we're going to just have
this variable and program delay which is
going to say the message has kind of
comment in delay seconds and if it
doesn't then we'll fail and the way that
will fail is that anyone as well as
underscore means anyone is able to
submit the message and what this message
does is it will commit the transaction
and then say that we have finished
writing the curveball and the reason
that I'm returning this array of turin
zero is because at the end of the
protocol when we're finally done we're
gonna return how many times the parents
said yes and how many times the parents
said no so if the child times out and
never joins and we're done and so no
event actually happened now after we do
this now the code has transitioned down
here and we're now inside of the
contract so at this point we need to
verify anything that must be true above
the publication now in this case I think
was actually
there's nothing to say so we commit the
transaction and now we go back to a
context where we're outside of the
purple the idea of the reach language is
that you switch between local blocks
where a particular agent or many agents
are simultaneously doing things and then
synchronization or consensus works and
in those consensus works all of the
parties are doing the same thing and
they agreed on all the information of
let's do an actually interesting example
so after the child has joined the
protocol we now want the parent table so
a parent table only so this is something
that only the parent they do now what do
we want them to do we're going to have
them run a function and so we'll specify
that as a function of narrators and what
they'll do is they'll compute what the
allowance that we're going to give us
now notice that this is a circumstance
where it makes sense that the at this
point in the parole the parent is always
going to decide what the allowances but
in our reach program like how do we know
what you do clear parent are going to
give to Sally before she goes on her you
know it's big trouble
how do you know well there's two ways
that we can do this the first thing is
that notice I'm here when I wrote when I
defined the parent I said and this empty
object right here
so in this spot you can write and
at every print that that participant
starts the Protomen
so we could add in here knowledge what
the initial step will do though is that
we will interact with the front end so
we interact this is a special object
inside of the reach language that
represents the client it will ultimately
run the parent part of the world so
we're going to take that object and
we're going to call allowance on it now
let's convert our net value and we need
to assert that that value is going to be
an integer now this value right here we
want to eventually provide it so we'll
go next and we'll say parent not publish
the allowance so we're going to publish
to the rest of the world that the
allowance that that child has access to
is this number now unfortunately if we
try to compile the program right now it
is going to fail and it's not an ability
because I have this time here it's got a
billion records that the reason it's
going to fail is that this program fails
to satisfy the information flows of
dreams the reason why is that all the
information that comes from the client
comes from the front end is assumed to
be standard information
it must be it
classified so we'll do we'll call do you
classify MS and another Declassified in
we're allowed to watch it okay now the
next thing that I want to talk to you
about is how every time we make a
publication we can combine that with a
unit of value that we transfer it to so
so will actually pay the allowance and
will write down the time code so every
program every interaction on the chain
must be accompanied by what would happen
if there's a timeout we refer to this
property as kill safety the idea is that
your program has to be safe with respect
to any participant refusing to engage in
the protocol at every point going
forward so in this case what we're
saying with this time of luck if we're
saying what if the parent never did this
problem what should happen now do these
early stage of the protocol there's
really nothing interesting to say that's
why they just had but in principle as we
go forward there's going to be more
interesting interrupts they're going to
happen
all right so now at this point you're
now inside of the contract the contract
has access to the allowance and you need
to go forward the thing that we want to
do going forward is what to have a
little well and this little while loop
is going to repeatedly allow the child
to ask a buzzer so we'll write about
now what is the condition that's going
to tell us that we're done well the
condition was going to tell us that
we're done is that the balance is going
to be zero when the balance is empty
then the program will be over now Alice
Bob something like special variable that
we're not going to we're going to keep
track of the balances okay so we're
gonna say that well the balance isn't
zero continue running this part of Seoul
define a new variable call the balance
it's going to be equal to the allowance
no just so that we have something
interesting to return to do is we're
going to keep track of how many times
you said yes and how many times you said
no running the program so how many times
the child asks for money and the parents
that way we don't this isn't that
important you just keep adding something
and then that's the information that
we're going to return at the end
okay now there's one last thing that we
need to do and it's actually kind of a
big thing when you're doing formal
verification and you have a value the
while loop represents a point in your
program where many many different things
to cover there's an addition of this
program that runs where you reach this
point in the allowance with zero and
since the allowance was thrown we never
execute the code inside of here and we
go right to the end there's another
version of this program of this program
executing where we run the inside of one
time then after running it one time it
all balances fun and then meetings
there's another version we're gonna run
it two times sometimes so there's some
times an infinite number of different
ways to run a program that has a single
level I don't know how many times you go
around the mouth so it's a big problem
how are you gonna know what the program
will actually do because the way to
think it's a way to internalize what
program is is you're making a prediction
about what the program will do now one
way that we could do this is that we can
automatically take the program and
verify it for when we went 0 times
verify Poneman 1 verifiable 1 2 3 4 5 6
7 8 9 10 etcetera and what we would be
doing is we will literally be like
copying piecing this code inside of the
verifier over and over again to verify
each one of those different versions
that's called interject evening
and intimidated is what to do in
situations where we can't figure out we
do not either
instead we have a programmer specify a
loop invariant now if you remember from
your analysis of algorithms course we're
you to use the CLN respo excuse
computers I hope you've probably learned
a lot love with veneering and if you're
like me you hated that class and it was
very frustrating okay mostly I do have a
little bit Marion is what do you know
before those nerves and what you know
again another thing that we know is that
the balance in the contract is equal to
this balance okay and anything that we
do inside of this that and will not be
like will not be allowed to compilers
and what this is gonna do is it's gonna
allow the compiler to make it to verify
this mortgages we're gonna verify
everything above this to make sure it
establishes Levin great we're gonna
verify the inside to make sure that
preserves it then we're gonna verify the
end and then also air but what this
means is that we provide complete nerve
agent
behavior of your program by just proving
three smaller girls it's not let's go
inside and do some stuff so we were in
kind of the context of the consensus so
we have to commit the transaction and
that will go back to the world where the
two participant do something and then
they want to do is want the child to do
something or something where she's gonna
ask for a certain amount of money and we
know that this money will start be
classified and it's going to be a number
and will interact interact with a
customer sorry-sorry the front end to
request the money and the way that we're
gonna do this they said we're gonna tell
the front end how much money is in the
account it's okay
you know know how to display to the user
yeah Sally do you have a hundred dollars
of elders how much do you want
so this internet object is not only a
way to get information from the front
end it's a way to share information so
it's a two-way street essentially what's
going on is that this breach program is
specifying the API to the contract the
API to the clients sorry that they've
got to the backend then we'll write up
some client
now the next thing we need to do is
write an assertion that's gonna say that
how much had better be stronger than or
equal to the balance because this
program would make sense in that
production business function right here
is one of the verification assertions
that we can put out I mentioned before
you can go look at the slides that you
might enter that there are different
kinds of a search assertions are things
I always want to be true if they're not
refusal in compile assumes are kind of
like require insulin where we obviously
check this property at runtime but the
other thing that we do is we make sure
that all the assertions later on in the
program are entailed by these
assumptions so later on in the program
were allowed to write down a service and
if any ascertain would fail because you
forgot one of these assumes then will
refuse to compile the program the idea
is that we're guaranteeing consistency
between the clients and the contracts
we're making sure that your program at
runtime actually verifies all the
properties that are necessary for your
contract to run so now what we'll do is
we'll have the child publish mmm
then animal ready the time ability and
the type of food will be a lot of
available to the parent to run and if
she fishy times out then we'll just say
that it is an automatic dignity
so it's not an it's not a yes or a No
but we just continue the purple so what
happens here is that rather than
returning at the end we say that all of
the variables that the loot is iterating
over they stayed up in the statement and
then we continue to the next generation
if we wanted to we could say that if the
time what happens then it like goes in
favor of the of the child that she had
for me they talk to us and we do this by
the way is one of these one of the one
of the examples that the reach language
is different from my earlier project the
elaborate language because they have
that pretty language the timeout locks
are automatically generated upon ear and
a half they're not able to but also you
don't have to specify what they do so
they automatically enter protocol to get
all the money okay so now we're inside
of the contract and we will require that
how much is less than the balance
so this vertical only makes sense going
forward and how much it is not more than
that once now it looks like what we're
doing is we're saying something twice
we're setting about here coursing event
here and of course we've literally
ripped down how much less than miles two
times what we did it for totally
different reasons what we're doing right
here is we're saying that this protocol
makes no sense
unless this is true what we're saying up
here is that I am a bad client if I
don't check this properly and you have
to specify both of those things if you
want to have a current program because
you're writing down the client and
you're writing down the content and one
of the thing we'll do in the
verification process is make sure that
the contract only interacts with good
clients so if we left of this line and
this line will fail to verify and it'll
say that because of course in the actual
and like your actual project you don't
want to submit a transaction and how
that transaction will fail because you
failed okay so then we'll forget the
transaction and now we're back to the
local context and we'll have to parent
oh I know this is approved
in this case we'll get back to moving
because the interact on there doesn't
only the turn numbers can return
arbitrary information so will the
interaction will say all approve and
will tell the front end here's how much
she asks for it here's what the
remaining balances then what we'll do is
we'll publish that and we'll have to
deal with what happens if there is a
timeout and we'll do the same thing as
before where is that if there is a time
of the parent never gets around to it
and in this case we'll call that a note
and
okay so now we're back inside of the
context
45:34 the contract and now the contract
knows the balance it knows how much
money was asked for and it knows whether
the parent degrees so at this point we
can actually make this transaction so
we'll say if the approval is true then
we'll transfer how much to the China and
we'll update our state areas say that
the balance is less than that how much
we'll say that there's been a one that
is called yes and no notice and then
we'll continue and otherwise what will
do it will say that the balance is
unchanged
okay is unchanged but there's
and we'll continue and then at the end
we'll need to commit the final
transaction when the balance is empty
and then we'll return the OTAs in the
mix okay so we just fruit 63 lives and I
hope that it belts not to beard it
doesn't feel like rating saluting it
doesn't feel like writing a smart
contract it feels like reading the whole
done behind the scenes what we're going
to do is we're going to automatically
synthesize the front end code and we're
about to synthesizing a contract out
let's go to the terminal and see what
type of a name and then so we'll take
make building and what it's going to do
is it's going to run the compiler oh I
made no mistakes so I don't know about
you guys but I'm a master and a lot of
the time my students make mistakes when
they write paragraphs okay this is why
you shouldn't hire them to write their
verified compilers you should hire me to
write over
first time now let's me go back for a
moment and look at what we read now what
if we made a mistake
so obviously this it would be totally
stupid but what if we accidentally
subtracted how much and then added one
there's no off by one error in our
program now I've never made not that
whatever program but I've heard of it
okay let's try to compile and see what
happens
I'm suspicious that maybe it's not
looking in smile hmm okay I'm really
nervous one of the one of the annoyances
with doctor is that sometimes doesn't
copy
ok hold up talking about that for a
moment what I'm going to show you right
now is what we make what the compiler
produced so if there's an adult
directory and we'll look at the saloon
because it was generating so right now
the reach language can in principle
produce things other than a theory but
right now the only part of the theory
this is the contract that came out so
this program this contract is come
certainly laborious embers so there's
100 nod2 lives you can look at if you
want to send them to the Builder
everything right in yourself and let's
just look at like one little part of it
so let's look right here at message six
so message six is a message that has all
these parameters and let's try to see if
what's going on so it says right here
that it must have come from a zero that
the block number is less than the delay
going in there the value has to be 0
that's one of the messages that doesn't
have a payment with that over these 17
has to be smaller than to be aimed of
least 17 that's how much he ate was the
balance then what we do is we commit
that and then update the state
so with this messages this event number
six is the six thing in our program
which is this step right here and this
publication right here when the child
says here's how much I want and when you
go to the contract we require that how
much does my eye care I realized by the
way why the by that allowed us to
comment on that line because actually
commented out the line that that was the
assertion rather than the line that made
sure the assertion was right so I
believe that if I comment about this one
all right now I'm not really nervous
though
Hey sorry okay so
now let's look at the image options that
they generated so this the structure
could have generated is the code for the
child so we get a new it's called child
that takes as an argument that hand over
the contract will see this given a
leader and the interact object and then
it goes through and it has each one of
the pieces of the program so just make a
new window we can compare the two of
them so for example look at the first
one that took the child does the child
calls requests on the Internet so the
very first thing is that we published
nothing and then we're going to wait or
the parent to publish the allowance so
we look at the code the very first thing
that happens is that the child sends and
then receive special message one with no
information expecting to receive event
one afterwards or event two of those
entitled there was talent nobody do is
mean to you or both remember we expect
to receive event three and event three
comes with these five this
that will end up being the allowance
okay so this rest of the curve right
here is you know no code that a human
would ever write but it's very
straightforward about compilers it has
wonderful things like let V 9 equals 0
because let's be 9v9 is the count for
how many times we said ok alright so now
what we've done is we've written the bar
for every reach we've compiled it behind
the scenes it's done verification for us
and we now have the Johnson poop and we
have this ability code but this
javascript code that we have the only
thing that it does is it provides these
high level up these high level functions
to spin up a child and twos enough the
parent may skip down there's a limit
parents and then we also and then you
know the details of the contract know we
have eight minutes left so we're not
going to break by in the front encoder
instead I'll show you the front so what
I'm going to do is I'm to go out of the
app directory and go is the minimal
directory and don't look at the index
MJS file so the first thing that we'll
do is we'll import the standard library
we'll import that noticing for them
well Sid our starting balance and then
to be
we're going to test assignment and then
we'll scrape a new account for the
parents that have that starting balance
and then that's going to deploy the W
parent unemployed then what we're going
to do is we're going to define the
internet project and for this first
version I'm gonna say that the allowance
is always going to be fifteen there so I
just write this function that money that
when you get that pause with allowance I
return to the beaver now if I we're
making like a real application you know
I might have a pop up for ever and oh
you mean like actually do a real
interaction with music then remember our
approval function and our cool function
this is a really nice parent aircrew
function is true okay because this is
just for testing purposes okay then what
we'll do is we'll define a logo that
will run the parent function so the
whole month is it but can't give it this
contract object that you might have to
play into that interactive function and
then we'll get back a promise for the
answer that will eventually come out of
the parent when it's done right and to
do something similar to the child will
start it off with the balance and just
because I'm lazy in this test I mean to
start in exactly the same so and you
have some money to provide the gasoline
then the child will attach to the
multi-state contract and when you attach
versus deployed he doesn't say what the
address of the contract is and when it
was created
you need to know what it was created to
the you know they're not sending people
now the child it's gonna say I'm
ingredient Island what I want to do my
request is everything and then we'll ask
for it he apparently will wait those two
in there let me just pop back to the
comment over to turn over here and we'll
make run
finding out that that meant starting get
waiting for it to be around I mean this
the texture here
that's actually running it
really nervous in my life demo now ended
and it said apparent up there okay so
what this coach shows us is that we have
28 lines and we're able to take our
noticing program that we wrote and write
the rapper front-end so this code is the
minimal amount of traveling code that we
would need to write have something
useful in to take this structure right
here
and you can build your unit testing
library for this between there now now
let me show you one more version that
does a little bit more interesting stuff
so what this person is gonna do is it's
gonna be 41 lines so it's like twice as
long and we're just going to do is it's
my two messages about what's happening
and other that's gonna be different is
is that the parent is going to say that
you can have any time you ask for money
as long as you can ask for less than
half of what's left will say yes
spatulas you can ask without much much
as
and though the child is going to do it
as a child is going to ask for a random
amount of money that is divisible by 8
dollars life
it's a liar why am I doing this just let
it over to love life the child
particularly asked for random lots of
money and needs until eventually it gets
down to the point where there's only I
think one eater left and then it will
end so this new version of the permit is
going to be more like exciting to watch
we're gonna mean but really all they're
showing you is that I'm not developing
that happening work I'm making a user
interface I mean the policy for what the
parent doesn't mean you can policy or
what the child does be here is an
automated policy but you could have it
be instead not automated one the one
that's right by and we'll build in - and
I love
and make the text a little bigger so you
can really experience okay so they
deploy the contract okay that's great
put in 50 ask your not okay but one of
this come in look at all this money this
right now it's like there's lots of
times actually have paper and then it's
ready for a while this is gonna get down
to the point where there's only one left
it's gonna take a while we get positive
payments awesome plus the parent said
yes 13 times and no 13 times the child
so what we did today is we wrote an
entire down from start to finish in 30
minutes
now I program
there's no point at which I said here's
this complicated solidity idea to a
Titan call or is it transfer it is
supposed to be send let me go looking at
Stack Overflow question again these are
the kinds of things that are done that
are decided before you correctly buy
them from Heather one point the next
thing is that we verify that the data is
trustworthy or at least we would have my
doctor configuration was writing copy
the files correctly so you want out send
you well then we'll post a link to a
version of this this walkthrough where
we show the verification condition was
failing and then and it ensures that the
clients and the contracts rating system
art for T lying reach program produced
300 lines of front-end Java code and so
the code and the details of those two
programs have to mean the mentalist be
connected with one another to make sure
that it executes correctly now obviously
you like everything pretty simple 300
lines that has to be right if you broke
a real program not this little model
there is
help right now we have our data that has
many different many constraints later
but and we have a release plan for over
the next year to expand the 72 though
I'm very grateful for you to come here
please check out our website realization
is look it up on Twitter and all the
social platforms you should really check
out an Instagram account I've got a
really cute cat and finally I just want
to see exercise and reach was only a
project that I worked on that's based on
the same principles and so thank you so
much for your time
[Applause]