Turing completeness is a red herring in such contexts. People who may know about the undecidability of halting for programs in Turing complete languages are und

Turing completeness is a red herring in such contexts. People who may know about the undecidability of halting for programs in Turing complete languages are under the impression that if a language is not Turing complete (and is therefore decidable), then analysing a program in such a language would generally be easier in practice (if not downright easy) than a program in a Turing complete language. This is quite simply completely and utterly wrong, because decidability is not a relevant bar for feasibility (tractability). TQBF [1] is already well beyond our practical powers of sound program analysis (and there aren't even good heuristics as for SAT), and to be reducible from TQBF all you need are boolean variables and either functions (even if recursion is disallowed) or loops restricted to two iterations (corresponding to quantifying over true and false). Even P=NP won't help you when you're PSAPCE-complete. In other words, once you're PSPACE-complete, sound analysis is already intractable. Not being Turing complete makes no further practical difference ("sure, analysing a program will take longer than the heat-death of the universe, but we take comfort in the fact that it's bounded!"). Decidability is an older and more famous notion than tractability, but in computational complexity and in program analysis we care about the latter (the former matters only so far as if something is undecidable then it's also intractable). [1]: https://en.wikipedia.org/wiki/True_quantified_Boolean_formula https://en.wikipedia.org/wiki/True_quantified_Boolean_formul...