5 ms·

> Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care abou

> Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself. I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. In fact, this would be a huge, huge deal if you could solve it in an efficient way. > There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much. I think you missed one of my points: > while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But we don't know whether P=NP. And there's another issue here as well: I'm not even sure if P=NP actually has any meaning in this context, because I assume issues related to P=NP are usually analyzed in the context of Turing machines. This actually ties into the other point I mentioned: > How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?

markusde 4y ago
> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. Fair for many applications. I work with computers that write proofs. > Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But there's another issue here as well: we don't know whether P=NP. There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. > How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Well, not me! Formal methods and program synthesis are alive and well, but it's important to researchers in these areas to understand what parts of our work are decidable and what aren't. I should mention that Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, and tailoring tools to real user patterns can really blunt the problem of undecidability in practical use cases.
- wizeman 4y ago
  > There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. I mentioned this in another comment: isn't EXPTIME only defined for Turing machines? Which again, just touches on all of my points. For all we know, if you've reached the conclusion that an algorithm's complexity is EXPTIME, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers. > Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, My point is that you shouldn't believe that the theories are undecidable because those analysis were done using Turing machines as models. And the other point is that sure, there are many people doing formal methods, etc. But how many more would there be if most people believed the problem to be solvable?
  - markusde 4y ago
    I think I see what you're getting at. A few final points: - There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM. - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist. edit: typo
    - wizeman 4y ago
      > - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. So I'm not 100% sure that those measures of complexity have the same real-world meaning, for similar reasons. > - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. Yes, but even in that case, the amount of memory would be finite. Because the universe is expanding faster than the speed of light, there's only a finite amount of energy that is accessible at any point of spacetime (as far as I understand). So even in theory you can't say the amount of memory can scale infinitely (not to mention in practice). > - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. The theories are undecidable only if you assume a model of computation with infinite memory. Which can be interesting from the mathematical point of view, but not for applying those results to real-world problems, because now you've made a grave mistake: you believe something is undecidable when it is in fact decidable. I mean, sure, I can also invent a new super-duper-amazing model of computation that is even more powerful than Turing machines and can perform incredible Oracle-like feats and, say, run all programs in constant-time (yeah!), but it would not be correct to say that all the results obtained in this model apply to the real world. If an SMT solver is trying to prove that my program has a bug, even though some theory says that the problem is undecidable if my program was running on a theoretical Turing machine, this is meaningless to me (and quite misleading) because the problem is actually decidable given that my program is going to run on a computer. > No stronger method of computation which can also be physically implemented is known to exist. You say that like Turing machines can be physically implemented.
kaba0 4y ago
Well, I may be writing stupid things in the following, but have a look at the Busy Beaver problem. Even for tiny tiny state sizes it will grow faster than any computable function — so for a sufficiently complex property you would effectively have to iterate over this problem space. No matter if even P=NP, that is just.. literally bigger than any function you could make up.
- wizeman 4y ago
  > so for a sufficiently complex property you would effectively have to iterate over this problem space. Why? Why are you assuming that the only way to figure out if a program halts is by simulating running it step by step? And not by analyzing the description of the program?
  - kaba0 4y ago
    You can analyze it, and for that you would use some system like logic. But it so happens that these pesky mathematicians are everywhere, because any sufficiently complex system will fall victim of Gödel. And in fact, Math itself is limited and trivially overstepped by Turing machines, but you are free to create any other reasoning system, it will also fall short of Turing. So, will you believe that these people (I believe Gödel was praised highly by even Neumann!) weren’t talking out of their asses? :D
    - wizeman 4y ago
      Gödel proved things about the limits of math and logic. What does that have to do with how long a specific algorithm takes to run?
      - kaba0 4y ago
        Well, if not by running them and not by analyzing them (any rule system, not just logic is affected), what is your proposed.. whatever to say whether they halt or not? Or any other non-trivial, semantic property?
UncleMeat 4y ago
> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. Great. And the entire field of static analysis is available for you to do this. But when discussing the formal consequences of the halting problem it is just completely pedantic to show up and point out that actually you can run Coverity and it'll spit out some pretty useful results on most programs.
- wizeman 4y ago
  > Great. And the entire field of static analysis is available for you to do this. But when discussing the formal consequences of the halting problem it is just completely pedantic to show up and point out that actually you can run Coverity and it'll spit out some pretty useful results on most programs. I'm glad that my points were so clear and obvious to you!
mannykannot 4y ago
> This actually ties into the other point I mentioned: >> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Few if any, as those who are good enough have no difficulty understanding both the seminal importance of Turing's work and the realities of actual computing devices.
- wizeman 4y ago
  I agree a bit with your point, but still, given how little it is usually emphasized that the Halting problem is not valid for finite-state machines I'm not sure that even very smart people don't mistakenly end up believing that it is.
  - mannykannot 4y ago
    You appear to have a low opinion of other people's cognitive abilities. In that light, perhaps you should consider the possibility that your position, which strenuously attempts to imply that there is a serious cognitive dissonance here, could complicate understanding these matters for someone who is approaching them for the first time.

markusde 4y ago

> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. Fair for many applications. I work with computers that write proofs. > Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But there's another issue here as well: we don't know whether P=NP. There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. > How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Well, not me! Formal methods and program synthesis are alive and well, but it's important to researchers in these areas to understand what parts of our work are decidable and what aren't. I should mention that Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, and tailoring tools to real user patterns can really blunt the problem of undecidability in practical use cases.

wizeman 4y ago
> There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem. I mentioned this in another comment: isn't EXPTIME only defined for Turing machines? Which again, just touches on all of my points. For all we know, if you've reached the conclusion that an algorithm's complexity is EXPTIME, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers. > Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, My point is that you shouldn't believe that the theories are undecidable because those analysis were done using Turing machines as models. And the other point is that sure, there are many people doing formal methods, etc. But how many more would there be if most people believed the problem to be solvable?
- markusde 4y ago
  I think I see what you're getting at. A few final points: - There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM. - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist. edit: typo
  - wizeman 4y ago
    > - Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity. Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me. So I'm not 100% sure that those measures of complexity have the same real-world meaning, for similar reasons. > - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe. Yes, but even in that case, the amount of memory would be finite. Because the universe is expanding faster than the speed of light, there's only a finite amount of energy that is accessible at any point of spacetime (as far as I understand). So even in theory you can't say the amount of memory can scale infinitely (not to mention in practice). > - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. The theories are undecidable only if you assume a model of computation with infinite memory. Which can be interesting from the mathematical point of view, but not for applying those results to real-world problems, because now you've made a grave mistake: you believe something is undecidable when it is in fact decidable. I mean, sure, I can also invent a new super-duper-amazing model of computation that is even more powerful than Turing machines and can perform incredible Oracle-like feats and, say, run all programs in constant-time (yeah!), but it would not be correct to say that all the results obtained in this model apply to the real world. If an SMT solver is trying to prove that my program has a bug, even though some theory says that the problem is undecidable if my program was running on a theoretical Turing machine, this is meaningless to me (and quite misleading) because the problem is actually decidable given that my program is going to run on a computer. > No stronger method of computation which can also be physically implemented is known to exist. You say that like Turing machines can be physically implemented.

kaba0 4y ago

Well, I may be writing stupid things in the following, but have a look at the Busy Beaver problem. Even for tiny tiny state sizes it will grow faster than any computable function — so for a sufficiently complex property you would effectively have to iterate over this problem space. No matter if even P=NP, that is just.. literally bigger than any function you could make up.

wizeman 4y ago
> so for a sufficiently complex property you would effectively have to iterate over this problem space. Why? Why are you assuming that the only way to figure out if a program halts is by simulating running it step by step? And not by analyzing the description of the program?
- kaba0 4y ago
  You can analyze it, and for that you would use some system like logic. But it so happens that these pesky mathematicians are everywhere, because any sufficiently complex system will fall victim of Gödel. And in fact, Math itself is limited and trivially overstepped by Turing machines, but you are free to create any other reasoning system, it will also fall short of Turing. So, will you believe that these people (I believe Gödel was praised highly by even Neumann!) weren’t talking out of their asses? :D
  - wizeman 4y ago
    Gödel proved things about the limits of math and logic. What does that have to do with how long a specific algorithm takes to run?
    - kaba0 4y ago
      Well, if not by running them and not by analyzing them (any rule system, not just logic is affected), what is your proposed.. whatever to say whether they halt or not? Or any other non-trivial, semantic property?

UncleMeat 4y ago

> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever. Great. And the entire field of static analysis is available for you to do this. But when discussing the formal consequences of the halting problem it is just completely pedantic to show up and point out that actually you can run Coverity and it'll spit out some pretty useful results on most programs.

wizeman 4y ago
> Great. And the entire field of static analysis is available for you to do this. But when discussing the formal consequences of the halting problem it is just completely pedantic to show up and point out that actually you can run Coverity and it'll spit out some pretty useful results on most programs. I'm glad that my points were so clear and obvious to you!

mannykannot 4y ago

> This actually ties into the other point I mentioned: >> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Few if any, as those who are good enough have no difficulty understanding both the seminal importance of Turing's work and the realities of actual computing devices.

wizeman 4y ago
I agree a bit with your point, but still, given how little it is usually emphasized that the Halting problem is not valid for finite-state machines I'm not sure that even very smart people don't mistakenly end up believing that it is.
- mannykannot 4y ago
  You appear to have a low opinion of other people's cognitive abilities. In that light, perhaps you should consider the possibility that your position, which strenuously attempts to imply that there is a serious cognitive dissonance here, could complicate understanding these matters for someone who is approaching them for the first time.