> What I am saying is that in practice, for the huge majority of interesting problems, it is not useful to finitize the actual program but instead to abstract over the program that assumes no meaningful resource constraints. Wandering off down a road of looking for efficient algorithms that take advantage of the actual finite nature of real programs will only harm you in the enormous majority of cases.

You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong.

> Again, people only "get it wrong" if you are being maximally pedantic in a way that provides negative value to thinking about these problems.

If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.

Fortunately, some people have proven that these algorithms exist and have created such algorithms. Some have even created new such algorithms, improving their efficiency.

I just want more people to try and find more efficient versions of those, which is why we should not be spreading mistaken beliefs that the Halting problem is undecidable when a program runs on a computer.

Which is why I would argue, in fact, that saying the Halting problem is undecidable is what provides negative value, because this is only of theoretical interest and generally speaking, it's only a useful result in practice if the program you're analyzing is trying to solve a mathematical question (i.e. one about infinity).

For most real-world programs, the question of whether they would halt (or whether they behave correctly, in general) if they weren't allowed to consume infinite memory is much more interesting and useful, and actually decidable!

So let's focus instead on improving the time complexity of such algorithms. Let's not focus on saying that they are impossible to solve, which prevents from focusing on the former.

> You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong.

The entire thread started off by you rejecting the formalism provided by folks like Turing in favor of the practical argument. I'm speaking from a practical perspective of building actual static analysis tools. When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best.

> If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.

No that's not true. Not at all. We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems.

There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Actual deployed algorithms have some number of false positives or false negatives (or both).

> When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best.

That's not what I'm arguing at all. I'm arguing that as long as you restrict the programs being analyzed to the subset of programs that use a finite amount of memory (i.e. those that can run on a computer), then all so-called undecidable theories suddenly become decidable. And that this could be a property that we could perhaps exploit to analyze programs more efficiently.

But you don't have to make your models more complicated. It's simply a property that you can exploit, whenever you want to.

> We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice.

Exactly. Wouldn't it be better if you could always have true positives and true negatives?

To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO.

> We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems.

It is decidable, that's my entire point! If there's a finite amount of memory, the theories become decidable!

Perhaps you're just confusing time complexity with decidability?

> There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time.

Exactly, there isn't! Which is why we should find one that terminates in a reasonable amount of time. That's what I'm arguing.

> Actual deployed algorithms have some number of false positives or false negatives (or both).

Agreed.

> That's not what I'm arguing at all. I'm arguing that as long as you restrict the programs being analyzed to the subset of programs that use a finite amount of memory (i.e. those that can run on a computer), then all so-called undecidable theories suddenly become decidable. And that this could be a property that we could perhaps exploit to analyze programs more efficiently.

Well this one is just plain wrong. It is "if my grandmother had wheels she'd be a lawnmower." What you are saying is "if you change the problem, the properties of the problem change." Yes, the set of turing machines that halt in fewer than some fixed N steps is decidable. This is not interesting. It is pedantry.

> Exactly. Wouldn't it be better if you could always have true positives and true negatives? To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO.

But it isn't. And I've told you. You'll increase the running time of useful programs by hideous amounts. Like "won't finish executing until the universe ends" amounts.

> Perhaps you're just confusing time complexity with decidability?

I am not.

> Well this one is just plain wrong. (...) Yes, the set of turing machines that halt in fewer than some fixed N steps is decidable.

That is NOT the problem I mentioned. Programs that use a finite amount of memory do not necessarily halt, ever!

But the problem I mentioned is also decidable. We already know of algorithms that can always determine if a program that uses a finite amount of memory halts or not.

> This is not interesting. It is pedantry.

Actually, what is not interesting is analyzing problems that can only exist on super-powerful imaginary machines (i.e. with a truly mathematically infinite tape, which is a very absurd feature to have) that do not fundamentally represent what computers can do.

In the real world, truly infinitely-large things (and I'm talking about true mathematical infinity) cannot ever exist or be built. And even if they were to exist, they would never be accessible to us.

So I'd prefer to have a model of computation that functionally represents what computers can actually do and then extract my conclusions using this model (in which many problems are decidable), rather than an imaginary super-powerful model which actually has more limitations (as many problems are undecidable) than models of computers.

I mean, if you like solving imaginary problems that do not represent what can exist or be built in the real world, I mean, sure, fine, that's OK with me. But if you use such an absurd model, then don't extract absurd conclusions and then tell me that these conclusions apply to real computers.

> But it isn't. And I've told you. You'll increase the running time of useful programs by hideous amounts. Like "won't finish executing until the universe ends" amounts.

No. Restricting yourself to analyzing a subset of problems does not "increase the running time" of anything.

Why? Because you can use the same algorithms that work for analyzing programs that use infinite memory (the undecidable ones) and you can also use additional algorithms that only work for programs that use finite memory (the decidable ones).

Which means that you have additional tools at your disposal, which means that the problem can be solved in an equal or better way.

To be clear, I'm not saying that we currently know of such efficient algorithms that only work for programs that use finite memory.

I'm saying that it might be possible to create such algorithms given that the problem is decidable.

The problem you mentioned is decidable. Nobody other than you is talking about that problem. This is for two reasons. It is not theoretically interesting and it is not practically useful. Again, this is "if my grandma had wheels she'd be a lawnmower."

You keep insisting that this reframing can somehow lead to more efficient practical systems. It will not. As evidence, I point to five decades of research on practical static analysis where nobody has come to the conclusion that explicitly modeling the finite nature of real computers is useful in the slightest. The "additional tools at your disposal" are literally useless.

And if you ignore this property (as you now mention) then what have you gained through your reframing? Nothing. All you've done is added additional complexity to a problem formulation for no gain.

You keep hiding behind "might." This is just magical thinking.

Ok, for the sake of argument I will agree with you on "it's not practically useful" (for now, at least).

But I will disagree with you on "it's not theoretically interesting".

Almost the entire field of computer science is based on Turing machines and on the following definition of "computable function": "computable functions are exactly the functions that can be calculated using a mechanical calculation device given unlimited amounts of time and storage space".

Now, of course, I can argue that this definition of computable function and Turing machines are ridiculous and will lead to ridiculous conclusions, but I think I already did that elsewhere, so let's move on.

Now imagine that instead of Turing machines, computer science would use deterministic linear bounded automatons (deterministic LBAs, which are the closest finite approximation of Turing machines).

And instead of that definition of computable function, let's use this one: "computable functions are exactly the functions that can be calculated using a mechanical calculation device given unlimited amounts of time but limited amounts of storage space".

What would be different in computer science?

Well, at least the following would be different:

1. The Halting problem becomes decidable

2. Rice's theorem becomes false, which means we can decide properties about computable functions.

3. As an example, perhaps you're familiar with the busy beaver problem, which is defined over Turing machines and is a function of N, where N is the number of states of the Turing machine. It is impossible to create an algorithm to decide whether a Turing machine is a busy beaver.

If you defined the busy beaver problem over deterministic linear bounded automatons (LBAs) adding an additional parameter K for the length of the tape, then suddenly it becomes possible to create an algorithm that determines whether a given LBA is a busy beaver!

Similarly, the busy beaver function is defined over Turing machines and is a function of N (where N = number of states).

In my redesigned field of computer science, the busy beaver function would also be defined over deterministic LBAs and would be a function of N and K, where N is the same as above, and K is the length of the LBA tape.

This would also have interesting consequences.

First of all, the busy beaver function would become a computable function instead of non-computable.

It would also become more meaningful in the real world, because we could answer the question: my computer has K bits, how many 1 bits could a halting program with N states write?

And you would still be able to answer the original questions about the original busy beaver, which you would realize is not a computing question, but it is actually a mathematical question concerning infinite Ks, which is: "for a fixed N and for all K, what is max(busy_beaver_function(N, K))?".

There's also an interesting additional mathematical question that would come up: for all N and for all K, is it true that if busy_beaver_function(N, K) = busy_beaver_function(N, K+1) then there is no J such that busy_beaver_function(N, J) > busy_beaver_function(N, K)?

In other words, if you increase K and the busy beaver function gives you the same result, does that mean that there is no point in increasing K any more because no higher K will give you a larger result?

What if you step-wise increase K by multiplying by 2 instead of adding 1?

Presumably, the above questions have to be false, otherwise the original busy beaver function would be computable, but it would still be interesting to have separate proofs, which could lead to new insights, especially if you didn't know that the original busy beaver function was non-computable!

All sorts of similar reasoning would apply to all sorts of other problems. Many undecidable problems become decidable. Many non-computable functions would become computable. Many questions that were previously about Turing machines suddenly become more meaningful for actual computers. You would naturally ask more interesting (finite and infinite) questions as functions of state size.

And, you could still answer the same mathematical questions about them (that we currently use Turing machines for), just by introducing a "for all" quantifier in the state size. Which would also make many things a lot clearer.

I could go on and on.

(To be clear: a computable function does not imply that it can be efficiently computed, i.e. computed within a reasonable amount of time. This is true both for the current definition and my definition).

> You may very well be correct, but there's no formal result that proves that, right?

GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world.

> If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.

This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.

> GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world.

Ok, I see your points.

> This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.

It doesn't?

I thought the halting problem was the problem of constructing an algorithm that decides whether a machine that runs an arbitrary program will keep cycling between states or not (which in the case of a Turing machine, includes the state of the tape).

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

> 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).