4 ms·

Why though? The halting problem is interesting. The fact that there is a proof that it isn't possible for a certain class of inputs, doesn't mean it is imposs

Why though? The halting problem is interesting. The fact that there is a proof that it isn't possible for a certain class of inputs, doesn't mean it is impossible for all inputs. Where is the line? Can we solve it for practical programs? Can we solve it in a non binary manor "Program XYZ halts for inputs UVW, but not for inputs RST"? To me the halting problem proof suggests way more questions than it answers.

UncleMeat 5y ago
Those questions have themselves been solved. Static analysis works in practice, even for very intricate properties.
- nh43de 5y ago
  From the paper: "Interestingly, reduced versions of the decidability problem have produced a fruitful area of re-search: formal verification, whose objective is to produce techniques to verify the correctness of computer programs and ensure they satisfy desirable properties (Vardi & Wolper, 1986). However, these techniques are only available to highly restricted classes of programs and inputs, and have been used in safety-critical applications such as train scheduling. But the approach of considering restricted classes of programs and inputs cannot be useful to the containment of superintelligence. Superintelligent machines, those Bostrom is interested in, are written in Turing-complete programming languages, are equipped with powerful sensors, and have the state of the world as their input. This seems unavoidable if we are to program machines to help us with the hardest problems facing society, such as epidemics, poverty, and climate change. These problems forbid the limitations im-posed by available formal verification techniques, rendering those techniques unusable at this grand scale."
  - UncleMeat 5y ago
    Wow. That's just... not true. Not even a little. The authors have totally incorrect and limited understanding of the state of static analysis.

UncleMeat 5y ago

Those questions have themselves been solved. Static analysis works in practice, even for very intricate properties.

nh43de 5y ago
From the paper: "Interestingly, reduced versions of the decidability problem have produced a fruitful area of re-search: formal verification, whose objective is to produce techniques to verify the correctness of computer programs and ensure they satisfy desirable properties (Vardi & Wolper, 1986). However, these techniques are only available to highly restricted classes of programs and inputs, and have been used in safety-critical applications such as train scheduling. But the approach of considering restricted classes of programs and inputs cannot be useful to the containment of superintelligence. Superintelligent machines, those Bostrom is interested in, are written in Turing-complete programming languages, are equipped with powerful sensors, and have the state of the world as their input. This seems unavoidable if we are to program machines to help us with the hardest problems facing society, such as epidemics, poverty, and climate change. These problems forbid the limitations im-posed by available formal verification techniques, rendering those techniques unusable at this grand scale."
- UncleMeat 5y ago
  Wow. That's just... not true. Not even a little. The authors have totally incorrect and limited understanding of the state of static analysis.