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.
It is a matter of cleverness (rather, successful algorithm design and theorem proving) how large you can make that subset. Such a subset could, for example, consist of programs written in a particular (non-Turing-complete) language, such that it is known how to construct a proof of (non-)halting because the structure of the program corresponds to the structure of a proof assembled from parts corresponding to the language's constructs.
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.
The structure of the above argument applies just as well to characteristics other than halting. For example, one can straightforwardly prove that any program does not access unallocated memory, provided that that program was written in a memory-safe language; the language is designed such that none of its constructs, nor any composition thereof, can be caused to do so. The analogous impossibility condition for this example is that you cannot express a C (or other non-memory-safe language) implementation in this language (without a virtual memory layer).
> 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.
Choosing such a subset is not solving the halting problem. The halting problem says it is impossible to find a mechanical procedure that says whether an arbitrary program will halt. If a mathematician, by some intuition, is able to come up with a subset of programs for which some property can be proven, then this is not solving the general problem. Since this subset is not equal to the general set of programs, nor has it been found by some mechanical, formal means, it is not a violation of the theory of the halting problem. It can be a matter of a carefully crafted programming language, along with certain annotations (e.g., dependent types). Really, before making insistent statements like this, you should do some research (e.g. there's the whole field of program verification).
It is a matter of cleverness (rather, successful algorithm design and theorem proving) how large you can make that subset. Such a subset could, for example, consist of programs written in a particular (non-Turing-complete) language, such that it is known how to construct a proof of (non-)halting because the structure of the program corresponds to the structure of a proof assembled from parts corresponding to the language's constructs.
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.
The structure of the above argument applies just as well to characteristics other than halting. For example, one can straightforwardly prove that any program does not access unallocated memory, provided that that program was written in a memory-safe language; the language is designed such that none of its constructs, nor any composition thereof, can be caused to do so. The analogous impossibility condition for this example is that you cannot express a C (or other non-memory-safe language) implementation in this language (without a virtual memory layer).