> If you say it's undecidable, it implies no such algorithm can exist.

It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines.

It does not imply that “cycle detection” is an impossible task under any circumstances, possibly on different classes of graphs, or possibly sacrificing strict correctness.

I honestly think you understand this and are just being intentionally obtuse.

> It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines.

Yes, what you said is strictly correct, but that's not how the Halting problem is usually presented nor how it is usually understood.

Normally, you don't hear people saying: "the Halting problem is undecidable for Turing machines", and that's it, everybody understands what's going on and the limitations of that statement.

Instead, it is usually said: "The Halting problem is undecidable". And then they say: "Here, let me show you that it's undecidable using this clever proof, which uses a Turing machine as a model".

And then, more crucially, they don't say "But of course, this proof is completely wrong if you assume that the program runs on a finite-state machine. And not just that, but it is proven that it is decidable in such circumstances".

> I honestly think you understand this and are just being intentionally obtuse.

I understand in general, but I might misunderstand particular statements in some precise way. I'm not intentionally being obtuse, I promise you.

There's a lot of nuance in this topic and when we're not being mathematically precise it's easy to misunderstand each other.

> And then, more crucially, they don't say "But of course, this proof is completely wrong if you assume that the program runs on a finite-state machine. And not just that, but it is proven that it is decidable in such circumstances".

Of course they don’t, because it’s extremely obvious that it’s decidable for finite state machines.

However, in practical terms computers are more usefully modeled as Turing machines than as FSMs (yes, even though pedantically speaking they are FSMs).

> Of course they don’t, because it’s extremely obvious that it’s decidable for finite state machines.

Wow, that's quite an interesting statement to make. And it doesn't explain dozens and dozens of statements that I've read over the years implying that people don't actually understand this.

Hell, even the tutorial that this post is about claims the following, right in the beginning:

> Turing famously showed that computers can’t decide whether your code halts.

Which, of course, is not true, unless you interpret this in a bit of a twisted way by imagining that the algorithm that does the halting analysis is running on a computer but it is only allowed to analyze the program as if it were running on a Turing machine, which is the least useful way to solve this problem.

> However, in practical terms computers are more usefully modeled as Turing machines than as FSMs

I'd argue the exact opposite, because it's obvious that if you do that, it will result in you proving that something is true when for what the real-world cases we care about it is actually false, as well as the "true" proof not actually being useful for almost anything interesting (except math-related results having to do with infinity).

But since you truly understand the implications, then I accept your difference of opinion.

> I'd argue the exact opposite

I'm truly interested in hearing your reasoning beyond "it is obvious to me." What background do you have in this field? Because if we wander over to the papers published in SAS we can look through the ways in which various systems model programs and they do not choose to model physical computers as FSMs. We've got decades of people thinking hard about this problem who've come down on the complete opposite side as you. Maybe literally the entire field is wrong about this. I doubt it.

As I said in my original post, Turing machines can be useful.

But they do a huge simplifying assumption which is that the program can use an infinite amount of memory.

This is OK in some cases, but it is not OK in others, especially when it comes to analyzing decidability (of programs that are not trying to compute mathematical answers, i.e. answers with infinite bounds).

For example, I think it is immensely useful to model computer programs in Turing-complete languages. I see no major reason why we should always use programming languages with enforced memory limits at the language level, currently.

Because, it's one thing to write a program, and it's another thing to execute it.

So, I'm not saying Turing machines are always inadequate. But I wish we would be more careful using them, so as to not make fundamental mistakes about what is true and what is false for important things that we actually care about (rather than strictly theoretical questions about programs that we will never be able to run successfully).