Stupid question, isn't this the Halting Problem?
Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps.
See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/...
Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving.
Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...
[1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...
An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction.
It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case.
In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.