The True Scope is Unknowable

"Agile" has balkanized, and the individual cults have - in some cases - become religions that are just as bad as the things they intended to replace. But at the outset, the interesting thing about "agile" (the only interesting thing about it, in my opinion) was that it was an attempt to acknowledge this reality, to address it explicitly, to deal with it. That was a good idea. We should keep striving away at it.

Mark Masterson, Process Perfection

Definitions aren’t helping. I'm growing increasingly in favor of the view that agile is as agile does. Rather than burning cycles trying to define a nuanced version of uppercase Agile, I'll just accept it more as a lowercase adjective, a way of doing business and making decisions that doesn't try to hide the fact that such uncertainty exists.

Certainly, the whole static typing and provability meme, as it relates to process management, is a chimera. The reality is that the same problems with management of scope and complexity will also arise on design projects that don't involve any formal software construction.

A good example of a software feature that defies formal verification in this way is an image cropping and resizing tool for a CMS. How would a software engineer go about proving that such a resizer is correct?

To the users, the resizer is a black box. A source image goes in, and a resized and cropped image comes out. Formally proving this program is correct using static analysis isn't going to tell us whether the program works, simply because it's not precisely clear what it means for this program to work in the first place. We could onerously unit test the resizer, but that's not going to be enough either - we can only get as far as verifying that the output images meet the expected width and height dimensions. We can't automatically tell whether the crop is good, whether the resize bulges or contracts the image to make it look stupid. If we did try to test this automatically, the sheer complexity of verifying the resulting images would far outweigh the complexity of the original resizer. There is a combinatorial explosion of possible ways to crop a given image, but only a handful of these results will actually look good.

So this is really a design problem. The program itself is fuzzy, akin to a 'best guess' algorithm. We can't make it work effectively without a human eye to run over the results and make decisions based on intuitive judgment. And that's exactly my view of agile development: To build usable software, we should be worrying about how effective a program is, more than how correct it is. Not that correctness isn't important, or that static analysis isn't amazingly useful. But in environments of complexity and uncertainty, effectiveness is ultimately the major criteria of how software will be judged.

I suspect that partly, the desire for provability and verification is the software engineering equivalent of the Laplacian dream. We should treat with suspicion, anything that proposes to be all-encompassing, especially if it requires perfect information in order to work in a world that we know to be messy and lopsided.