Ethereum Foundation Devcon2, 23 Oct 2016

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Designs for the L4 Contract Programming Language Based on Deontic Modal Logic

Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/2/designs-for-the-l4-contract-programming-language-based-on-deontic-modal-logic

We propose the creation of a domain-specific-language (DSL) for (smart) contracts are consistent, correct, and complete. Our DSL, L4, doesn’t simply fill templates, it fulfills the Curry–Howard correspondence between computer programs and mathematical proofs, i.e., what functional languages do for the 𝜆-calculus, the DSL will do for the deontic modal μ-calculus. This means the DSL natively expresses obligations, permissions, prohibitions, and other contractual concepts in a way that computers can easily reason about. The compiler will be responsible for static analysis of the contracts and automated detection of several classes of errors, including: inconsistency, inompleteness, goal satisfaction, and policy compliance. Functional languages are well-suited for this kind of formal verification, and we developing L4 in Haskell. L4 derives from the academic literature on contract formalization, everything is opensource and we invite feature requests and contributors to define and create what will become "SQL for contracts".

Speaker(s): Dr. Virgil Griffith & Vikram Verma
Skill level: Advanced
Track: Society and Systems
Keywords: legalese, lawyers, dapps, solidity, sql, language, code, syntax, semantics, trace, sequence

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 2 was held in Shanghai, China on Sep 19 - 21, 2016.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

A

Virgil, dr. Virgil, Griffith and Vikram Verma will present designs for the L for contract. Pro make programming language based on deontic modal logic.

B

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!

B

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.

B

There, a clicker, oh.

B

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.

B

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!

B

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.

B

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.

B

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.

B

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!

B

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.

B

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.

B

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.

B

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.

C

We have rough consensus, but not running code, and the rest of this talk is essentially going to be a.

C

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.

C

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.

C

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.

C

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.

C

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.

C

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.

C

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.

C

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.

C

I'm going on the wrong order.

B

It's the other way button the down button. Yes, the down. Thank.

C

You for the down button.

C

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.

C

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.

C

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.

A

C

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.

C

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,.

B

C

B

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.

B

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.

A

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

C

How much time do we have because the things.

B

A

Like 30 seconds I'm.

C

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.

C

B

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.

B

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.