Sunday, January 6, 2008

Methods Of Proof

Over the past couple of weeks or so, I've been playing with some recreational math. It was pointed out to me that the sum of the first n cubes always seemed to be a square. For example, 1^3 + 2^3 + 3^3 = 36 = 6^2. This is probably obvious to the highly numerate, but it blew my mind to learn it. After struggling a bit, I could show that the sum of the first n cubes is always the square of the sum of the first n integers. Wow!

I came up with a couple of different proofs that were full of tedious algebra, and didn't seem to offer any insights into why such a relation should hold. I became convinced that something so easy to state should have a brief demonstration, possibly geometric, and definitely more intuitive. For quite a while, I couldn't find such a thing.

Then it hit me. Induction! There are so many methods of proof: reductio ad absurdam, proof by construction, even proof by computer. Once I remembered the technique, I quickly banged out a proof by induction that the sum of the first n cubes is the square of the sum of the first n integers in just a handful of lines.

Mathematical proofs to me are a lot like tests in software development. Just as there are varied methods of proof, there are varied mechanisms for testing the deliverables in the software development process. For example, I might test that the requirements are met with formal acceptance testing. In other words, the acceptance test proves the functional spec (or some other document).

As another example, someone might say that the unit tests prove the code. As a fan of test driven development, I would say exactly the reverse. But the point is that different testing mechanisms are suitable for different parts of the development process. Just as a mathematician must be well versed in different methods of proof, we software folks must be well versed in different testing mechanisms.

But what tests the design?

Sure, a formal inspection can uncover lots of problems in a document, but is that really sufficient to demonstrate that a design is any good? Multithreading issues, resource leaks, inadequate error handling, and bottlenecks are difficult to uncover in a review, except in the most obvious cases. Formal review chauvinists are sure to challenge me on that opinion. But I believe that if humans really could anticipate how complex systems behaved, then there wouldn't be any such phrase as emergent behavior.

So, I feel that we need another "method of proof" suitable for evaluating design fitness. Ideally, it would be inexpensive and repeatable, giving it another leg up on formal inspections. It should also be available as early in the development process as possible. I suggest that designs are testable by simulation.

The project I've been working on most recently has lots of algorithms with tunable parameters, and one of the open questions is how much hardware firepower do we really need to handle realistic customer loads. Although I can imagine that somebody much smarter than I could figure this out from first principles, I wouldn't have much confidence in any design that wasn't vetted by simulations.

Happily, with simulation, we don't have to be done before we find out that our design is broken. With languages like Ruby, we can develop margin eaters and simulators rapidly. Design trouble spots can be identified early, maybe even before any production code is written. Of course, this is only possible if the architecture is amenable to simulation.

One figure of merit for a good architecture is how early it can support simulations. For example, a recent effort I've shepherded used text over sockets for interprocess communication. There were a lot of fans of Java Object Serialization, but that would have required Java on both sides of the connection. Sticking with text over sockets allowed rapid development of Ruby simulators and placeholders.

Testing designs by simulation is not an earth-shattering suggestion. Mature software companies have been using simulation forever, replacing margin eaters with production code as development proceeds. But as an architect, I have profited from the notion that simulation is a kind of test, a method of proof, for designs themselves.