No, we can. We just don't, because it's very expensive, and we lack proper tooling to make it cheaper and/or faster. The flaw as I see it is that ETH jumped the gun, and tried to move to software law enforcement without investing the right amount of time/money in the code.
Worthwhile goal (though the desirability and practicality remains debatable), bad execution.
> No, we can. We just don't, because it's very expensive, and we lack proper tooling to make it cheaper and/or faster.
Eh, it depends on how amenable your standards for correctness are to formalization. Also when it comes to security, where clearly bugs tend to hurt a lot more, we're almost always at the mercy of "unproven" (in the formal sense) algorithms. Don't get me started on quantum computing's effects.
Reasoning about concurrent programs (let alone distributed ones) is something where I don't think we've got many reasonable schemes, even at the academic level. Though it's great to hear the Ethereum foundation is willing to drop some cash on that problem! I wish luck to anyone who takes them up on that, it's something I'd love to work on if I didn't have existing projects.
The Ethereum virtual machine isn't concurrent even though the network is. The model is a relatively simple serial sequence of operations, state machine style.
With enough effort, you can prove that your code conforms to the specification, but how do you prove that the specification conforms to your expectations?
You struggle to even do that. You can normally prove that some code conforms to a version of the specification that is explicitly formalised, but in practice, a large number of bugs are specification bugs and that will only increase the more you are forced to formalise the specification.
Sure there's evidence of that. Maybe not in the move-fast break things social/mobile/local web world, but in the mission/safety/life-critical and real-time systems engineering world there is. Just takes a quick google search, for example:
"As one example of Ada in an undergraduate setting, students at Vermont Technical College in the U.S. used the SPARK language (a formally analyzable subset of Ada) to develop the software for a CubeSat satellite that recently completed a successful two-year orbital mission. SPARK was chosen because of its reliability benefits. The students had no previous experience in Ada, SPARK, or formal methods, but were able to quickly come up to speed.
Of the twelve CubeSats from academic institutions that were included in the launch, the one from Vermont Tech was the only one that completed its mission. Many of the others met their doom because of software errors. The Vermont Tech group credits its success to the SPARK approach, which, for example, allowed them to formally demonstrate the absence of run-time errors."
I've read similar success stories for Lisp and Haskell. Rust will likely add more evidence as it becomes more widely used. Agda and Idris are also capable in this respect.
The problem is too many engineers are just day-jobbers, who want to crank out LOC and quickly add features that get them paid, regardless how sloppy their work or the tools they use may be, or how much work/cost it adds to the maintenance overhead down the road. That work can either be done up front writing bug-free code, or later during maintenance putting out fires, but it can't be avoided. Programmers who chose the former use the excuse "bug-free code is impossible so we don't have to try" to justify pushing the work off on the maintenance team later. But it's demonstrably false.
You can write a formally verified, simple Hello World program and prove that it adheres to both your design and implementation specifications. You can this all the way down to how the specific processor will run the resulting machine code.
The catch is that this is difficult and the time and cost both scale non-linearly with the complexity of the software. But if you can do it for dead-simple programs running on hardware you understand very well, you can do it for complex software as well. Just be prepared to pay millions of dollars for it.
> But if you can do it for dead-simple programs running on hardware you understand very well, you can do it for complex software as well.
Not necessarily when you're bounded by reality and finite amounts of time and energy. Just because you can count to 2^8 doesn't mean you can count to 2^128.
Perhaps, but nobody can write a bug-free legal contract either, and no legal system is without bugs.
Sadly, for the legal system, many of the bugs are due to corruption, so they are actually more akin to systematic exploits being done again and again by malicious actors (who often happen to be wealthy or powerful).
Also, in terms of how drastic this bug is, suppose $5M gets stolen over a few days. If the community can strengthen itself and become resilient to a whole class of attacks, that is likely far superior to a meatspace improvement in contract law, which would likely take years to become law (and would be selectively enforced once it did).
> Perhaps, but nobody can write a bug-free legal contract either, and no legal system is without bugs.
The difference is that when there is an issue with a legal contract you can defer to an arbiter (a judge) and discuss whether that is a bug or a feature as soon as a divergence of interpretation is detected.
Hell, even just having a sentient empowered human in the loop is sufficient, with fully automated response systems we'd never have survived the cold war as a civilisation, the first false-positive detection (and there have been several) would have ended it.
You are describing human judgement or human discretion. It's probably a given that AI will surpass humans in judgement and discretion of many things in the coming years and would be at least as able to avoid reacting to a false-positive as any human.
The problem (and the thing you propose as a solution) is deferring to an arbiter. This is not human judgement as much as it is human authority. We conflate the two in meatspace because of the social rank conferred upon such positions (this is the same drive that makes humans bow before gods and dictators)
The very idea of decentralization is a different authority model than what is typically in human institutions. In theory, institutions managed in a decentralized and anonymous way have the potential to achieve a form of democratic governance that is far more resistant to corruption than any form previously invented.
In meatspace, a judge must be chosen, elected/appointed, confirmed, etc., and when that judge needs to be replaced we take an entirely different (largely unknown) judge and do a full-scale migration to that new judge's "firmware".
With smart contracts, we can divide the execution into many smaller smart-contracts, each with a specific domain of expertise. This makes versioning, incremental improvement, and extreme transparency possible.
If you listen to us SCOTUS argument, particularly when a case involves discussion of the intent of specific words in a law, it becomes clear how utterly mutable all of the constructs are. While the SCOTUS is a world-class institution in terms of its overall quality, it is reinforced using a highly centralized model of human authority, with all its problems.
There's nothing preventing a contract from adding fallback modes that require interaction from human agents. Indeed, most of the more high-assurance contracts will probably require this.
I agree, for now. What I argue is that just like nobody can write bug free code, nobody can write bug free contracts as well. I think this might have a good use case down the road once all the bugs are worked out. That said, it's not ready for prime time yet.
"Oh, that contact for 1000 dollars is really 10 dollars because they 'missed' a decimal place. You still have to uphold your part though."
Corruption of judges can be a problem in that space and that is in part what this is attempting to solve. A lofty goal, maybe even impossible, but certainly worth the time to try.
I actually found a typo of a 100x magnitude in a Washington, D.C. law about ten years ago. Submitted it, and it was administratively adjusted. No need to even take it back for another vote. I believe is happens with much greater frequency than anyone outside the business of maintaining legal documents imagines.
[even had a typo in the first publish of this comment!]
Situation was basically a table rendered in prose format. I can’t recall the precise verbiage, but it read something like:
In 2015, the requirement shall be 0.05%. In 2016, the requirement shall be 0.7. In 2017, the requirement shall be 0.09%
Very subtle typo which, had it been treated as The Truth of The Text would have bankrupted anyone attempting to adhere to the regulation.
for obvious fixes, that’s not actual power: They could not do that if the correct answer weren’t obvious.
If I offered a new car for 10€ — obviously it should have been 10k€, so others cannot expect me to fulfil that (ask your local police).
If I had offered it for 8.5k€ and suddenly claim it should have been 10k€, it’s far from obvious that this was a mere error, so I’d likely have to stand for it.
If I offered a used car for 10€, the case becomes murky.
This is hacker news. If this was some code rather than in meatspace and you trusted a single client to modify a turning complete config file for everyone else you'd call it a massive security vulnerability. I don't understand how having humans involved changes that. Yes, they probably have good intentions but has that assumption ever worked out in human history? If it's not used today for something nefarious, it will be used tomorrow.
A legislative body is a conflict resolution mechanism, and one that is basically in the business of writing the code of law (literally). For something to be considered a typo, there must be negligible conflict over that interpretation. If not, the legislative body addresses it again or it’s handled by the judiciary. The legal register who maintains the official version of the text works at the behest of the legislative body. These things are not occurring without supervision.
Aside from everything. In writing a contract, it's very common to write price with numbers and letters in brackets next to them. E.g. 1000$ ( one thousand dollars ), exactly because typos happen.
The decision what a typo is is made by the parties, in case of dispute then by several courts ( based on the evaluation of the contract ). That's at least in continental law system.
There's a way to specify a 3rd party court ( non-corrupted one, called arbitrage ) which can solve disputes for that contract.
Corruption of judges problem is being fixed also in several ways. Usually decisions in high courts are decided by 3 judges ( again continental law ) and sometimes a jury ( prevailing in anglo-saxon law system ). Also there is a way to appeal the decision of the court to a higher court(s).
It's impossible to corrupt a 3rd party judge (shouldn't all courts be third parties?), or 3 judges? I agree it's the best system we have today, but it won't be tomorrow.
There are relatively few cases where $1000 and $10 are both reasonable numbers. It should be pretty obvious to both parties from context which is the 'correct' interpretation.
To a rational person without ulterior motives yes, but remember in my country "The right of the people to be secure in their persons, houses, papers, and effects, against unreasonable searches and seizures, shall not be violated, and no warrants shall issue, but upon probable cause" means "Go ahead and take papers (cash) from peoples cars without warrants, and then the burden is on them to prove they obtained it legally"
I certainly distrust the American legal system enough to use something like this in the future.
No-one can write bug-free code, so why are these people building a huge, expensive system that relies on no bugs being found?