Lambda the Ultimate

Since the "why are type systems interesting" thread is getting so long, I thought I'd start a new thread on this somewhat more specific issue.

I agree with Frank that software development is concerned with building artefacts (i.e, program, program modules, classes, libraries and what not) about which we can reason statically - which seems to me to be tantamount to saying that we must be able to understand the product we are building, not just be able to run it.

But let's back up a bit, and consider the problematic issue of gathring software requirements. This is one of the issues software engineering is struggling with. We aren't very good at establishing what the real customer requirements are, and even when we do, customers change their mind, or want more features in the next release. The iterative life cycle model isn't only (or even primarily) about fixing bugs. It's about evolving software per customer requirements.

Now let's assume a best case scenario, where we have consistent, even formal, requirements, and we design a software system that fulfills them. We can reason statically, with the aid of a static type system, and convince ourselves that the software does what's expected from it.

Now comes the next cycle, because users want changes and additional features ("show longer names on the tracker page", "enable keywords for comments" etc.) Some would argue that unless we are talking about making trivial changes, we should start form scratch and redesign the system. For various reasons, most of them obvious, this isn't what usually happens. We modify the exisiting sytem. Techniques like regression testing help us make sure we haven't caused too much damage.

Now, let's consider the question of whether the type system helps us with this sort of activity. Obviously, types give that same static guarantees for the changed program they give any type correct program. But can the type system do more? It's likely that some of the changes require chaneging the types we use in our system. Which type systems help us make such changes locally? Do types introduce unnecessary coupling to the sytem, making evolution harder? How about support for (sound) refinement, which would allow checking that changes are consistent with prior specification, while not propagating the the changes in the system in such a way that the impact of the change becomes unmanagable?

I think these sort of questions are worth considering. Thye may help us design better type systems, which would help solve a real need.

Booch's Rational User Conference presentation on software archeology is available online.

This is related to our previous discussions about reading code, mining code for patterns and about the history of programming languages and software systems.

Obviously, many of the issues mentioned in the presentation (e.g., SLOC counts) are programming language dependent. The major case study is Eclipse, which should make this interesting to IDEs buffs as well.

See here for more on Booch's work on documenting software architecture.