3 ms·

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

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

UncleMeat 4y ago
> 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.
- wizeman 4y ago
  > 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.
  - UncleMeat 4y ago
    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.

UncleMeat 4y ago

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

wizeman 4y ago
> 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.
- UncleMeat 4y ago
  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.