Virgil dr. Virgil Griffith and Vikram
Verma will present designs for the L for
contract Pro make programming language
based on deontic modal logic hello
everyone so we're working are we sitting
down you're going to sit down okay Suzy
doesn't sit down so we're gonna ice can
go to our first slide I mean this is
actually so there's me a lot of math in
this talk just like accept it
where's our slide well okay well tell
what the meantime so we're here to tell
you about we're developing a brand new
language for contracts and so so from a
company called legalese legalese calm
legalese is an open source project with
with delusions of one day being a
start-up and so and so originally so you
talk to us all there so I'm kind of the
face and the Crim here is is the brains
so we can we can just go ahead and going
straight and we can go to the next slide
and we'll tell you about the gist is
there a clicker oh okay wait buttons
okay great all right so yeah so so we
are giving you a lovely start up here um
so so originally our goal was to make a
little programming language for for
lawyers to use so so the idea is that
you would write your little contract in
a high-level language you'd hit the
compile button and you would get English
legalese out of it and that was kind of
like the big idea and so so I was
friends with italic over here and they
were and and and they were doing even
more sophisticated things with formal
verification so there's a nice joke the
joke is what do you call runtime
debugging of a smart contract and you
think about it and the answer is
litigation and you know yeah I know I
know it's funny but no it's actually
totally true totally true so amazing it
means that if you're have your smart
contract
having runtime errors is like crazy
expensive
and maybe you just can't have them so
you're like okay well how do we do it in
other industries like say a hardware or
space shuttle's where your runtime
errors are like just not okay because
you lose like a billion dollars so yeah
so you left for your vacation and so
we're like oh well let's go take all of
our stuff for lawyers and give it to
your to give it to you etherion x'
because you're probably gonna be our
power users and you need it even more
than the lawyers do so yeah so here we
are the so we're making a custom DSL
just for you no permissions obligations
surprisingly enough some of the lawyers
are actually they're already biting into
this you know we said it'll be
technophobic but hey someone can some of
them actually get it and so this is like
you know a real law firm and they and
they use some of our code so Oh wrong
button okay so this is just kind of a
b-t-dub
so the red is what we are modeling here
sort of all possible contracts and then
we have the deaths and then we have the
purple is where is where we can help you
out so so our ideal world is where
you'll write your write your little
contract you won't even think about
aetherium it'll just be oh they'll be
these agents with these obligation blah
and then and then it will just compile
and you can for the most part just not
worry about it and in the future you
could even get your english contract as
well so okay so let's go listen okay so
the first thing we'll ask well we love
solidity you do we really want another
language and the first answer is oh oh
you can still have your solidity and if
you still want your your low-level stuff
you should you should use just do it you
should still use solidity you can kind
of think of it as say using say c versus
i guess something like python i suppose
it's not quite exactly right but anyway
the idea is that you want like a high
level language for for doing high level
things you don't want to think about the
rest but if you're doing novel things
and you want to be close to the bottom
then you still use your solidity so we
use SQL sort of an example for why it's
a good idea so you can imagine query in
your database in C or Java Script would
be very unpleasant but doing it in SQL
is lovely so we're gonna give you an SQL
for contracts okay yeah that's why you
want to do it yeah and the cool part
about this is that that so we can't want
to do this is
because so first of all you you could
eventually one day compile your
aetherium contracts to English and
number two we could eventually start
getting Noir like like normal lawyers
aren't using aetherium because here's
the cool part because the etherium
system is more reliable than than a
judge's brain so you're like oh so it's
like so if you say oh you take all
lawyers you get all your regular
contractor you see compiling to English
but now you just run them on aetherium
and they're even more reliable and even
more predictable and they would be like
oh my god yes and therefore we bring you
know like what the 90 billion dollar
contract rafting industry into aetherium
which will make all your ether go up and
that will make all of you happy so this
is our start go so we have rough
consensus but not running code and the
rest of this talk is essentially going
to be a fairly high-level literature
review of ways of expressing agreements
and ways we can reason about them and
eventually ways in which we can compile
those in to code which is interpreted in
a way that preserves those semantics so
CL is a logic based formalism for
expressing contracts and this is its
syntax you can read that as saying that
a contract either indicates an
obligation to do something a permission
to do something a prohibition from doing
something the conjunction of two other
clauses or some contract becomes active
dependent on some other action having
being performed and we can look at the
structure of obligations where we have
two parameters C and alpha alpha is the
thing you're expected to perform right
now and if you do not do that then you
have to fulfill the reclamation clause
see that Clause C can be the far right
clause which is unfulfilled well and if
you ever get to that point you're in
breach of contract
actions are basic propositional
variables which can be either expressed
in terms of concurrent actions I do
things at the same time or you
sequencing you do one thing after
another or you do between one of two
things this is to make that concrete
here's an example of a fairly simple
clause this expresses that you should
that if you do a you must then perform B
and if you do B you must not perform B
and if you breach either of those
commitments then you are in breach of
contract and just to make some of more
later slides more legible we sometimes
omit the residual clause when it is
unfulfilled well so there have been
several semantics that have been defined
for this language originally it was
equipped with branching semantics and
the idea is there is that you can reason
about which expressions can be
substituted for each other and the sorts
of things they imply for example you can
take an obligation to perform some
action is equivalent to the prohibition
from not performing that action which
seems fairly simple we're gonna be
focusing here mostly on Tracy Mattox
where the idea is I want to say that
some sequence of actions is consistent
with a given contract you can read this
as saying the sequence of performing a
and then later B as the claim rather
fulfills the contract that we sold
before there are sets inside that
sequence to accommodate concurrent
actions and I seem to have missed
ordered the slides but essentially the
satisfaction define relation is defined
pretty much as you would expect if
you're obliged to form some concurrent
set of actions then you should perform
them or otherwise you must have fill the
reparation if you are obliged to perform
some sequence of actions
you should perform one and then the
other or otherwise fill that reparation
and this sort of reasoning is enough to
derive that claim we made before if
you'll admit the somewhat aggressive
normalization here so to show that if
you do a you must do B and if you do B
you must not do B in rough sequence well
we know that the sequence a B does not
involve initially doing a and so that
Clause is trivially fulfilled and in the
other clause because we do a initially
we have a residual we have the residual
obligation of having to do B and that's
a filled by the second component in the
sequence
I'm going on the wrong order it's the
other way button the down button yes the
down thank you for the down button so
that's really well but the cool thing
about this particular satisfaction
relation is its decidable and there's a
rendering on to automata so that you can
essentially just pass these things to
this machine and it can tell you whether
you're in compliance or in breach or
whether you have residual obligations
which later actions in the trace may or
may not let you fulfill and the cool
thing about these graphs this is an
alternative alternating all automata but
it doesn't have to be but never mind
because time is that you can do a bunch
of analyses about these which say which
tell you properties about your contract
so you can say that the sequence a B
satisfies it and so to the sequence a a
and B and so does the sequence B a
because that validates in both automata
you can say further that it's
satisfiable because there exists a trace
which is compliant another interesting
thing about this particular automata is
that if you consider the sequence in
which you initially perform both a and B
at the same time there is no valid trace
that valid extension of that trace and
so with respect to your standard tre
semantics that's probably fine but we
see something here we see that at this
coordinate we have the deontic
obligation to perform both B and not
perform B ie the contract is telling us
that under some sequence that we have
conflicting obligations and this is
somewhat undesirable and so there was
another paper which essentially extended
the semantics to account for the G on
take responsibility is it each
coordinate and essentially designed what
patterns you need to fulfill in order to
not have a conflict and this should be
true of all traces you can render this
into an automata but you're mushing
things together so all the obligations
are in the same place and then you just
pattern match on these to determine
whether you're saying two things which
you should not be saying at the same
time okay so okay so this is so this is
the one that I liked best so I am so
this one's a little neat because so this
so goes okay the previous one you saw it
gives a really nice flexible way of
representing contracts but when the
hits the fan you don't know know whom to
blame and you're like oh you always
gonna blame someone right and and in
particular so this is this is a sort of
a novel approach that allows you to say
oh well when when someone doesn't
doesn't do their job it says so and you
know you can see exactly who that is
this is nice because then you could
hypothetically aetherium eyes judges and
this is one where the lawyers would like
fully join us and that would be great so
so right now the way things go is that
you would write your things your
anything is a little contract but but
when it goes awry I mean you still have
to go to go back to the traditional
legal system so this ideas them at all
because you know exactly who is to blame
for every possible every possible path
through through through the contract and
that would just be great so I'll show
you roughly how it goes so this button
so basically there is a verdict which is
V and there's two ways a verdict can go
over a contract it can be a check mark
which means everything's great or it can
say there's a time stamp with a little
towel and there's a blame mean someone
need someone someone up and
basically and every contract is defined
as a function that map's sort of a
sequence of events or sequence of
actions Sigma to either a a check mark
meaning it's great or a timestamp and
then in
someone up and yeah so in like
and like that's it and so you can say oh
okay so and so you can fully describe
the ways through a contract through
through all these different Sigma's okay
and you can do like cool cool cool
composition on contracts too so you can
say oh well see how can you have
contract v1 and v2 so you can and them
or you can or them so you know it's a
little operations there and they sit
tells you how they go I mean and you can
do a more interesting things so you can
say oh so here's why the coolest one is
to look at this this is this on this
application clause so you have a agent
so this is this go back there so you
have h an e1 executing these these
actions kay and takes parameters X the
little thing over it and and so and it's
do with within some of the window D and
if it and if it wins I'm sorry and if
it's and if it satisfies all of it then
it says oh oh there's they're still you
get time left z so like so she had like
five days to do something and you finish
it in three days
z z becomes two and and then it goes on
to the next contract so you can sort of
chain contracts together and that's
gonna in this recursive form and that's
like really neat I mean so it's kind of
this idea oh so so so we're kind of
doing the beginning here we were doing
sort of like like what are the what are
the atoms of of contracts so I was like
the periodic table and these give you
all different ways that you can chain
them together into a chemistry of
contracts and make cool molecules out of
them and you can make like crazy
yeah so this says this is really fertile
okay yeah so here's an example one right
here so this is an NDA contract so this
ppreciate board so you see yep see it so
it takes one argument the employee and
it says oh if you ever get if you if you
if you ever get a disclosure reported
when it takes takes an E and if E is the
employee and it's happened within the
past five years then breach and and
that's and and that employee is is at
fault and the little little VIN employee
says the employee at blame and it says
Ellen by the way and it starts now and
sort of in this little simple code you
can compile this to English in ER
jurisdiction you could do it instead you
know of you know English French Mandarin
whatever or aetherium
and I and it would all just work okay
cool
so this is a saline here for the for the
languages and math people who want to
know how you actually implement these
ideas that's it this is for you and so
this so there there are some
complications in the way that you can
merge contracts there are there are some
restrictions so for example so if you
have so yet so you so you have a
different contract with it but the
people who they blame aren't always the
same you you you you can't combine them
and that's kind of a limitation and
that's annoying and we should pay a PhD
to figure that out okay so this is where
the next one this is how this connects
to the upcoming literature which you'll
probably hear about probably tomorrow on
a specifically etherium how much time do
we have because the things is like 30
seconds I'm just gonna skip to the next
slide and deccan beddings are cool and
we can we have a very well defined idea
in terms of the space of variation in
the contracts you can express what
indicates good behavior and the rest is
basically relates to the compiler and
you want to be able to say that
normalization with respect to a logic
behaves equivalently in your source
logic and in your compiled output and we
can do that and stuff alright next last
one you have to hit it all right so this
is the end
oh no next the other button there you go
um so okay so this may see our thing so
basically where we're here so we are
busy formalizing contracts sort of in
the broad sense we expect the authority
to be our power users so if you want
features you should let us know because
we're designing this and
yeah and we'll do like free work for you
and if you're in this kind of thing come
hang out with us and if you want to
follow us there's our mailing list and
there's our email address yep come talks
about languages sometime