为何编写正确软件如此困难

Why Writing Correct Software Is Hard

23 Jul 2016

… and why math (alone) won’t help us

I was very happy to speak at Curry On once again. Last year, following our work with Quasar, I spoke on continuations vs. monads. This year I gave a talk about computational complexity results in software verification, a subject I became interested in while formally specifying and verifying our upcoming revamped version of Galaxy.

What follows is an extended version of the talk (embedded above), containing some additional proofs and results I didn’t have time to cover, complete with footnotes, for those wishing to study the topics further. Reading time: ~45 mins.

In this article, we try to understand the relationship between programs and correctness, and in particular, why writing correct programs is hard. We will review results from computability theory and complexity theory, and see that programs and complete understanding – which is required for correctness – are fundamentally at odds. The main contribution of this text is aggregating in one place some results (as well as some references) pertaining to the essential difficulty of producing correct software. My motivation was various statements I found online (such as this, although it is far from the only one) claiming that software correctness is easy to achieve with the right tools. While some tools may (and do) certainly assist ensuring programs are correct, correctness comes at a significant cost. The cost of correctness – like the energy cost of reducing entropy – is a result of the “natural laws” of computation, that cannot possibly be avoided.

CHAPTER I: FOUNDATIONS

The story of theoretical CS began about a hundred years ago. With the growing success of mathematical logic, the mathematician David Hilbert laid out a program to formalize all of mathematics. He wanted to prove the formalism consistent and complete, and to find a decision procedure, an algorithm for determining the truth of every formal statement:

· Consistency: proof that no contradiction can be obtained in the formalism.

· Completeness: all true mathematical statements can be proved in the formalism.

· Decidability: an algorithm deciding whether any statement is a theorem (Entscheidungsproblem)

Hilbert believed that anything that can be formally reasoned can also be fully understood, and by that I mean all of its properties proven. the 19th century view on the limits of knowledge was expressed by the maxim “ignoramus et ignorabimus”, meaning “we do not know and we will not know”. For his retirement in 1930, Hilbert gave a lecture – “Naturerkennen und Logik” (Logic and the understanding of nature) – in Königsberg to the Society of German Scientists and Physicians which he challenged this view. He said:

For the mathematician there is no Ignorabimus, and, in my opinion, not at all for natural science either. … The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is no unsolvable problem. In contrast to the foolish Ignorabimus, our credo avers: We must know, we shall know!1

Those words – Wir müssen wissen. Wir werden wissen – are inscribed on his tombstone.

Unbeknownst to Hilbert at the time, his program had been demolished a day earlier, when Kurt Gödel tentatively announced his first incompleteness result2.

Gödel’s incompleteness theorems demolished the first two pillars of Hilbert’s program (some say also the third, only he didn’t realize it3), and in 1936, Church and Turing broke the third, that of the decision problem, with proofs of what is today known as the halting theorem.

The halting theorem – CS’s first theorem – was proven in both Alonzo Church’s4 and Alan Turing’s5 papers in 1936. The theorem is so fundamental to the essence of computation that it is no accident that it appeared alongside both formulations of computation. It states that there cannot exist an algorithm that decides whether any given program ever terminates. The proof (which is given here in a shortened form) is based on the idea of diagonalization, or self reference, the same idea Gödel had used in his incompleteness proof.

Assume such a program H exists:

H(M, x) := IF M halts on x THEN TRUE ELSE FALSE

we can then easily construct $G$:

G(y) := IF H(y, y) = FALSE THEN TRUE ELSE loop forever

If we then pass $G$ to itself ($G(G)$) we get a contradiction between what $G$ does and what $H$ says that $G$ does.

It is interesting to note that the halting theorem immediately yields a version of Gödel’s first incompleteness theorem. The proof says simply6: suppose that for every true statement there was a logical proof in some logical theory (basically a set of axioms). So, given a program, starting from those axioms, we can enumerate all theorems one by one by using logical deduction. Because the number of all statements, let alone all theorems, is countable, and because every statement either has a proof or its negation does, we would eventually find the proof of one or the other. Therefore, given a program, we can start enumerating all theorems until we find a theorem showing that the program terminates, or one that says it doesn’t, thus violating the halting theorem.

However, the halting theorem has some other immediate corollaries that tie it more directly to the problem of software verification, which is our main focus. The first is the simple result about reachability.

There does not exist a program R, when given a program M, a set of initial states I and state configuration S, determines whether or not M ever reaches S when it starts in one of the states in I.

The proof is a simple reduction from halting: if there were an such an algorithm, we could ask it if, starting with the input x it ever reaches the halting state, and so solve the halting problem7.

A more interesting corollary is Rice’s Theorem. Programs can compute what’s known as partial functions. If they stop when given an input, we consider the output written on the tape to be mapped to the initial input; if they never stop for a given input, we consider that input unmapped. Rice’s theorem states this:

For any non-trivial property of partial functions, no algorithm can decide whether or not a program (TM) M computes a partial function with that property.

For example, there is no algorithm to determine whether the output of a program is always the square of its input. This theorem is also proven by a reduction from Halting.

For our purposes, I think that the most interesting corollary of the halting theorem is what we’ll call the “Busy Beaver theorem”8, because it captures best the notion of the complexity of analyzing programs, giving it some quantitative measure. Like all results we have and will cover here, this one applies to both dynamic and static views of programs (namely, their behavior as they run or their global properties), but this one targets each view separately, and so it helps give a more direct intuition that they are two sides of the same coin.

In the dynamic version, we define the following function on the natural numbers:

$f(n)$ = the maximum number of steps a halting TM with $n$ control states may take before halting

A Turing machine’s control states constitute its program, so $n$ is the size of the program. This function is well defined because there is a finite number of TMs of size $n$. The subset of them that terminates is also finite, so there exists a maximal number of states.

The theorem says $f$ is non-computable. Suppose that $f$ were computable. If so, that would be a violation of the halting theorem. Given a TM, we count the number of control states, $n$, compute $f(n)$ (which is possible by our assumption of $f$’s computability), and then run the machine for $f(n)$ steps. If it doesn’t terminate by then — then it must surely never terminate (by the definition of $f$), and we have a decidable procedure of the halting problem, in contradiction with the halting theorem.

Not only is $f$ a non