The balance of expressiveness and reasonability

Yesterday during the question and answer period of a talk, Matthias pointed out that there is usually a balance involved in language design between the expressive power of the language and the ability to do local reasoning on programs in the language. This confirmed and crystallized an intuition I've been mulling for a while. It was always clear to me that an increase in expressivity is not inherently "good" (for example, in his expressivity paper, Matthias proves that set! increases the expressive power of a language, but he certainly wasn't advocating the gratuitous use of mutation). But I hadn't quite put my finger on it until Matthias's comment.

It's in fact a direct result of the idea that powerful language constructs require global transformations: when you use a construct that affects your whole program, then you have to reason globally about the changes it makes. Essentially this means you'll need more powerful reasoning tools to be able to tame the power -- which can be both constructive and destructive -- of the new language feature.

As a simple example, the other day I was writing some pattern matching code in "substitution-passing style," where the matcher returns either a substitution or #f, the latter indicating that it failed to match. But before I knew it, I ended up with loads of intermediate checks to see if intermediate matches had failed. The real kicker was when I started writing helper functions (match-list) that themselves had to propagate these checks. I finally decided that there was no need to reimplement a poor man's exception mechanism when my implementation language already has one. So I changed the interface to have matchers raise a match-error exception when matching fails. But the upshot is that the code no longer locally indicates that such an exception can occur; this property then ends up in comments and in proof obligations of the clients.

Type and effect systems like Java's checked exceptions can mitigate these non-local changes by checking and maintaining invariants about the effects. This is precisely an example of the kinds of reasoning tools that help tame the power of expressive language features.

Another example is dynamic dispatch in OO languages. I was having a discussion last year with Shriram about local reasoning and AOP, and he made an analogy to dynamic dispatch. Programmers are completely accustomed to looking at a local piece of code and not knowing its behavior, he argued; in OO languages a method call could refer to any arbitrary reimplementation of the method. But this is par for the course, and in practice we assume that the reimplementations will be well-behaved.

Furthermore, we don't use this power with reckless abandon. I found a relevant quote from an aside made by Paul Wilson in the midst of an unrelated Usenet conversation:

It turns out that at most overtly polymorphic call sites in OO programs, the receiver is always of the same class. And of the minority of truly polymorphic call sites, there's only two or three classes of receiver. That makes it sound like OO doesn't do much work for you. But it does, really, because the 10% of sites where you need it, you need it bad.

Now, I was initially unhappy with these "pragmatic" justifications of language features that destroy local reasoning. They seemed to pit abstraction and local reasoning on one side against usefulness and practicality on the other, and I'm simply not prepared to give up on abstraction. I just don't see how anyone could survive a software project without it. But the underlying tension is this one between expressive power and local reasoning. So good language design requires a sweet spot between features that are just powerful enough to express the kinds of things you want to express while not being too much harder to reason about.¹

I believe that the core principles of program design (should) stem from functional programming. But many important design principles require more powerful tools than pure functional programming offers. So more powerful language features are important. On the other hand, any time you introduce effects that can affect the behavior of arbitrary parts of a program, you need to be able to mitigate those changes with reasoning tools, whether they are proof techniques or automated reasoning software.

---

¹As Moore's law allows lightweight formal methods to get closer to what used to be heavyweight formal methods, we should be able to make more powerful reasoning tools for our programs, which should allow us to slide the scale further in favor of more expressive language features. Which is all to say that I should really check out Shriram and Kathi's work on formal methods for AOP.