[tarre]

In nuclear power plants you just don't walk in and install new equipment. When upgrading control room to digital, you pretty much also need to upgrade the automation of the plant to be digital and qualifying it to be used in NPP is a real nightmare. In mainstream software markets you can always release bugfixes and add new features afterwards. In NPP your system must work the right way in every possible situation right from the start. I don't think, there are many software companies writing fail-safe programs of that size. And what's even more difficult, you have to prove it to be fail-safe to the regulators.

[lutusp]

> I don't think, there are many software companies writing fail-safe programs of that size. And what's even more difficult, you have to prove it to be fail-safe to the regulators.

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.)

[kpreid]

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).

[lutusp]

> 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.

[andreasvc]

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).

[andreasvc]

The grandparent obviously meant "prove" in an informal sense, as in getting something accepted by some bureaucratic certification. You're talking about formal, mechanized proof systems.