I commented in a similar vein on a piece that said that smart contract environments should never use Turing-complete languages because of the undecidability of program properties: https://news.ycombinator.com/item?id=11942015 (That piece seemed to have a misconception that you can never prove properties of programs, rather than that you can't always prove properties of programs.)