# Designs for the L4 Contract Programming Language Based on Deontic Modal Logic

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2017-10-09
- Duration: 18:50
- Topics: blockchain, smart contracts, distributed ledger, Vikram Verma, Virgil Griffit, Dr. Virgil Griffith, L4 Contract Programming Language, L4 contract, Deontic Modal Logic, ethereum, devcon2
- Watch: https://streameth.org/watch/yt-Ufy8oM-Ou90
- YouTube: https://www.youtube.com/watch?v=Ufy8oM-Ou90

## 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/

## Transcript

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