2 ms·

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 tr

by skulk 5y ago

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. [1]: https://en.wikipedia.org/wiki/The_DAO_(organization) https://en.wikipedia.org/wiki/The_DAO_(organization)

User23 5y ago
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-calculus-and-program-semantics https://www.goodreads.com/book/show/3144463-predicate-calcul... [2] https://www.goodreads.com/book/show/2276288.A_Discipline_of_Programming https://www.goodreads.com/book/show/2276288.A_Discipline_of_...