somebody needs to introduce a touch screen and some LCD displays to these people.
That's not possible. It is not possible to prove a nontrivial program to be fail-safe, any more than it is possible to prove a nontrivial axiomatic system to be internally consistent -- and for the same reason: Gödel's Incompleteness Theorems.
The Turing Halting Problem, and Gödel's Incompleteness Theorems, are deeply connected. The second cannot be resolved because the first cannot be resolved.
http://en.wikipedia.org/wiki/G%C3%B6dels_incompleteness_theo...
A quote: "The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency." (Emphasis added.)
http://en.wikipedia.org/wiki/Halting_problem
A quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. A key part of the proof was a mathematical definition of a computer and program, what became known as a Turing machine; the halting problem is undecidable over Turing machines." (Emphasis added.)
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).
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.