i enjoyed skimming the paper, but i don't agree to your conclusions. It reminds me of an recent discussion i had about Dependent Types in Haskell, why not just check for termination instead of asserting it (I know about the halting problem)?

I think for many applications there is no binary answer, it's not just a good or bad idea. The question is how good can we get and is it any better than the state of the art? There are theoretical limits, but the interesting part is whether there exists a practical approximation. I don't believe in a fundamental difference between us and computers, i think everything we can reason about should be possible to algorithmically reason about. I think smart-contracts are a fundamental improvement over "non-code as law", i really believe in them. They are reproducible and exact. But it's a shame that solidity is so badly engineered, because they it is really hard to prove anything in it. I think they did the exact opposite of what would be the right language. I understand the reasoning behind "the limits of correctness", but does this means that proving anything is meaningless?

I would expect most contracts to be stupidly simpel, at least to a machine, with simpel properties that need to be proven comparable to testing Haskell with quickcheck. And i believe they are an improvement over "non-code as law", even if not provably correct.

The problem with bugs and smart-contracts is interesting. But implementing smart-contracts does not mean automating the judge.