In the general case, there can be cases where it's simply straight up undecidable. (Think of a while loop going for as long as it finds a counterexample to insert your unsolved math problem of your choice) and call a free after. Sure, it's a very contrived example but similar "basically impenetrable barriers" do happen.

But the more common case is simply that each line of code gets some limited "thinking", whether it's inside the model's weights, a thinking block, or a whole turn. Only repeated turns can reason for arbitrary depths, so it's just not necessarily a good use of any of these buckets to spend on something we have a good and efficient algorithm for. Plus any of the former are stochastic which may accidentally ignore true issues (just like humans).

Because LLMs are statistical. They can, with a given probability, avoid memory issues, but cannot prove the non-existance of memory issues in the way that that borrow checkers and other formal methods can.