> undecidability can sneak into the requirements in forms that are not immediately recognizable.

The whole issue is loops and recursions (more complicated loops). And how to avoid the bad sort is to inspect your invariants. For classic loops, you need to prove that your condition will eventually be false. For iterators, you need to prove that your data is bounded. And for recursion, that the base case will eventually happens. The first two are easier to enforce.

The goal is for your code to be linear. If you have code as one of your input, you force it to be linear too.