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.
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.