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.
If a smart contract is small enough in scope then eventually you can be reasonably sure it’ll behave the way it’s supposed to.
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.
Once you start combining "small" contracts (e.g. they call into each other), you have a large program one way or the other. The combinatorial explosion pretty much guarantees there will be some input combinations that lead to unexpected consequences, even if you claim to know everything there is to know about each particular component. If there's a way to get around this, I'd be very, very interested in reading about it.
Predicate transformer semantics[1] are an approach that would work with sufficient discipline. Given that the cost of a bug is potentially losing everything, maybe smart contracts will finally be impetus developers need to learn enough of the predicate calculus to compose programs that behave as specified.
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.
Thanks for the reference. I'm currently studying type theory and the Curry-Howard correspondence, and this seems to be an interesting bridge between that and traditional imperative programming.
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.
It sounds like you might appreciate Predicate Calculus and Program Semantics[1] which is a rigorous formal treatment of the subject. Dijkstra's earlier work, A Discipline of Programming[2] lacks mathematical rigor, but is still quite pragmatic and is arguably a much gentler introduction to the subject. It also focuses more on real-world use cases.
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.
Nobody has yet convinced me that the effort spent on blockchain smart contract whatever would not have been better spent un-pretentiously re-writing traditional banking infrastructure with lessons learned in the last 40 or so years.
Good luck with that. Myself and others have lost hope that the current system can ever change. You're never going to convince the people in power to rewrite the current system.
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.
Using a Turing complete scripting language means it does not have a good scalability balance.