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