The basic problem is that executable programs are a crappy representation for contracts. Analyzing executable programs is too hard. A declarative representation with guarantees is needed.
Here's a suggestion: an classic form called a decision table. See the Wikipedia entry.[1] For smart contracts, the underlying system should treat the actions as an atomic transaction - either they all happen, or none of them do. The input conditions in the table are expressions, but they are read-only and have no side effects.
Decision tables can be displayed in a simple, understandable tabular form. Ordinary people can understand them. This is essential for contracts.
For an action in a decision table to be another decision table might be permitted; this allows subroutines. But the whole operation must be treated as a single transaction, to prevent exploits and sync problems.
Decision tables can be turned into IF statements by a straightforward algorithm; the implementation is not hard.
This approach might make smart contracts usable. Etherium is too complicated, too l33t, and too buggy.
As a design goal, a programmable contract should be able to express:
- A time deposit, like a CD
- A credit card
- A recurring service charge cancelable by either party.
- A mortgage loan
- A rental agreement (which is what Slock.it was supposed to do)
- Most financial derivatives
If you can do those things, you've probably covered enough use cases for practical purposes. Complexity beyond that increases the attack surface.
Standard functions in rules can do most of the computational work. Good date functions, and financial functions such as present value, are needed. An HP-12C, the standard pocket calculator for finance, is a good basis for the functions needed. (The financial industry would like it if smart contracts got exactly the same answers as an HP-12C.)
Ethereum struck me as having been designed by somebody who didn't really know quite what they wanted it for. Finance not being my thing either, I didn't think of the HP-12C.
That might not be too damning an accusation. This is ver 1; it's a platform, not an app; nobody quite knows what the outcome will be anyway; and the terminology, while suggestive, is not prescriptive. However the lack of any kind of inbuilt datatype for managing an amount of money still did strike me as an odd omission...
(Maybe that would be too limiting? But I didn't like the way you had to send money and adjust balance(s) as separate operations. And, yes, of course, this was the cause of The DAO hack - but I don't want to sound too prescient here. It seemed to me an annoyance, no more.)
A security researcher from the access control industry agrees that Solidity has far too much complexity for the job.[1] He also suggests simple, declarative systems, and lists a few from the access control industry.
I remember the Interledger paper since it was one of best I've seen in these kinds of discussions. It was relatively simple, built on existing concepts, had much better odds of adoption, formally specified/verified, and leveraged prior schemes for robustness. That's how this kind of work should proceed whenever possible. Probably any protocol with significant use as well.
+1 on decision tables. I've been so deep into esoteric stuff that I forgot all about those. Tie-in to recent research is Boolean truth tables. The simple logic & ability to map it out so easily allowed for vast improvements in synthesis, transformation, and especially verification of properties. It's a major reason hardware is so much more reliable than software of similar complexity. Similar tooling could be applied to software version for contracts. Protocols and control systems, too, I'd think. Might have started there.
Another old technique from high assurance was using relatively simple functions and interactions with each one being a state machine. Dijkstra-style, we state input and output assumptions in precise, formal way. Then, the function is expressed in terms of both successful and failure states. Already plenty of techniques to model-check this sort of stuff to cover all cases. Even tools that generate them from specifications. So, modifying them for smart contracts with push-button verification that properties apply to all states is another option. Just dawned on me that the combinatorial explosion risk might make a natural mechanism to force the contracts to stay ultra-simple.
Animats, what do you think of that latter idea? If not for contracts, than verified software in general. Many talked about Kloc we could cover at any point as a limitation. People like Wirth saw simplicity as a benefit. Perhaps a reasonable Kloc limit combined with great tooling/process could be seen as an enabler for simpler, assured software? I mean, there's proven impact of such rigorous techniques & modular code in defect rates. But I'm thinking for non-pro's prone to incidental complexity working within limits that reduce their defect rates by forcing them to keep simple and verifiable.
Note: Might seem a bit rambling more than specific question. I'm sort of brainstorming on that one is why...
I used to work on program verification.[1] I've worked on automatic theorem proving. Formal verification is too much heavy machinery for this application. Here, you want something simple and understandable. Find the minimal solution which will handle the use cases listed and any likely ones I missed. That's probably enough.
With decision tables, you can run a case through them by hand quite easily. You can explain decision tables to lawyers and judges when necessary. You can distinguish between "contract did the wrong thing" and "underlying system executed the contract incorrectly." This is a big help when there's trouble.
After the Etherium/DAO debacle, the next attempt at this has to be simple and understandable. It would probably get more use, too.
these aren't at odds with each other. A decision tree is an executable program. What you mean is that you want a _less expressive_ language than full turing-completeness.
> What you mean is that you want a _less expressive_ language than full turing-completeness.
Why don't you restrict yourself to a more simple subset that you understand instead of throwing away the Turing completeness (I'm sure for the latter there are good use cases)?
From what I understand of DAO and the Turing Complete capability of Ethereum, the fundamental "flaw" in smart contracts is not "more testing for bugs", nor "more static analysis", nor "case insensitive syntax". Instead, the gap that will be always there is related to Rice's Theorem and/or Godel Incompleteness Theorem. E.g. you can't take the rules of a system and use it to prove its own consistency. The other concept that is relevant is the "limits of correctness."[1]
Based on Godel Incompleteness & Limits of Correctness, you will always require an outer "context" to verify that the smart contract did what was intended. That outer "context" can't be the Ethereum code -- it has to be humans. Whether it's humans in "an open source council", or arbitrators, or courts.
In a similar example with the NASDAQ crash in 2010, they cancelled some "bogus" trades.[2] NASDAQ is mostly automated by computers -- in fact, the "electronic trading" was its selling point over the NYSE. Even with NASDAQ's computer automation (this includes both the computer code inside NASDAQ and computer code of traders' computers) being a weaker form of "smart contracts", NASDAQ still has to have humans be the final judge of which trades were "correct". Is it possible to write a NASDAQ decision tree embedded in source code that will handle all errors thereby eliminating the need for any human intervention? I don't believe it's possible.
The idea of "smart contract" source code being the final authority is an unattainable goal. The DAO/Ethereum had the "NASDAQ 2010 cancel trades" moment by forking the code. That decision to fork is the outer context of the "smart contract".
In a sibling post, Animats writes,
>"A declarative representation with guarantees is needed."
A declarative syntax can reduce the bug count but it can't eliminate them and thereby remove humans from being ultimate judge of what is a "incorrect smart contract".
For a similar example, consider the following super simple function:
According the ideals of Functional Programming, that function is referentially transparent -- it does not reference global variables and just uses what's explicitly passed as a parameter. Also, the operations of multiplication, division, and addition are "well understood." There is no overflow flaw because a "double" datatype can handle all temperatures from Kelvin absolute zero -273 to Plank Temperature of 10^38. It doesn't have any gotos or jumps. It certainly looks like a "zero defect bug free" function.
So... what could go wrong with that function that could make it not work the way humans intended? I leave that as an exercise for the reader. (Hint: read "Limits of Correctness".)
Thanks for the paper. Didn't have it. Just skimming it for now.
"legal contracts, and other humanly interpretable specifications, are always stated within a background of common sense, to cover the myriad unstated and unstatable assumptions assumed to hold in force. (Current computer programs, alas, have no common sense, as the cartoonists know so well." (Smith)
Most appropriate quote of the paper for purposes of this discussion. Human negotiators have common sense plus legal precedents (and lawyers) that guide the process to create sensible terms. They might argue over them later but the process works well enough. You'll rarely see something enormously simple and stupid happen. Whereas, computer programs, when asked, will happily divide by zero, overwrite their own system files, or make some prick investing in blockchains richer than deserved. They're idiotic. The part of INFOSEC dedicated to reducing impact of inherently risky and idiotic computers running arbitrary programs has been a miserable failure. The ones using constrained, predictable programs on less risky or idiotic HW/SW combos have a steady stream of good results. Especially in safety-critical industry. One trick is they, like legal contracts, are extra clear on the Why, What, and Where of their operation. The typically implicit assumptions are explicit enough to check with regular brains and smart tooling. Smart contracts will need this property as well.
"consider the following super simple function:"
That function isn't simple because it has floats. I've forgotten too much C to be sure of what the error is. I'm suspecting one or both of two: no sanity check on lower bounds of input value in Celcius, which might affect correctness; errata related to floating point math (esp rounding) which is not decimal math that we teach students to use for conversion functions & likely was in the mental spec developer had in their head. I avoided floating point wherever possible due to its weird issues. Was I close or what was the actual error?
> You'll rarely see something enormously simple and stupid happen.
Because our society trains all people in this area very deeply. If the society would mainly train people really deeply into mathematics and computer science instead, I believe the situation would be exactly opposite.
Lack of bounds check on the input was my first thought, too. Need to deal with NaN sanely, too, but usually that takes care of itself as it propagates through any operations.
Here's a suggestion: an classic form called a decision table. See the Wikipedia entry.[1] For smart contracts, the underlying system should treat the actions as an atomic transaction - either they all happen, or none of them do. The input conditions in the table are expressions, but they are read-only and have no side effects.
Decision tables can be displayed in a simple, understandable tabular form. Ordinary people can understand them. This is essential for contracts.
For an action in a decision table to be another decision table might be permitted; this allows subroutines. But the whole operation must be treated as a single transaction, to prevent exploits and sync problems.
Decision tables can be turned into IF statements by a straightforward algorithm; the implementation is not hard.
This approach might make smart contracts usable. Etherium is too complicated, too l33t, and too buggy.
[1] https://en.wikipedia.org/wiki/Decision_table