All this talk about bug free code is kind of amusing. While I am unhappy about the number and type of bugs found in Civ 3, I do realize that bug free code is usually impossible. There are ways to prove a program mathematically correct, called formal methods I think, but these proofs become exponentially expensive to perform and probably are not practical for game development or any commercial software for that matter.

Exactly correct. Such programs are called verifiers, validators, or model checkers. I’ve written one, and used a couple of others. There are several major problems with the entire genre, including but not limited to the following:

  • As you point out, the state space grows very quickly to the point where the time required for validation exceeds the lifetime of the universe. It happens sooner than you think. State space explosion is the #1 problem in this field, and quite a few brilliant researchers have spent their whole careers trying to address it…sadly, to little practical avail.
  • Successful validation only proves that the program meets the requirements as given to the validator as input, and that input can have its own bugs.
  • Both the algorithm and the requirements must usually be specified in a validator-specific language, which inevitably means that what you’re validating is not the actual running code. The only system I know of that applies serious validation techniques to real code is Dawson Engler’s MC, and that technology is still in its infancy.

I apologize for interjecting a little software-engineering reality into what is obviously a very satisfying (but uninformed) pig-pile, but it just seemed necessary. The perfect is the enemy of the possible, and I’m really big on exploring the possible. Maybe we can get back to something related to games now, instead of pretending to be software-engineeering experts.

My own validator, to which I referred above, is described here.