Understanding Computation

Chapter 9. Programming in Toyland

Programming is about using syntax to communicate ideas to a machine. When we write a program, we have an idea of what we want the machine to do when it executes that program, and knowing the semantics of our programming language gives us some confidence that the machine is going to understand what each small piece of the program means.

But a complex computer program is greater than the sum of its individual statements and expressions. Once we’ve plugged together many small parts to make a larger whole, it would be useful to be able to check whether the overall program actually does what we originally wanted it to do. We might want to know that it always returns certain results, for example, or that running it will have certain side effects on the filesystem or network, or just that it doesn’t contain obvious bugs that will make it crash on unexpected inputs.

In fact, there are all sorts of properties that we might want our programs to have, and it would be really convenient if we could just check the syntax of a particular program to see whether or not it has those properties, but we know from Rice’s theorem that predicting a program’s behavior by looking at its source code can’t always give us the right answer. Of course, the most direct way to find out what a program will do is just to run it, and sometimes that’s okay—a lot of software testing is done by running programs on known inputs and checking the actual outputs against the expected ones—but ...