10
$\begingroup$

I have often heard it said that you cannot write a program to catch bugs in a web browser, or word-processor, or operating system, because of Rice's Theorem: any semantical property for a Turing-complete language is undecidable.

However, I am not sure to what extent this applies to real-world program likes operating systems. Do these types of programs need the full strength of Turing completeness? Are there simpler models of computation (such as PR) in which these applications could be written? If so, to what extent does this allow decidability of program correctness?

|cite|improve this question
$\endgroup$
  • $\begingroup$ you cannot check non-trivial universal properties (e.g. something holds for all inputs) of much weaker models, e.g. you cannot check if two polytime computable TMs are computing the same function (although halting is decidable for them because a polytime TM always halts). On the other hand, if the domain of inputs is bounded you can check some properties in some models, e.g. the program doesn't crash on inputs of size less than 1,000, at least in theory (in practice it might be intractable). $\endgroup$ – Kaveh Sep 28 '11 at 11:46
  • $\begingroup$ mildly related question $\endgroup$ – Artem Kaznatcheev♦ Sep 28 '11 at 16:41
14
$\begingroup$

You certainly can write programs which catch bugs -- there is a large and active community of people who write programs to do exactly that. However, what Rice's theorem prevents you from doing is to write bug-catchers which are both sound and complete (i.e., catch all bugs of a certain class with no false positives).

That said, naive restrictions on the model of computation don't actually help you very much in improving the practicality of program analysis. The reason is that you can get programs which do "almost the same thing" by turning while loops

while P do 
   C

into for-loops with a big iteration constant:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Now this program does not even need the full strength of primitive recursive (since the for-loop can be macro-expanded into a huge nested if-then-else statement), but in most practical cases it will behave just the same as before. Note that it does help decidability in theory -- the program is total, so you can answer questions by running the program and seeing what happens. This is not what we actually want, which is to get answers faster than running the program -- the artificial termination introduced doesn't actually help program analysis in practice, since bugs occur because of errors in the real program logic, and we haven't touched that at all.

Furthermore, adding abstraction facilities to a programming language can radically worsen the complexity of the analysis problem, while making it easier to verify programs in practice. For example, proving termination of the simply-typed lambda calculus with natural numbers requires induction up to $\epsilon_0$, but by adding type polymorphism you get System F, whose termination proof as strong as the consistency of second-order arithmetic. Yet, in practice programs written in F are much easier to verify, because the modularity properties of second-order quantification make writing structured programs and correctness proofs much easier.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ What do you mean by "this program is not even primitive recursive"? $\endgroup$ – Ryan Williams Sep 28 '11 at 17:28
  • $\begingroup$ @RyanWilliams probably just that it can be written in a system which allows less than the full array of primitive recursive functions, for example programs that need explicit (compile time) bounds on the loops. $\endgroup$ – cody Sep 28 '11 at 18:59
  • $\begingroup$ You can macro-expand away the loops, leaving you with a branching program (ie, with only if-then-else and sequential composition). $\endgroup$ – Neel Krishnaswami Sep 29 '11 at 5:19
  • $\begingroup$ Perhaps it would be clearer to say something like "this program does not even need the full strength of primitive recursion". $\endgroup$ – Max Sep 29 '11 at 8:27
  • $\begingroup$ @Max: suggestion accepted! $\endgroup$ – Neel Krishnaswami Sep 29 '11 at 9:03
5
$\begingroup$

Since you asked about program correctness of real world programs like operating systems, you might be interested in the seL4 project (journal, pdf, conference).

The NICTA team took a third-generation microkernel of 8700 lines of C and 600 lines of assembler implemented according to an abstract specification in Haskell. They provided a formal, machine-checked proof (in Isabelle/HOL) that the implementation strictly follows the specification. Thus proving that their program is bug-free.

So just like the halting problem, although it can't be solved in general, it can be solved for some specific instances. In this case, although you can't prove that arbitrary C code is bug free, they could do it in the case of the seL4 microkernel.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Note that certified code is still vulnerable to mistakes in its specification, so you can only say that the code is bug free relatively to the specification. $\endgroup$ – nponeccop Nov 28 '11 at 16:05
  • $\begingroup$ @nponeccop definitely true, but when you start to doubt the specification you also start to really blur the infamous bug-feature line. To call something a 'bug' you must have some implicit specification in mind, capturing the intuition behind such an implicit specification starts to dig really deep until you hit questions at the foundations in philosophy of math (in the style of Brouwer vs. Hilbert). $\endgroup$ – Artem Kaznatcheev♦ Nov 28 '11 at 17:01
  • $\begingroup$ By 'specification' I meant the formal specification i.e. the formal theorems you prove. You may still make mistakes in turning your textual requirements into theorems. The only things you get with certification are reduction of your trusted codebase (you should only trust your theorems and not your code or proofs) and consistency of your code with your theorems. $\endgroup$ – nponeccop Nov 28 '11 at 23:53
  • $\begingroup$ Here is a quote from seL4 website: 'The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.' $\endgroup$ – nponeccop Nov 29 '11 at 0:13
2
$\begingroup$

The questions you ask are actually quite different.

However, I am not sure to what extent this applies to real-world program likes operating systems. Do these types of programs need the full strength of Turing completeness?

It takes extremely little for a model of computation to be Turing complete. For example, various models with counters can simulate Turing machines. If you believe your software requires more than two counters that you can manipulate arbitrarily, you are using a Turing complete language. Though machine integers are apriori bounded, heap-allocated data structures usually are not. If your software needs lists, trees, and other dynamically allocated data, you are using a Turing complete language.

Are there simpler models of computation (such as PR) in which these applications could be written? If so, to what extent does this allow decidability of program correctness?

It is important to recognise that we do not want to check arbitrary properties of our software. Checking very specific, narrow properties (no buffer overflows, no null-pointer dereferences, no infinite loops, etc.) immensely improves the quality and usability of software. In theory, such problems are still undecidable. In practice, focusing on specific properties allows us to discover structure in our programs that we can often exploit to solve the problem.

In particular, you can modify your original question to

Is there an abstraction of my software that I can analyse efficiently in a non-Turing complete model?

An abstraction is a model that includes the behaviour of the original software and possibly many additional behaviours. There are models such as one-counter machines or pushdown systems that are not Turing complete and that we can analyse. The standard approach in program verification with automated tools is to construct an abstraction in such a model and check it algorithmically.

There are applications where people care about sophisticated properties of their hardware or software. Hardware companies want their chips to correctly implement arithmetic algorithms, automotive and avionic companies want certifiably correct software. If it's that important, you are better of using a (trained) human being.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ I think you have answered the opposite question, namely is it possible for a word-processor to be Turing complete? With appropriate handling of registers, it is. Nevertheless, it is possible to impose rules of register manipulation to defeat Turing completeness. My question is how much you can program practically in these narrow constraints. $\endgroup$ – David Harris Sep 29 '11 at 13:38
  • $\begingroup$ I was answering the question about whether writing operating systems and other application software requires a Turing complete programming language. If you need multiple counters or unbounded data structures, you will require a Turing complete programming language. $\endgroup$ – Vijay D Sep 29 '11 at 21:36
  • $\begingroup$ @Vijay: no, this isn't true. There are plenty of type theories (e.g., Agda and Coq) which are both extremely expressive and do not permit unbounded recursion. $\endgroup$ – Neel Krishnaswami Sep 30 '11 at 5:48
  • $\begingroup$ @Neel: To clarify, I am only talking about Turing completeness. Is it not possible to simulate a Turing machine in these theories? $\endgroup$ – Vijay D Sep 30 '11 at 21:07
  • $\begingroup$ That's right-- they are not Turing complete. In constructive logic, Turing-completeness permits an analogue of Russell's paradox to be programmed. $\endgroup$ – Neel Krishnaswami Oct 2 '11 at 14:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.