What do we know about provably correct programs?

Question

The ever increasing complexity of computer programs and the increasingly crucial position computers have in our society leaves me wondering why we still don't collectively use programming languages in which you have to give a formal proof that your code works correctly.

I believe the term is a 'certifying compiler' (I found it here): a compiler compiling a programming language in which one not only has to write the code, but also state the specification of the code and prove that the code adheres to the specification (or use an automated prover to do so).

While searching the internet, I only found projects that either use a very simple programming language or failed projects that try to adapt modern programming languages. This leads me to my question:

Are there any certifying compilers implementing a full-blown programming language, or is this very hard/theoretically impossible?

Additionally, I've yet to see any complexity class involving provable programs, such as 'the class of all languages decidable by a Turing machine for which a proof exists that this Turing machine halts', which I shall call $ProvableR$, as an analogue to $R$, the set of recursive languages.

I can see advantages of studying such a complexity class: for instance, for $ProvableR$ the Halting problem is decidable (I even conjecture $ProvableRE$ defined in the obvious way would be the largest class of languages for which it is decidable). In addition, I doubt we would rule out any practically useful programs: who would use a program when you can't prove it terminates?

So my second question is:

What do we know about complexity classes which require their containing languages to provably have certain properties?

Answer 1

"Certifying compiler" usually means something slightly different: it means that you have a compiler which can prove that the machine code it emits correctly implements the high-level semantics. That is, this is a proof that there are no compiler bugs. The programs that people give to the compiler can still be wrong, but the compiler will generate a correct machine code version of the wrong program. The biggest success story along these lines is the CompCert verified compiler, which is a compiler for a large subset of C.

The Compcert compiler itself is a program with a correctness proof (done in Coq), which guarantees that if it generates code for a program, it will be correct (with respect to the operational semantics of assembly & C that the CompCert designers used). The effort to machine-check these things is quite large; typically the correctness proof will be anywhere from 1x to 100x the size of the program you are verifying. Writing machine-checked programs and proofs is a new skill you have to learn -- it's not mathematics or programming as usual, though it depends on being able to do both well. It feels like you are starting from scratch, like being a novice programmer again.

There are no special theoretical barriers to this, though. The only thing along these lines is the Blum Size theorem that for any language in which all programs are total, you can find a program in a general recursive language which will be at least exponentially larger when programmed in the total language. The way to understand this result is that a total language encodes not just a program, but also a termination proof. So you can have short programs with long termination proofs. However, this doesn't really matter in practice, since we're only going to ever write programs with manageable termination proofs.

EDIT: Dai Le asked for some elaboration of the last point.

This is mostly a pragmatic claim, based on the fact that if you can understand why a program works, then it's unlikely that the reason is some vast invariant millions of pages long. (The longest invariants I've used are a few pages long, and boy do they make the reviewers grumble! Understandably so, too, since the invariant is the reason the program works stripped of all the narrative that helps people understand it.)

But there are also some theoretical reasons, as well. Basically, we don't know very many ways to systematically invent programs whose correctness proofs are very long. The main method is to (1) take the logic in which you prove correctness, (2) find a property which can't be directly expressed in that logic (consistency proofs are the typical source), and (3) find a program whose correctness proof relies on a family of expressible consequences of the inexpressible property. Because (2) is inexpressible, this means that the proof of each expressible consequence must be done independently, which lets you blow up the size of the correctness proof. As a simple example, note that in first-order logic with a parent relation, you can't express the ancestor relation. But $k$-ancestry (ancestry of depth $k$) is expressible, for each fixed $k$. So by giving a program that uses some property of ancestry up to some depth (say, 100), you can force a correctness proof in FOL to contain proofs of those properties a hundred times over.

The sophisticated take on this subject is called "reverse mathematics", and is the study of which axioms are required to prove given theorems. I don't know that much about it, but if you post a question on its application to CS, and I'm sure at least Timothy Chow, and probably several other people, will be able to tell you interesting things.

Answer 2

I think the answer to the first question is that generally it is too much work with current tools. To get the feeling, I suggest trying to prove the correctness of Bubble Sort in Coq (or if you prefer a little more challenge, use Quick Sort). I don't think it is reasonable to expect programmers write verified programs as long as proving correctness of such basic algorithms is so difficult and time consuming.

This question is similar to asking why mathematicians don't write formal proofs verifiable by proof checkers? Writing a program with a formal correctness proof means proving a mathematical theorem about the written code, and the answer to that question also applies to your question.

This does not mean that there has not been successful cases of verified programs. I know that there are groups who are proving the correctness of systems like Microsoft's hypervisor. A related case is Microsoft's Verified C Compiler. But in general the current tools need a lot of development (including their SE and HCI aspects) before becoming useful for general programmers (and mathematicians).

Regarding the final paragraph of Neel's answer about program size growth for languages with only total functions, actually it is easy to prove even more (If I understood it correctly). It is reasonable to expect that the syntax of any programing language will be c.e. and the set of total computable functions is not c.e., so for any programming language where all programs are total there is a total computable function which cannot be computed by any program (of any size) in that language.

---

For the second question, I answered a similar question on Scott's blog sometime ago. Basically if the complexity class has a nice characterization and is computably representable (i.e. it is c.e.) then we can prove that some representation of the problems in the complexity class are provably total in a very weak theories corresponding to the complexity class. The basic idea is that the provably total functions of the theory contains all $AC^0$ functions and a problem which is $AC^0$-complete for the complexity class, therefore it contains all problems in the complexity class and can prove the totality of those programs. The relation between proofs and complexity theory is studied in proof complexity, see S.A. Cook and P. Nguyen's recent book "Logical Foundations of Proof Complexity" if you are interested. (A draft from 2008 is available.) So the basic answer is that for many classes "Provably C = C".

This is not true in general since there are semantic complexity classes which do not have syntactic characterization, e.g. total computable functions. If by recursive you mean total recursive functions then the two are not equal, and the set of computable functions which are provably total in a theory is well studied in proof theory literature and are called the provably total functions of the theory. For example: the provably total functions of $PA$ are $\epsilon_0$-recursive functions (or equivalently functions in Godel's system $T$), the provably total functions of $PA^2$ are function in Girard's system $F$, the provably total functions of $I\Sigma_1$ are primitive recursive functions, ... .

But it does not seem to me that this means much in program verification context, since there are also programs which are extensionally computing the same function but we cannot prove that the two programs are computing the same function, i.e. the programs are extensionally equal but not intentionally. (This is similar to the Morning Star and the Evening Star.) Moreover it is easy to modify a given provably total program to get one which the theory is unable to prove its totality.

---

I think the two questions are related. The objective is to get a verified program. A verified programs means that the program satisfies a description, which is a mathematical statement. One way is to write a program in a programming language and then prove its properties like it satisfies the description, which is the more common practice. Another option is to try to prove the mathematical statement describing the problem using restricted means and then extract a verified program from it. For example, if we prove in the theory corresponding to $P$ that for any given number $n$ there is a sequence of prime numbers which their product is equal to $n$, then we can extract a $P$ algorithm for factorization from the proof. (There are also researcher who try to automatize the first approach as much as possible, but checking interesting non-trivial properties of programs is computationally difficult and cannot be completely verified without false positives and negatives.)

Answer 3

What you are asking about in the first question is sometimes called a "verifying compiler", and a few years ago Tony Hoare offered it as a grand challenge for computing research. To some extent this already exists and is in active use in tools such as the Coq theorem prover, which organize the problem by way of type theory and the propositions-as-types principle ("Curry-Howard").

EDIT: just wanted to add emphasis on "to some extent". This is far from a solved problem, but the success of Coq gives hope that it is not a pipe dream.

Answer 4

A tool that checks whether a program is correct is sometimes called a program verifier. In this context, "correct" usually means two things: that the program never produces certain outputs (think segmentation fault, NullPointerException, etc.) and that the program agrees with a specification.

The code and the specification may agree and still be perceived as wrong. In a sense, asking developers to write specifications is like asking two developers to solve the problem. If the two implementations agree then you have higher confidence that they are OK. In another sense, however, specifications are better than a second implementation. Because the specification needs not be efficient or even executable, it can be much more succinct and hence harder to get wrong.

With these caveats in mind, I recommend you look at the Spec# program verifier.

Answer 5

Chapter 6 of the following classic monograph studies almost exactly your second question:

Hartmanis, J. Feasible computations and provable complexity properties, CBMS-NSF Regional Conference Series in Applied Mathematics, 30. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, Pa., 1978.

For example, he defines the class "F-TIME[T(n)]" (where F is some reasonable formal proof system) to be $\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$ (where $M_i$ is the i-th Turing machine in a complete list of TMs, and $T_i(n)$ is the maximum running time of $M_i$ on inputs of length $n$). Let me just highlight a few results relevant to your question - many more can be found in the monograph and references therein:

Cor. 6.4: Let $T(n) \geq n \log(n)$ be a computable function, and let $g(n) \geq 1$ be an unbounded computable function. Then $F$-$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$.

Theorem 6.5: There exist computable monotonically increasing time bounds $T(n)$ for which $F$-$TIME[T(n)] \neq TIME[T(n)]$.

Theorem 6.14: For any computable $T(n) \geq n \log(n)$, $TIME[T(n)] = \{ L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)] \}$.

For space, however, the situation is better controlled:

Theorem 6.9: (1) If $s(n) \geq n$ is space-constructible, then $SPACE[s(n)] = F$-$SPACE[s(n)]$.

(2) If $SPACE[S(n)]=F$-$SPACE[S(n)]$ ($S(n) \geq n$) then there is a space-constructible $s(n)$ such that $SPACE[S(n)]=SPACE[s(n)]$.

Answer 6

In the general case, it is impossible to create an algorithm that confirms whether an algorithm is equivalent to a specification. This is an informal proof:

Almost all programming languages are Turing-complete. Therefore, any language decided by a TM can be also be decided by a program written in this language.

The problem of determining whether two TMs accept the same language, known as $Equivalence/TM$ is undecidable. As a consequence of Turing completeness, the same holds for the programs of the given language. In other words, it is undecidable to know whether the inputs you want your program to accept and the inputs it really does are the same.

Furthermore, $Equivalence/TM$ is not even recursive enumerable. That is because $Non-emptiness/TM$ (whether a TM accepts at least one input) is an acceptable language, since you can iterate over all possible inputs. If the TM is non-empty, eventually you will find a word that is accepted. Therefore $Emptiness/TM$ is unacceptable, otherwise $Emptiness/TM$ would be decidable (which we know it is not). However Emptiness/TM can be reduced to $Equivalence/TM$, therefore $Equivalence/TM$ is also unacceptable. Therefore you can use an algorithm whether or not two machines are not equivalent, but you cannot be sure if they are equivalent, or you haven't given your algorithm enough time.

However, this is only for the general case. It is possible that you can decide whether or not the specifications are equivalent to the program, by solving a more relaxed version of the problem. For example, you might examine only a number of inputs or say that the two programs are equivalent with some uncertainty. This is what software testing is all about.

As for the rest of your questions:

Note: This part has been edited for clarification. It turns out that I did the mistake I was trying to avoid, sorry.

Let $TrueR$ be the collection of languages that we know to be decidable. Of course $TrueR \subseteq R$. One can then prove the following:

$ProvableR = TrueR$. It is easy to see that $ProvableR \subset TrueR$. However, it is also $TrueR \subset ProvableR$ . The proof is very easy: Let $A \epsilon TrueR$ . By definition , in every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $A \epsilon ProvableR$ .

Informally , this can be summarized as: You don't know that a language is decidable until you have proven it to be. So if in a formal system you have the knowledge that a language is decidable, this knowledge can also serve as a proof for that. Therefore, you cannot simultaneously have the knowledge that a language is both decidable and it cannot be proven so, these two statements are mutually exclusive.

My final point is that our knowledge is partial and that the only way of studying $R$ is through $ProvableR$. The distinction might make sense in mathematics and we can acknowledge it, but we possess no tools to study it. Since $ProvableR \subset R$ , we are bound to never completely know $R$ in its entirety.

@Kaveh summarizes it best: Provable always means provable in some system/theory and does not coincide with truth in general.

The same holds for any other complexity class: To determine membership you need a proof first. This is why I believe that your second question is too general, since it contains not only complexity theory, but also computation theory as well, depending on the property you want the language to have.

Answer 7

The question has to be posed correctly. For example, nobody ever wants to know whether an actual program would complete given infinite memory and some means of accessing it (maybe an operation to move the base address by some number). Turing's theorem is irrelevant to program correctness in any concrete sense and people who cite it as a barrier to program verification are confusing two quite different things. When engineers/programmers talk of program correctness they want to know about finite properties. This is also pretty much true for mathematicians who are interested in whether something is provable. Godel's letter http://vyodaiken.com/2009/08/28/godels-lost-letter/ explains this in some detail.

Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem.

It may well be infeasible to examine the immense state set of a program executing on an actual computer and detect bad states, there is no theoretical reason why it can't be done. In fact, there has been a lot of progress in this field - for example see http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf (thanks to Neil Immerman for telling me about this)

A different and more difficult problem is specifying exactly what properties one wants a program to have in order to be correct.