<p>You certainly <em>can</em> 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). </p>

<p>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</p>

<pre><code>while P do 
   C
</code></pre>

<p>into for-loops with a big iteration constant:</p>

<pre><code>for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break
</code></pre>

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

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

CC BY-SA 3.0
2011-09-28T17:28:14.327Z
What do you mean by "this program is not even primitive recursive"?
Ryan Williams
CC BY-SA 3.0
2011-09-28T18:59:33.490Z
@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.
cody
CC BY-SA 3.0
2011-09-29T05:19:10.897Z
You can macro-expand away the loops, leaving you with a branching program (ie, with only if-then-else and sequential composition).
Neel Krishnaswami
CC BY-SA 3.0
2011-09-29T08:27:39.803Z
Perhaps it would be clearer to say something like "this program does not even need the full strength of primitive recursion".
Max
CC BY-SA 3.0
2011-09-29T09:03:58.030Z
@Max: suggestion accepted!
Neel Krishnaswami
CC BY-SA 3.0
2011-09-28T12:10:52.577Z
2011-09-29T09:03:44.537Z
2011-09-29T09:03:44.537Z
Neel Krishnaswami
<p>Since you asked about program correctness of real world programs like operating systems, you might be interested in the seL4 project (<a href="http://dl.acm.org/citation.cfm?id=1743574">journal</a>, <a href="http://galaxy.lamar.edu/~sandrei/CPSC-4360-01/ListOfPapers/p107-klein.pdf">pdf</a>,  <a href="http://dl.acm.org/citation.cfm?id=1629596">conference</a>). </p>

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

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

CC BY-SA 3.0
2011-11-28T16:05:14.803Z
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.
nponeccop
CC BY-SA 3.0
2011-11-28T17:01:16.757Z
@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).
Artem Kaznatcheev
CC BY-SA 3.0
2011-11-28T23:53:19.040Z
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.
nponeccop
CC BY-SA 3.0
2011-11-29T00:13:36.517Z
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.'
nponeccop
CC BY-SA 3.0
2011-09-28T17:04:49.327Z
2011-09-28T17:04:49.327Z
Artem Kaznatcheev
<p>The questions you ask are actually quite different.</p>

<blockquote>
  <p>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? </p>
</blockquote>

<p>It takes extremely little for a model of computation to be Turing complete. For example, various <a href="http://en.wikipedia.org/wiki/Counter_machine" rel="nofollow">models with counters</a> 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.</p>

<blockquote>
  <p>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?</p>
</blockquote>

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

<p>In particular, you can modify your original question to</p>

<blockquote>
  <p><em>Is there an abstraction of my software that I can analyse efficiently in a non-Turing complete model?</em></p>
</blockquote>

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

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

CC BY-SA 3.0
2011-09-29T13:38:22.230Z
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.
David Harris
CC BY-SA 3.0
2011-09-29T21:36:56.030Z
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.
Vijay D
CC BY-SA 3.0
2011-09-30T05:48:22.030Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2011-09-30T21:07:17.653Z
@Neel: To clarify, I am only talking about Turing completeness. Is it not possible to simulate a Turing machine in these theories?
Vijay D
CC BY-SA 3.0
2011-10-02T14:05:56.090Z
That's right-- they are not Turing complete. In constructive logic, Turing-completeness permits an analogue of Russell's paradox to be programmed.
Neel Krishnaswami
CC BY-SA 3.0
2011-09-29T03:15:50.550Z
2011-09-29T03:15:50.550Z
Vijay D
<p>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. </p>

<p>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?</p>

CC BY-SA 3.0
2011-09-28T11:46:18.070Z
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).
Kaveh
CC BY-SA 3.0
2011-09-28T16:41:59.690Z
mildly related [question](http://cstheory.stackexchange.com/q/5120/1037)
Artem Kaznatcheev
<computability>
Computational hardness of "real" computer programs
David Harris
# Computational hardness of "real" computer programs

(Asked by: username_0 on 2011-09-28)

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?

**Tags:** computability
> **Comments:**
> **username_1**: 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).  
> **username_2**: mildly related [question](http://cstheory.stackexchange.com/q/5120/1037)  

---

## 3 answers

### Answer by username_3 on 2011-09-28. Score: 14

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.

> **Comments:**
> **username_4**: What do you mean by "this program is not even primitive recursive"?  
> **username_5**: @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.  
> **username_3**: You can macro-expand away the loops, leaving you with a branching program (ie, with only if-then-else and sequential composition).  
> **username_6**: Perhaps it would be clearer to say something like "this program does not even need the full strength of primitive recursion".  
> **username_3**: @Max: suggestion accepted!  

---

### Answer by username_2 on 2011-09-28. Score: 5

Since you asked about program correctness of real world programs like operating systems, you might be interested in the seL4 project ([journal](http://dl.acm.org/citation.cfm?id=1743574), [pdf](http://galaxy.lamar.edu/~sandrei/CPSC-4360-01/ListOfPapers/p107-klein.pdf), [conference](http://dl.acm.org/citation.cfm?id=1629596)).

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.

> **Comments:**
> **username_7**: 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.  
> **username_2**: @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).  
> **username_7**: 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.  
> **username_7**: 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.'  

---

### Answer by username_8 on 2011-09-29. Score: 2

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](http://en.wikipedia.org/wiki/Counter_machine) 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.

> **Comments:**
> **username_0**: 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.  
> **username_8**: 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.  
> **username_3**: @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.  
> **username_8**: @Neel: To clarify, I am only talking about Turing completeness. Is it not possible to simulate a Turing machine in these theories?  
> **username_3**: That's right-- they are not Turing complete. In constructive logic, Turing-completeness permits an analogue of Russell's paradox to be programmed.  

---

