Re:Vitalik Buterin Proposes New EIP to Tackle Ethereum’s Sky...
by User23 on Monday November 29, 2021 @08:50PM
(#29387832)
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.
[1] https://www.goodreads.com/book/show/3144463-predicate-calcul...
[2] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...
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.
[1]: https://en.wikipedia.org/wiki/The_DAO_(organization)