Rethink Trust 2018: Douglas Beardsley, Smart Contracts You Can Take To The Bank
Recording: Rethink Trust 2018: Douglas Beardsley, Smart Contracts You Can Take To The Bank
I'm Doug Beardsley I work at a company called Kadena in New York and I'm here to talk about our smart contract language called pact and how pact can help you write smart contracts that are less likely to have bugs and more likely to do what you want them to do quick overview of of what we're gonna cover start with just a little bit of a high-level blockchain background whirlwind overview I know everyone probably knows it but just to establish a baseline of what we're gonna be talking about then look at some of the problems with smart contracts we're not gonna try to enumerate all of the problems but just a few that I think are important and then look at how pact solves these problems so what our blockchains they're at their core tamper-proof append-only digital storage now we've had append-only digital storage for a long time and the core thing that blockchains added that we did not have before is that they allow us to make these stores tamper proof which is really a pretty significant thing and I think the world is still realizing and coming to appreciate exactly this what the significance is blockchains accomplish this by storing the same data on lots of different computers around the internet every one of these computers that is participating in the network has to agree exactly on the data in this store and that's what we call consensus the result is that you don't have to trust a central source of truth the network is your source of truth now smart contracts they're a little bit of a misnomer they're not really smart and they're not really contracts they're just computer programs that you store on a blockchain and they are run by the computers that are participating in the net work that is storing the blockchain data and that's kind of all they are but writing programs in this domain is different than writing programs normally like most of us are used to every operation that you do it has to be run on thousands of computers across the network which is not not normal for us programmers and every every one of those computers has to have exactly the same results every time that the same inputs must always give exactly the same outputs if you don't have that characteristic then you can't establish consensus and you and the baseline of what we use to determine whether something has been tampered with is gone and that's really different than normal we have most programming languages have functions that will say get the current time but the current time function returns a different thing every time you call it or it may be something else that reads from the keyboard and it returns whatever key you press which is not necessarily always the same if you run that in a blockchain context you're not going to get the same result and you won't be able to establish consensus and this is a really significant point another thing is that since these smart contracts are often dealing with crypto currencies various kinds of digital representations of of assets the stakes are a lot higher than normal and there's there's lots of digital money on the line and that is a new thing I think also you have to pay transaction fees maybe not in all blockchain settings but certainly the popular ones in order to interact with any of these smart contracts you have to pay some fees it just adds another another layer of difficulty that you want to make sure you get you're getting things right and then because these stores are tamper-proof the code that you put in them is immortalized forever it's it's there and you can't go back and say oh I need to fix this thing you could potentially release a new version of that thing but the old version is still gonna be there and and there's nothing you can do about it once you put it out there and that's also fairly different from what we are used to the result of all of these factors is that correctness in a blockchain context is much more important than usual so what are the what is the problem bugs smart contracts are notoriously buggy 25% plus of contracts tested in this one paper had exceptional owner abilities and this is just one kind of vulnerability and there's there's plenty others I'm not gonna try to characterize like the total percentage of buggy contracts but whatever it is I think everyone agrees that it's a lot what is this account what does this do to us it if you have contracts that are buggy people are gonna be less likely to put their money behind them and that means that the top the adoption is going to be slower so higher risk slower adoption that's not what we want this is this is a new technology we want to experiment with it we want to allow people to have reduced risk and adopt more quickly so we can we can learn faster so what are some problems with smart contract languages well there are a number of them I'm not gonna try to enumerate all of them here but I want to focus on three first of all they're based on mainstream languages or at least a number of them our second code that is stored in the blockchain is not human readable certainly in the case of aetherium you're storing evm bytecode which is not the thing that the programmers actually work with but that's the thing that is immortalized in the blockchain and that makes it harder to understand what's going on and then these languages are often difficult to verify and and be confident that they do what you think they do so let's look at these a little bit more detail a while back there was a smart contract called Rubic's II and this is this is actual code for an actual contract in the etherium blockchain now and it's it's not obvious what happened here but on line 13 we have this function dynamic pyramid which was the old name of this smart contract but then somewhere along the line they decided that they were going to rename it and they renamed it Rubik's II but they forgot to change the name of the constructor function what that does is it means that that function dynamic pyramid is not a constructor function anymore and that constructor function is the function that sets who owns this smart contract big problem anyone can become the owner now because that's not the constructor that's just a normal function that anyone can call and so it basically made this completely a free-for-all anyone in this room can go and like submit a call to this dynamic pyramid function and then you will become the owner of the rubic C contract well what that probably means is that not very many people are going to use Rubik C anymore but I thought this was a really interesting illustrative example the object-oriented paradigm and the associated drive violation now DRI stands for don't repeat yourself which is a common at best practice in software if you repeat yourself and you change one thing and you forget to change the other thing that can often be a bug and that's exactly what we had in this case and the the object-oriented programming paradigm says oh we're gonna have a class and the constructor of the class is gonna be the same name of the class is directly responsible for this bug so mainstream languages I argue are not sufficient for smart contracts this Rubik's II problem you wouldn't think that this was a significant thing in oo languages it's it's just a two minute fix you're like oh I forgot to change the constructor name you change it and you move on but in the smart contract setting you can't change it because it's tamper proof and that that is a really big issue for a lot of contracts also mainstream languages aren't very good at guaranteeing determinism because we've never needed that before it's fine to have a function return a different value every time we need it all the time but in this setting we can't have that and so we need languages that understand this and have this taken into account from day one when the language is being designed and third mainstream languages just don't provide enough safety for this high-stakes environment that we have in the blockchain world second point is code is unreadable in the blockchain now the the counter-argument to this is that oh you can publish your code and then people can verify that that code created the evm bytecode and that's true and it's used but only about 1% of contracts have their source code available so clearly it's not very widespread and wouldn't it be better if we were building on a system where you just were putting the human readable stuff into the blockchain from the get-go and my last point these languages are hard to verify there are situations where fallback functions in solidity complicate the control flow values can be mutated mutation is a little bit harder to analyze and a lot of these languages are turing-complete and that makes them much more difficult to analyze so how does pact address these problems well first of all we did not default to a flawed paradigm just because it's popular we said let's really think about what characteristics we need in our language in order to make make the guarantees that we want achievable pact is purpose-built with smart contracts in mind the code in the blockchain is human readable you will put pact code right into the blockchain and everyone will know exactly what code you were looking at when you wrote it also we are going to have a provision for smart contracts to be updated or fixed this does not revert what I said earlier about block chains being tamper proof we're going to to have a mechanism for declaring a new version of something and people will just by default use a new version and that's a really important feature in a lot of situations it's also designed for storing data which is really one of the key things that blockchain programs do it has built-in auth infrastructure which is often a source of trouble and there's all kinds of things that you can get wrong if you're rolling your own crypto so we're putting that in and taking care of most of those concerns for you so you can focus on the business logic you also can't put encryption keys in code currently this is fairly fairly widely considered a best practice but you can still do it in pact you can't it just can't be done also pact is not turing-complete values are immutable and it's an open source language it's written in Haskell by people who are familiar with cutting-edge programming languages Haskell is fairly fairly widely understood to be one of the the bleeding-edge languages where a lot of programming language research happens and the people that built pact are aware of this stuff and are able to take the the state-of-the-art technology and programming languages and apply it to the blockchain setting so here's a little example of what some pact code looks like on line one you can see we're defining our admin key set and you can see this this read key set call here is where we don't allow keys to actually be put into your code you have to call this read key set function and the key comes in from outside of your code then you associate this key with this module so that that key is the the key that has the Amendola jiz for this module and it's just very straightforward there's nothing nothing complicated you're kind of saying what you want I'm not gonna talk about most of the rest of the code in detail but I will point out that down here at the bottom lines 22 through 25 this is where the constructor code goes and it doesn't have a name that name doesn't have to match the name of the module it just gets run by default so the problem that Rubic's he had could cannot possibly happen in pact also pact has formal verification now a lot of people throw around the terms for a formal verification and I think it's not really appreciated quite what's going on formal verification at least impact allows you to prove things about your program for all possible inputs it would be impossible to actually test them all what we're doing is we're doing math to analyze the way the program is structured and actually have a proof that certain conditions can or can't happen and that's really really powerful and it's benefitted substantially because pact is not turing-complete it becomes much more easy to analyze so here's a little example of formal verification this is a very simple function it calculates the absolute value it just takes one input an integer and returns you an integer that is the absolute value and there are a number of things we might want to prove about this function we might want to prove that the result is always greater than or equal to zero and this is exactly how you would do that you just say that there's a property that has to be fulfilled that the result is greater than or equal to 0 and pact will actually prove that for you this this is something that it can do and it works today another really interesting one is are these two about not reading or not writing to the accounts table in some circles they call this side effects and you often take them for granted but we can prove these things impact we can prove that this function does not read or write from any database table and for simple functions like this that's really useful it would be really problematic if this program did read from the database but uh the language would allow it but we have this property checker that can make sure that you're not doing that it's it doesn't seem as significant for a small function like this but when your functions get larger it's it's really easy to lose track of what was happening somewhere down further in the code and not remember that this property had to hold so just to recap things humans are always going to mess things up I think that's that's a pretty clear takeaway that I've had in my software career when we look at all the bugs and smart contracts especially like this Rubik's e1 this is that was a bug that like is easy and obvious it's not it's not subtle at all but there are just so many details that you have to wrangle when you're writing software that you're not going to make sure they all line up and so I think we have to accept this as a fact and try to build systems that make these kinds of mistakes actually impossible so they cannot happen and because the stakes are higher in the smart contract domain it becomes even more important that we do this pact was purpose-built designed just for the needs of writing smart contracts it's human readable and it has really great formal verification properties and check it out we if you would like more info I'm gonna be around you can certainly talk to me here we have some documentation on our website you can also try pact just instantly by going to the try pact page and you can play around writing a little bit of pact code right there pact is also open source you can look at the code it's on github you can give us pull requests and open issues and help us evolve the language and also kadena is hiring if you are a high school developer and you would like to work on this language then definitely send me your resume also if you're not a Haskell developer we are going to be looking for people who can write packed code for clients and so there are job openings there as well thank you very much oh I guess we have a little time so are there any questions so we'll ask you to speak to the microphone so our volunteer will bring the mic to you please wait until a raise your hand and wait until he brings my so thank you doc this is awesome I I want to thank you from the bottom of my heart for bringing Liz be cold to the old bars of Amsterdam this is probably the first time when it happens and your hostel company so it's all you know very near and dear to me question yeah I mean it still looks complicated right so when you talk about parked developers so how do you envision enterprises we still use couple in their basements in Excel and things like that how do you envision how how much harder is say part than than an Excel function in reality what how do you envision the development environment will there be an IDE will be parked meetups and people sharing tips like how do you envision like a system and how the envision these are these people gonna be developers are there gonna be business users if you can talk to that yeah I think that pact is actually very easy in some axes because the syntax is incredibly simple it is a lisp as alexey mentioned and other people might have noticed so the syntax is is very very simple straightforward there's not a lot to learn there as far as syntax goes as far as IDE features and and like larger scale development we definitely foresee those kinds of things happening the community already has a fair amount of tooling will will try to steal as much of that as we can and make it our own I absolutely envision meetups and and thriving developer communities but these things take time and we just need people trying it out using it for their problems and seeing seeing what works and what doesn't any other questions right here yeah very interesting talk thank you I I'm minding that there's been a lot of work in verification and certain vertical sectors are very strong on it for example if I'm writing software for an aeroplane I probably go and I'm wondering to what extent have you been able to leverage learnings from those areas so I can't speak for specific domains but under the hood pact uses the z3 theorem prover from Microsoft so we are absolutely standing on the shoulders of giants there and that's that's what really makes all of this stuff go under the hood other questions over here on the right and is it possible to roll random numbers because there are algorithms like quicksort which use random numbers but are still deterministic great question no because fundamentally that is not deterministic so if you're gonna do random number generation you have to do pseudo random number generation do take the cryptographic hash and you know take some bits of that you could implement your own pseudo-random number generator and then pass in the seed as as an argument to the function but that is an area that I think makes my point that sort contract programming is very different because normally we just take for granted that we can Oh get a random number from anywhere but you actually have to be much more roundabout you can't just do that in smart contracts in general because every every computer out there will run this run the program get a different number and now no one will agree on consensus and that that just doesn't work in this setting any other questions thank you very much I appreciate the time [Applause]