> They have the best balance of decentralization, scalability, and security.
Using a Turing complete scripting language means it does not have a good scalability balance.
Using a Turing complete scripting language means it does not have a good scalability balance.
The amount of brainpower needed today to _prove_ that a smart contract does exactly what is intended doesn't scale to a whole financial system. The existing financial system gets away with having "oracles" called judges (in a court). I think we can graft this onto Ethereum by accompanying each smart contract with some natural language that can be interpreted as its "intent", and in the event any bug in the code violates this intent we can bring in a human judge who can decide whether to fork or not.
On the other side, I think any sufficiently strong theorem-proving strategy will resemble simply limiting yourself to a non-Turing-complete subset of the language.
With enough of these contracts you start to build a financial operating system that can be relied upon.
However I do think the human component is underrated in the crypto space. I imagine the future will consist of humans being injected into the financial operating system itself instead of bypassing it like you describe.
That's just half of the problem though. The other half is knowing that your specification doesn't admit any unpleasant behaviors. I expect some combination of KISS and model checking is appropriate.
[1] https://en.wikipedia.org/wiki/Predicate_transformer_semantic...
As for the second part, do you know off the top of your head if [not checking whether the proved behavior admits abuse] was the issue that resulted in "millions of dollars" worth of coins being stolen in the various debacles we hear about? I have an inkling that almost every time, it's actually this.
The only one I ever looked into was the 2016 DAO[1] hack and I didn't get the impression that it was because they didn't check their code for spec violations, rather they just designed a system that allowed someone to do something bad. I have no idea how we can prevent this, even with all the power of theorem provers.
Like most of his work, the general theme is "how can we avoid making a mess of things unnecessarily?" Avoiding needless complexity is clearly the programmer's greatest challenge.
[1] https://www.goodreads.com/book/show/3144463-predicate-calcul...
[2] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...
It means that a single transaction can be very computationally expensive, compared to a Bitcoin transaction that is very simple, meaning that it's exponentially harder to scale Ethereum than to scale Bitcoin.