It would be safer in many of these ways to prefer non-Turing-complete smart contracts -- and non-Turing-complete software environments in general for many tasks -- but I think formal undecidability is something of a red herring here because not all programs' behavior is undecidable. My previous comments on this issue in this context:

https://news.ycombinator.com/item?id=11942015