As I attempted to say in my previous comment, undecidability[1] isn't limited to deciding if a program will halt (or even the weaker question of if it will halt in a given finite time). Recursively enumerable[2] languages that require a Turing machine to automate have an intrinsic complexity (i.e. any Turing-complete language). This isn't a "work harder to solve it" level of complexity; some behavior will always be undecidable.
You might experience this problem in the traditional form of the "Halting Problem" where the question "Will this program halt?" may be answered with "I don't know, it's still running" in addition to "yes" or "no". However, this level of complexity can also cause unexpected output due to subtle interactions inside the program that are difficult to predict from the source. Some behaviors are provably unknowable.
You can avoid this problem by using a simpler class of language. Regular languages (which "regular expression" match[3]) are safe, as are deterministic context-free[4] languages. You may find the lack of loops limiting.
[1] https://en.wikipedia.org/wiki/Undecidable_problem
[2] https://en.wikipedia.org/wiki/Chomsky_hierarchy#Type-0_gramm...
[3] basic regexp, not PCRE or other language-sepcific extensions!
[4] https://en.wikipedia.org/wiki/Context-free_grammar#Undecidab...
What if Ethereum offered a non-turning-complete subset of Solidity (that included formal verification) which could optionally be used in smart contracts. Would this cause you to view the platform differently?
Arguably unclear termination semantics would be a good reason not to trust a contract. Ideally trust mechanisms would exist such that closed source contracts were trustable via a pure insurance-based mechanism.