The idiom of program design as language design can be seen as taking the robustness or "viscosity" of a solution seriously. PL designers can't get away with saying, "oh, this corner case doesn't matter because nobody would possibly ever use the language that way." For one thing, people always use languages in way you don't expect. For another, meta-programming tools like compilers that generate code in the language you've designed will use your language in ways that no human being would be caught dead doing. In other words, compilers can be seen as combinatorial test-case designers.
By contrast, building software by case analysis doesn't scale. When configuration options X, Y, and Z don't play well together in various combinations, you have to make a million special cases, the code becomes brittle, and the users must be careful never to combine features wrong.
Compositional program design (or the "closure property," in SICP-speak) is a way of building in correctness from the start, avoiding the combinatorial explosion of proof obligation1 as more features or configuration options get added. You start with simple program constructs that are well-behaved, and then only allow means of combination that preserve the good behavior. This is a common trick in PL, ranging from the design of syntax to proof by logical relations.
1I don't love this phrase, because in my experience people talk about proving properties of programs much more than they actually do it. But at least informally, we always reason about the correctness of programs, and anything that simplifies this reasoning is usually seen as an improvement, and not just by theoreticians.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment