Bloomberg – Blockchain Company's Smart Contracts Were Dumb
bloomberg.com
bloomberg.com
Model checkers work. You can, with effort, prove programs correct. This works very well for small programs but grows exponentially more complex in the number of branches and variable constraints. Even if you had the computational power you'll quickly hit an inflection point where you're as likely to have a bug in your proof as you are the underlying code.
Life-critical systems style code review works. NASA is very good at writing bug-free C code via a style guide that subsets the language, static analysis/formal methods, and a review process that makes waterfall look agile.
Voing works. In aerospace, code that's responsible for controlling actuators and surfaces is often implemented in three different ways, driving three different actuators. If one implementation returns a different result, majority wins. Same principle for other applications - the output need not be an actuation.
The biggest problem isn't that bug free system are a pipe dream - it's that making one is very expensive, and the cost grows massively as your tolerance for error decreases. This is a community that wants to drive adoption, and that means competing with the status quo. If one of your selling points is that you're saving the cost and complexity of dispute resolution and human constructs, you've gotta factor in the cost of writing bug free contracts in the first place.
IMO it probably won't be overly onerous to develop reliable contracts of this size using many of these techniques. It's just so few people have the discipline to delay implementation for design and planning at the level required when it needs to be bug free. Most software developers have no training in how to even begin designing and developing using these techniques.
[1]: Shuttle's primary flight software contains 400,000 LOC http://www.nasa.gov/mission_pages/shuttle/flyout/flyfeature_...
It sounds like the contract was underspecified.
In my experience, the basic core logic of a system's usually a pretty small part of the overall codebase - the edge cases and error handling tend to be the bulk of the code.
This tends to be the case in legal contracts, too - 100 pages of boilerplate to make sure the two pages of contract are air-tight.
For example, a few weeks ago, there was a news story about an ethereum prenuptial agreement : http://www.coindesk.com/prenup-ethereum-marriage-obligations... : https://drive.google.com/file/d/0B1MEGeLr7lWiNEE2U2lGdGFvSm8...
Ok, obviously a dumb idea, and not serious (I hope?) But take just one of the contract terms: 'It is stipulated that both the parties should spend at least 100 minutes every 10 days on a date-night'
As someone in r/buttcoin wrote at the time: "In the last ten days, User 1 spent 5 nights at home, 1 night in a wrecked car and 4 nights in Lakeville Hospital. Date night clause has been broken. Marriage terminated."
My point is that coding is the least of the problems with a smart contract. There needs to be a way to handle unexpected circumstances. In the real world, courts do that. In smart contracts, you're out of luck.
[...]
> What JPMorgan did was explicitly allowed by the rules, but that doesn't mean that it was allowed.
This seems like both the biggest feature and the biggest bug of our legal system. On the one hand, the court system exists to adjudicate cases that aren't clear-cut, and often establish precedent in the process. On the other hand, that makes it extremely difficult to construct a system where all the rules are clear cut and have "let the buyer beware" all over them, and not have someone "cheat" and ask the court system to reverse a result that didn't go in their favor. Heads I win, tails the court system might say I win anyway.
If you want a contract where the "spirit of the law" prevails, write it that way. For example, the electricity regulations mentioned in the article could have been written to say "if you find way to arbitrage this and produce infinite money, you're wrong; this is governed by the spirit of the law as interpreted by $governing_body".
But there should be a way to write a "letter of the law" agreement, too, where people can actually rely on the rules. There should exist a sufficiently strong disclaimer that anyone agreeing to it will get summarily rejected from a court saying "you should have known better". There should exist agreements where someone giving their word is ironclad and irreversible.
You can build systems that incorporate human judgment and reversibility on top of such an ironclad rule-based system. But the reverse isn't true: you can't build an ironclad system on top of a system where anyone can cheat by saying "no fair, I lost my money and I didn't really mean it" to a court.
Sometimes, people find it comforting to have a "soft" system backing them up that will look at the human factors involved; for some systems, I do too. But in some cases, you want the comfort of knowing that you can rely on the rules as stated and not someone saying "actually, now that I've lost money I don't like the rules anymore, give me my money back".
Which is why it's literally not possible to reduce a contract to code, and it never will be.
Even if you could produce perfect bug-free code at reasonable cost - a fantasy in itself - you still have to contend with the irreconcilable motivations of the parties to the contract, and the fact that contracts are used to hide motivations as often as they are to reveal them.
It's perfectly possible - common, even - that the motivations are conflicting, irreconcilable, and ambiguous, to the extent that the true practical meaning of a contract can only be defined by an external higher legal and political authority.
Or by one party rolling over. Because making that more likely is what many lawyers get paid for. (And what some of them live for.)
I don't think that's a reasonable dichotomy. "Letter of the law" isn't exclusively useful for people looking to exploit power asymmetries or create unfairness. It's also useful for smaller entities to protect themselves from threats that larger ones have enough insulation to just weather and survive.
Consider a service where you take money from a user, and then use that money to run a service on their behalf, in a fully automated fashion. You get $x, you spend $y on a server and bandwidth, and you pocket x-y as profit. But if the user pays for your service on a credit card, they could dispute the $x, and leave you on the hook for $y, which could be arbitrarily large; you can immediately cancel their service, but that doesn't get you the $y you've already spent back. It'd be nice to have an enforceable agreement that "you can cancel at any time and stop paying us, at which point the service goes away, but under no circumstances will we owe you anything".
(This is also one reason why companies often don't offer discounts for paying up-front for a year or more, and credit card processors consider those high-risk: too many people dispute the transaction after a short time and get all their money back, including what they've already paid.)
I can imagine many more scenarios that rely on "once you have the money it can't go away", that don't work nearly as well with reversible transactions.
> how do you avoid massive problems due to buggy contracts as we're seeing?
In cases where you want human judgment as a safety precaution, write it in at the top level of the contract. "Notwithstanding anything else, all transactions are reversible for up to X days based on the judgment of Y, to be supplied via Z mechanism; if such judgment is not supplied, the transaction becomes immutable after those X days have passed." (Or, if you want, "all transactions can be disputed for up to X days, which will then hold them for judgment by Y for up to Z days".) The equivalent of "don't run untrusted software in ring 0"; the "pure letter of the law" space is ring 0, and many things could be built on one or more layers of indirection above that.
In cases where you don't want human judgment, then you avoid buggy contacts the same way you avoid buggy software: get a lot of people looking at it, and limit how much you trust things that haven't been heavily hammered on for years. Anyone investing millions into a "smart contract" today is taking an absurd risk.
You could also purchase insurance of some kind. If the price of that insurance is absurd, that should tell you something. But not every transaction should have to price in built-in insurance (and actuaries to properly price it).
Or just ask people to pay you in cash.
If you have to sue to recover the money, you're out the money until you win, and you might not win. You're also out the money if the entity you try to sue can't be sued, which can happen for a variety of reasons, such as "already pulled the money into a different jurisdiction you can't touch", or otherwise "doesn't have the money to recover". And in any case, it isn't worth the trouble unless the transaction is large enough, which is why most service businesses have to budget a certain amount for losses due to fraud.
I'm not sure why you think an unbreakable agreement wouldn't fix that, assuming it was actually enforceable as such.
> Or just ask people to pay you in cash.
Cash doesn't function for online services (with very rare exceptions). And even for a cash transaction, people can sue you and demand their cash back.
To clarify something: I don't think that the entire economy should use "rules as written" transactions; I think that would be an incredibly bad idea. For example, I want to store the majority of my savings somewhere that follows "spirit of the law", and has some protections and recourse for transactions I don't want. And I spend money on credit cards, confident that I can call up American Express if something goes horribly wrong. (I've never had to do so.)
I do think it should be possible for me to intentionally and verifiably move a small amount of money from my bank account in a "rules as intended" system into a transactional account in a "rules as written" system, and then use it to conduct a transaction in that system. (Moving the funds is necessarily governed by "rules as intended" protections provided by my bank, as for example I would want some recourse from my bank if that transaction wasn't initiated by me. That then gives the bank an incentive to make absolutely sure they have valid authorization from me.)
Did I misunderstand the idea?
A well-established mechanism for text contracts to say "this means exactly what it says" would be quite useful for a wide variety of applications, though it would be limited by the need for minimal interpretation of natural-language text.
A form of contracts-as-code would also be useful for the much narrower set of applications in which code can completely describe the implications/performance/etc of the contract.
This is really a good thing. The most tangible example I can come up with is employment law in California: One big thing that distinguishes the labor market in California from other regions is that non-compete clauses are basically unenforceable. Non-compete clauses being a big drag on innovation (since they basically imply that if you have a good idea that is related to your current line of work, and your current employer doesn't see the value, then you're SOL and not allowed to have a go of it), there's a very strong argument to be made that Silicon Valley couldn't have happened in any other jurisdiction.
These would be great to make people sign at gunpoint!
Beneath that though, i think there's an undercurrent of something that feels like misanthropy: a strong desire to replace political human beings interacting in order to resolve conflicting interest, reconcile conflicting experiences and pursue common interest with purely economic agents that interact with each other through free (read: mechanistic) markets and algorithmic contracts.
It feels like there is an unspoken need to be able to tell every human being who has a problem "too bad", and a need for a societal structure that is maximally ""rational"" and unassailable by human political action.
Obviously this would be a strawman if i said any particular person or group specifically held these beliefs. It's an amalgamate of various ideas I've seen pop up in the same places at the same time. Call me a skeptic of any thought that leans in this direction.
A more charitable stereotype might be that cryptocurrencies and automated contracts appeal to anyone who thinks that they can design (through their technical expertise) a better world than the current political elites. I'm not saying that they're right or that their line of thought hasn't been historically responsible for atrocities, but I don't think it's fair to paint them as sociopaths.
The benefits of cryptocurrency i've seen argued for in left libertarian circles don't propose some narrative where it supplants the current structures of government. I think a lot of leftists would reason (certainly, I reason this way) that cryptocurrency's much touted benefits are in conflict with capitalism and could not support capitalism at all. This is at odds with the right libertarian ambitions for the technology: right libertarians love capitalism and the crypto enthusiasts on that side of the spectrum think it would be great for capitalism! It's a fundamental disagreement. I've heard about bitcoin being used to great effect by left wing insurgencies like Rojava. It is useful in its current form as a subversive means of transmitting resources.
I'm not familiar with the left wing arguments for cryptocurrency as a transformative tool for structuring new societies. It sounds like technocracy and vanguardism and, well, we know how that's played out.
Then they rules are a sham. They are meaningless. If the "rules" in a contract are just vague suggestions, then the contract is basically useless.
wat? can't people just realise it was a loophole and hence unacceptable?