| > The halting problem is undecidable over all possible Turing machines (i.e. programs, assuming Turing machines are an adequate model for the sort of programs of interest). It is entirely possible to choose some subset for which you know how to decide the halting problem, and program within the that subset. No. Think about what you're saying. To be able to choose from among useful, nontrivial programs, those to whom the unsolved Turing halting problem doesn't apply, is to solve the Turing halting problem. > It is a matter of cleverness (rather, successful algorithm design and theorem proving) how large you can make that subset. This is a first-class logical error. Choosing the subset as you suggest, is equivalent to solving the Turing Halting problem, yet the problem is known to be insoluble. Surely you see this. > This subset, this language, will necessarily exclude universal Turing Machines and other forms of interpreters — but I see no particular reason this is a problem for writing power plant control systems. There is no other way to say this -- you are mistaken, in the most basic way. The Turing halting problem is not the common cold, that you can wait out, nor is it a question of language design, that you can finesse. It is fundamental, and the original claim -- approximately "prove to be failsafe" -- is not possible for any program more complex than "Hello World". If you want a failsafe program to regulate your drilling operation or nuclear power plant, yes, you can have it, but all it can do is print "Hello World" over and over again. If instead you want a useful program, one that can actually do useful work, you must accept that the Turing halting problem is (a) unsolved, and (b) insoluble. > It is a matter of cleverness ... It is not a matter of cleverness. It is a problem of understanding the limits of technology. |