> That clearly doesn't hold for any current programming language. To be fair, programming language != implementation. A language can be Turing complete without

> That clearly doesn't hold for any current programming language. To be fair, programming language != implementation. A language can be Turing complete without the implementation being complete. > to solve the halting problem where memory size is fixed and finite Just to clarify any lost reader: The halting problem describes halting on Turing Machines, the algorithm presented only works because Turing Machines that have finite memory are not Turing Machines. > For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust). This is for me the most interesting part of your comment and something I have also thought about. This lead me in an interesting rabbit hole: Most of the lines of code we write don't require Turing Completeness. i.e. When we do `for i in 0..10` we are iterating over a finite range of memory, we can prove we will finish (which appears to be easier than proving we will not finish). If you loop a finite set of times and do a finite set of work each time you will eventually finish. This made me realize that if you know your input, the only regions of code something like what you are proposing would work are `while True` loops, recursive code, stream consumption (which in reality is just a fancy version of a while True), and functions where you cannot prove if the number of loops is finite (i.e Some inner part of the loop may reset the outer loop), etc...(there are some other examples out of scope). From those, it looks to me like only the last group would truly benefit, the rest are relatively easy to spot. But notice the big caveat, all of this only works at runtime (when you know the amount of work you have to do per loop). At compile time, it only really works for really small regions of code. So as far as I can reason, this kind of static analysis would not be as beneficial as one may originally think.