Smart Contracts will never work if we treat them as normal programs
For some reason, we have a strange tendency to call things “smart” as soon as we take the human out and replace it with code. We do it with the Internet of Things, calling things “smart” as soon as they have a processor and a connection, and we’re doing it again with smart contracts. If we normally call someone or something “smart”, what we normally understand is that it is capable of intelligence and reasoning, to make its own choices and interpretations. Code however is exactly not that.
If the recent issues around The DAO show anything, it’s that replacing the human with code doesn’t add any “smartness”. It rather removes it, leaving only the deterministic instructions created by a programmer behind. Including its flaws. Code is a deterministic calculation, unable to deviate from its programming and as such incredibly dumb. Capable, but dumb.
Contracts have to be expressed in a very precise language. That’s why we have lawyers and they have their own legal language in which they write contracts (which also serves to obfuscate contracts in some cases, but it is precise). Programming languages are very precise, so they might seem like a natural fit for writing contracts in. That is until you consider the huge gap of abstraction between legal language and a programming language. It’s like forcing a programmer who has only ever programmed in Java to build its own CPU. It’s not even in the same ballpark.
At the same time however it is a mind boggling choice. Everyone who has ever programmed anything serious before should know that every program is riddled with bugs. Normally we don’t have to worry about that too much, because it’s easy and fast to quickly fix any issues that pop up. But in Ethereum and in the current concept of Smart Contracts, as soon as the code is running, it can’t be modified anymore. So your software has to be bug free.
However, it takes an herculean effort to create software that is relatively free of bugs. Such an effort and investment is only made by organizations such as the NASA, and even then gives no guarantees. No real world process where the stakes are high can afford such an investment and risk.
The DAO is a great example of how this went wrong. The developers of The DAO, as well as of Ethereum, are all incredibly intelligent people, and are very good at what they do. However, they are programmers, and they write programs, and they introduced a bug. Probably more than one. There’s no way back, no way to patch the bug, write a database migration and move on. So now we’re stuck, and $50 million dollar is up for grabs.
The way forward
What we need is a language that is precise enough to write contracts in, while also being of a sufficiently high level of abstraction that it can be written, read and verified by the domain experts. The contracts written in this language should be executable, but also automatically verifiable.
Programming languages are obviously not a good match for this, so this is why we’ve developed ACE (Automated Contracts in English). ACE allows you to write contracts on a much higher level of abstraction. An example to give a general idea:
Concepts: -- total number of tickets: a Number -- number of scanned tickets: a Number -- Account A is organizer: True or False … Initially: -- Creator is organizer -- Creator is scanner …
Conditions that must be true at all times: -- for all accounts A: NOT (A has a scanned ticket AND A has an unscanned ticket) -- total number of tickets >= 0
Queries: Query: what is the total number of tickets? Provided that: -- Initiator is organizer The answer is: total number of tickets ...
Operations: Operation: add Number N tickets Provided that: -- Initiator is organizer -- N > 0
The result is: -- total number of tickets = OLD total number of tickets + N -- number of unsold tickets = OLD number of unsold tickets + N -- number of scanned tickets = OLD number of scanned tickets
Oh and we haven’t just designed a language. We’ve also developed a compiler that compiles this ACE contract to code that can run on the Ethereum blockchain. On top of that, it also generates a test suite that can be used to verify the implementation. And it can also be compiled to other environments of course, as smart contracts are also a very useful concept outside the blockchain world.
This approach keeps the domain expert in control of the contract and bridges the gap in abstraction. We’ve actually tested it in practice with the development of real legal contracts and it actually works very well. It turns out that lawyers are, not surprisingly, extremely good at writing smart contracts when given the right tools. They are incredible at finding exceptions and patching them, as long as they understand what is happening.
We think Ethereum is a great experiment, but should be seen as a step in developing the infrastructure. However, if we want to solve real world problems with Smart Contracts, we have to develop tools that involve the real world. We develop these tools such as ACE, and we are always looking for more use cases to apply our approach. So if you’re interested, make sure to contact us at firstname.lastname@example.org.