Flexibility in Solidity

when you design a programming language you have to make compromises constantly there are people who request features and of course features are nice but with each new feature the language gets more complicated and thus easier harder to understand and it's easier to make a mistake the more complicated the language is so you have the constant balance between functionality and safety of course there are features that are safe but yeah that's the compromise you have to find and this has not been the case for general-purpose programming languages for several years now but in blockchain there's always the factor of cost so smart contracts have to be very cheap to execute and that also limits the features you can add in a language back in the days when solidity was started the initial goal was to create a usable high language high-level language as fast as possible and I think we succeeded in that but of course we made some decisions we now yeah which turned out to be not that not to be the best decisions and now is the time to change them and solidity is still a language that changes and that allows us to make the necessary changes to the design and yeah the the path you want to go is we want to keep features that are relatively safe and we they look like high-level features but most of them are actually quite low level so we want to have features that that look like here look look like high level features but are still cheap and we want to remove everything that can surprise users or has some semantic involved and then a third factor is we are adding formal verification tools that are easy to use and this I would like to stress this easy-to-use part because that is essential and we will see that later in the talk and then if there is not enough for you we provide direct way to access very very low level features of the etherium virtual machine and the important point is here that we remove everything that is kind of intermediate level so for example address dot call will be removed in the future because it has some magic some some unexpected things involved that we would like to avoid so if you want to do such low-level things you have to go all the way down to the human virtual machine ok this is kind of the the path we want to take now let's talk about some new features we added in the last year this contract here is a simple database that stores people by an identifier a name and some flag that says whether they are owner of something and you have a function there which allows you to add one person to the database it already looks quite repetitive and but it gets even more complicated if you want to add a function that can append a list of people into that database the problem many people run into is that you kind of have to create an array out of these three things here and what you usually do is that you add three parameters which are each an array this of course creates the problem that you have to check that all of them have the same length because you have an ID that corresponds to name and this flag this looks really really ugly but fortunately now what you can do now is hope sorry what you can do now is this and we added structs as a central feature to the ABI which allows you to actually put just we passed this truck from JavaScript into the contract and remove all this these weird repetitions and of course you can also return an array of structs so this is not this is not yet available but yeah thanks so we hope to get that fully functional by the end of the year so and the way we the way what this this was possible while was through a change in the compiler itself so we we could have done that the old way but we decided to do a full rewrite of the ABI encoder and decoder and this is a snippet of the solidity code generator and how it looked before this change yeah this also this is also really really ugly the EVM is a stack machine and because of that you have these this pop and to operations and in the code Ranieri you constantly have to keep track which variable is where on the stack and because of that we have these comments and it's really really complicated to understand what this code does and also complicated to write new code and this is how it looks now and it leverages a new intermediate language we introduced called Yulia Alex talked about that I think yesterday or the day before yesterday so I will not go to into 10th about that but you see this is really really readable it has variables you know what happens you can use names we have for loops and so on and what you also see is you have these angle brackets here and this is because this is an intermediate language mixed with a very very simple string templating engine to make it more flexible what you see here is the full function to do any encoding of an of an array into the the ABI so it does handle memory arrays call it arrays storage arrays arrays of arrays arrays of constant length arrays of dynamic length and so on and the way it works is that for example here at the top we have length equals length fun and at the time of compilation this length furnace report is is replaced by the name of the actual function to retrieve the length of the array which is of course different for static resized and dynamically sized arrays okay and a language becomes more and more useful the better tools are available for that we already see that by in the questions that were asked in the previous talk remix got gigantic updates I think yang will talk about that later today we now can track variables have breakpoints see references of variables and I think soon can also rename variables and so on we have an way to export the ast which is the result of the of the parsing step and these this allows many new features and one of them is a tool to do code coverage not based on syntax not just based on lines but on semantics so for example is a less than operator actually tested to do what it does and then a standard JSON i/o this is a way to get more fine control fine fine grained control about the settings of the compiler yeah then I have a very special announcement to make and this is that the solidity documentation that we only have in English for now is now also available in Spanish so please give a big round of applause to these five people who these five people who did that in their free time just as voluntary contributors I think this is really important to make if you remix esse below the world and languages like so like like Chinese or Russian should also have a their own translation of the documentation and I want to spend the rest of the talk on formal verification of solidity and I think I showed this slide to you last year in Shanghai this is a smart contract and it has comments which allow a formal proof that the the some of the balances in this token contract never changes and the way it works is that the smart contract kannst gets translated by the compiler into a language called y3 and it mixes this translation with the with the comments you have here and then you run an external tool on that to create the proof that the balances are constant the sum of the balances are constant but what you see is that there are almost as many lines of comments in this code as there is code and you also see that the these comments use a language that is slightly different from solidity so it requires you to learn a new language it requires you to learn how to use these tools and this is this makes it very hard to use this formal verification tool and the harder it is to use the easier it is to make mistakes and also it is easier for so for Mara fication is only useful if people understand what is actually proven there so the statements that are proven there have to be understood by humans and if that is not possible then nobody will use formal verification and it's useless and because of that so yeah perhaps that approach was not so great so we took a step back and reconsidered how it looks now is like this we've replaced y3 by a tool called an SMT solver SMT solvers are less powerful than general theorem provers and because of that the smart contract in this smart country we cannot prove that the sum of all balances is constant but we can prove that the sum of the two balances that are modified is constant so what happens here is we have a require statement which is yeah doesn't have much to do with the formal verification this is just the regular solidity requirements require statement and then we store the sum of the two balances in the before variable we perform the modification and after that we check that before equals after and this is a regular solidity assert so if the sum of the balances is not the same then this will throw an exception at run time but using the SMT solver you also get a proof at compile time that this assertion will never be triggered okay more specifically what happens is that so you can use this tool with require statements to have expressions that you assume to be correct and then the tool proves that there is no assertion that fails there is no overflow or underflow in your Matic operations no division by zero no constant conditions no unreachable code and whatever we will come up in the future and so let's take a look at a simpler example this is the experimental feature and because of that you need this first line that activates the SMT checker and yeah the function here it just takes two numbers and adds them of course there's a problem because we can't create and we can have an arithmetic overflow here in this edition and this is exactly what the so if you run the compiler on that then this is the message you will get and the great thing about this isn't you solver is that it has so it's more limited than y3 but it has a feature that y3 did not have and this is the following so you if an assertion fails it tells you why it fails and I think this is really important because otherwise people say ah I don't know it doesn't work but okay let's just let's just comment it out or whatever throw something at it so that it doesn't complain anymore but this tells you why it fails and kind of forces you to think about this edition and think about why it might create an overflow and then take the necessary steps to prevent the overflow before it happens there are so currently what people often do is create runtime checks about overflow at runtime checks about overflow in arithmetics but this can be really dangerous because if you end up in a situation where you you have an overflow because of some yeah internal mechanism of the smart contract then it will be the the smart contract will be stuck because it will always throw this exception because of the overflow and you perhaps can't get the money out or whatever but if you already get the warning at compile time before you deploy your contract you can think about why it happens and prevent this from happening in the first place and how are you prevented this like this so you had a require statement which of course in the end has the same effect as if you would just check if there is an overflow but the benefit is that you see that there isn't there's an additional condition that is present about these numbers a and B and the SMT solver will now see the require statement take these conditions into account and then check again whether the overflow will happen and of course it sees that a number less than 2 to the 100 plus the number less than 2 to the 100 will be less than 2 to 1356 ok yeah let's take a look at another example this is taken this is an actual example from the underhanded solidity coding contest where there was a loop that used an unsigned variable and decreased it but checked against equaling zero and of course this loop condition is always true that's of course something that can be detected from the type of of the variable alone and you don't really need an SMT checker but yeah I this was a simple example to present here and it can do much more complicated conditions and yes this is what we'll see next and yeah this talk was quite dry about programming language theory so I would like to end it with an exciting math puzzle so here we have a circle plus circle equals 10 circle times square plus square equals 12 Circle Times Square minus triangle times circle equals circle or what is triangle any guesses so yeah easiest pie we just write a small solidity program that is equivalent to this puzzle and we add the conditions as require conditions and then at the end of search falls so assert false sounds weird why would we do that and the reason is if the SMT checker can prove so a failing assertion so assert false is not bad it's only bad if it's actually reachable code so false assertion will not be triggered if it's not reachable so the SMT checker has to prove to us that this assert false is actually reachable and it's reachable if all the three require conditions above are true and of course it doesn't just tell us that is reachable it tells us how it's reachable so what are the exact inputs to get this failing assert and we see that triangle this one okay this kind of shows the power of the SMT so we don't really know yet so it's not it's still experimental and not fully finished yet we don't know how it will behave and very complicated contracts but yeah we're we're optimistic and let's see how it goes thanks you thank you for your attention [Music]