Review of "The Science of Programming"

The Science of Programming, by David Gries. ISBN 0-38796-480-0.

This is a book on programming from an austerely mathematical viewpoint, much in the spirit of Dijkstra. Gries proposes that every program should be developed in conjunction with a proof of its correctness, with the proof frequently leading the way.

This is an old book: 25 years old now. Its age shows in several ways: programming languages have come a long way since 1981, and so have their libraries, and so have the tasks we expect computers to perform. The book feels very, very dated.

That doesn't mean that there's nothing of value here. If you think design by contract originated with Bertrand Meyer, think again: the key ideas are here. (In fact, they antedate this book by some way.) If you think "test-driven development" is new, think again ... well, at least a little. One of the underappreciated things that makes TDD tick is that it makes you keep track of what you know about your code and what you don't; the idea of "proof-driven development" found in this book resembles it at least to that extent.

Gries concentrates on small programs that do one clearly specifiable thing: sum all the numbers in an array, traverse a binary tree, enumerate the permutations of a given list of numbers. These days, we'd hardly consider such a thing a "program". Even in 1981, they were toy problems. "Every large program consists of many small programs", says Gries, and I suppose that's true, but the problems of writing correct large programs are often quite different in kind from those of writing correct tiny ones.

The book could have used a little more discipline in editing. There is an entirely unnecessary (though interesting enough, for those who are interested in such things) chapter on "natural deduction", and an equally unnecessary one on "inverting programs", by which Gries means taking a program that computes an invertible function of one variable and transforming it into one that computes the inverse function.

Everyone who writes software would benefit from some exposure to the sort of thinking found in this book. It's not clear to me that it's practical to write non-toy software this way; perhaps I've been corrupted by my time spent among engineers. I think it would be very interesting to see something along similar lines for modern-day programming; superficially it would probably look very different from Gries's book, but a lot of the underlying ideas would remain the same. (Maybe such a book already exists?)

Nothing could make a book like this easy going, but Gries does a pretty good job. It's concisely but clearly written; the text is thankfully less formal than the code and the proofs.