> Caveat, the thing that makes it decidable is not the fact that it was going to run on a computer with finite memory, the SMT solver will fail on many code chunks that can run on your computer.
And what does that say about the problem, that current SMT solvers fail?
It only implies that it's a difficult problem to solve (i.e. that the time complexity may be large, possibly), but it doesn't prove that it necessarily has to be that way.
> (And that's more or less the claim of the halting theorem, not that nothing useful can be done, but that anything done can only be heuristic.)
I don't think the Halting problem proves anything about the complexity of the problem or whether you can only apply heuristics and not solve the problem in a principled way. In fact, cycle detection algorithms work deterministically, without any use of heuristics.
The proof of the Halting problem only works because in Turing machines, programs are allowed to consume memory infinitely without ever running into a cycle. If you don't allow that, then the Halting theorem doesn't say anything.
> This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language
You mean, Turing-complete languages. In which case I agree, normal programming languages also make the simplifying assumption that the computer has infinite memory.
Which is actually OK!
That these programs are written in such languages doesn't prevent an algorithm from determining whether an arbitrary program written in such a language will halt or not, if it were to be executed in a machine with a finite amount of memory.
> you would get the result “this program will OOM, but if you run me in a machine with 1 meg less memory I will stop an odd number of cycles earlier and the program will not OOM, but will instead halt successfully telling you that the next cycle would OOM.”
Yes, exactly!
> Suddenly your tests that you build with this thing are all flaky, because it didn't have the humility to be a heuristic and say “I don't know this is too complex for me,” and in the real world you are running on Linux and you don't know how many megs you really have available. Better just to not play any of that game.
Actually, I would argue that it would be immensely useful to be able to run such a tool and that it would tell me:
"Hey, your program will OOM even if you run it with 1 TB of memory!"
Or even, say, 16 GB of memory.
Of course, with this value being configurable. And also, take into consideration that you'd be able to know exactly why that happens.
> So yeah the problem with Turing machines is not that they have infinite memory, infinite memory is in fact a standard assumption that most programmers in GCed languages make when programming most of their programs.
Yes, and I see nothing wrong with that. Although I would like a tool like described above which would determine whether my program is buggy.
> Put another way, Turing machines suck even if you enhance them to have 5 parallel tapes (God why do they not have parallel tapes by default, should have at least one for output, one for main memory, one for a stack, and some more as scratchpads) of bytes (seriously why are they still not bytes in textbooks) and enforce that the tapes each only have 1 billion symbols and any attempt to go off the edge crashes the Turing machine
Sure, but why would you do that? When analyzing cycle detection algorithms (which assume a finite amount of possible states) you don't do any of that crap :)
> You are joyous because it now only has finite memory, I can run a cycle detection with 10^{1 billion} nodes in the graph or whatever, so cycle detection is in principle solved! If you are as pragmatic as you say you are, you see that this is no help, halting is still effectively impossible.
Yes, it's solved! Awesome!
Not let's focus on how to reduce the time complexity, which is the actual important problem!
And don't assume that cycle detection needs to run a program step by step through all of the states of the program.