I think you can reason it like this. Assuming certain constraints (what you can define bounded analysis rules for) you can prove that things terminate. These r

I think you can reason it like this. Assuming certain constraints (what you can define bounded analysis rules for) you can prove that things terminate. These rules things are usually far more advanced than we suspect initially, but they're not still not fully unbounded.(And we can often come up with more rules to make things practical even if unwieldy) Deciding termination for an arbitrarily large program in a turing complete system CAN require no less than execution of such a program thus we CANNOT guarantee to be able to verify termination for EVERY program. (This is the halting problem) I spent a lot of time on my thesis learning about type inference systems and as many such systems for uncooperative languages(JS,Python,etc) need to do abstract interpretation they fall into the same kind of issues and this is why practical systems use JIT compilation instead of AOT even if there are exceptions (Shed Skin Python is quite impressive for example).