A little while ago, I went back to my old university’s website and flipped through the course catalog. It brought back memories. I learned a lot of interesting things when I was in school but in hindsight one of the most striking things about the experience was the mathematical focus of my coursework. I had courses in programming and software engineering, but I also spent a lot of time learning about abstract machines and languages, how to prove and disprove assertions about the complexity of algorithms, and all sorts of other things that really seem much more akin to mathematics than design. I remember one professor who felt strongly that we would soon have smart tools that would help us prove the correctness of our programs. It’s an old idea, and a very seductive one. If we could easily prove the correctness of our programs, wouldn’t that completely change the industry? We could have fewer bugs, fewer security problems and easier development overall?

This meme, program verification, has been around for a long time, but it isn’t as popular as it used to be. Superficially, the desire to prove programs correct sounds wonderful, until you realize that correctness means “matches specification.” How do we create a specification which is complete, concise, and unambiguous? It sounds suspiciously like writing a program in the first place. And, even if we were able to do that well, we’d have to hope that we are able to do it quickly. Every time we change a “correct” program, we’d have to re-prove its correctness, wouldn't we?

A few weeks ago, I went to the OOPSLA conference and I saw a demo by a company named Ergnosis. They are in the process of developing an IDE that really knows its language intimately. If you bring up a piece of a program and select it you get a menu of a large number of changes that you can make without altering the behavior of the program at all. Some are things I’ve been wanting for years. For instance, you can select a statement and drag it after a subsequent statement or take an expression that is in the argument list of a method and push it into the method. These actions are only allowed if they preserve behavior.

Interestingly, one of the things that their tool doesn’t do yet is allow users to manually edit the code. I’m sure they’ll have that feature eventually, but the fact that they have put off adding it for so long is pretty tantalizing. It is like a question that hangs in the air for people who notice it. How much of our editing has to be risky? Can tools get us to the point where we can assume that most of our editing doesn’t change behavior but only a small subset of it does? If we can’t easily prove correctness, couldn’t we get a leg up if we tackled the derivative: if we could be certain of the correctness of most of our changes? If we could work like that, we could add tested features into a system very directly and use a wide palette of safe automated moves to make the code more easily understandable.

Regardless of the amount of tool support that we achieve, programming is a human activity and we will make mistakes. However, it is great to see some emphasis on this other point of view: that demonstrating that we’ve preserved behavior matters. I think it would be great if more of the energy that has gone into program verification could go into change verification. To me, it just seems to be the more important thing right now.