I agree with everything Matt just said (except one place where an error of mine led him astray), but I want to re-frame part of it from the perspective of usability.
Condensing a bit, Matt wrote: > What do you mean? Correctness properties are part of a module > interface... Maybe what you're getting at is the need for programmers to > anticipate > the necessary properties for a an abstraction. I see this too as just > uncovering a real problem: if you make an abstraction boundary without > knowing what properties are really depended upon, then the abstraction > was premature. Mathematically speaking, an abstraction should tell you > the set of correct implementations. > > > - The properties we *need* at the interface tend to grow without > textually > > reasonable bound. > > Yes. > A module programmer probably can't anticipate all of the properties that you (a consumer of the module) might require. Maybe all it really means is that (a) not all things can be checked, or alternatively (b) unsupported assumptions have to be documented in the form of assertions. Neither of those seems like the end of the world to me. But from a usability perspective, most properties are distractions to most programmers most of the time. And *some* kinds of properties have a way of growing explosively. Consider bounds checks. There are a bunch of examples in which a seemingly simple procedure, ends up with a whole bunch of fragmented sub-bound properties that result from case analysis. Those sub-bound properties don't really mean much to the human, but they sure clutter up the specification! I think there is a human factors tradeoff. "Weak" type systems are weak in the sense that they say much less about guarantees, but "strong" in the sense that the humans actually understand what the stated guarantees *are*. Guarantees that I can't understand don't provide me with a lot of value. Finally, there are language limits. Sometimes we want to state one property, but due to limits of the property language we are forced to approximate that property by a collection of other properties that we *can* express. The catch is: that approximation may or may not actually capture what we *thought* it captured. I have no conclusion here. Just an observation that at a certain point clutter trumps precision, and it's hard to know where to draw the line when it's all so case-specific. > > > This becomes a particular concern as discharge obligations become > embedded > > in standard libraries. > > Hmm. How would that happen? I mis-wrote. What I intended to be saying is that we either end up with clutter at library boundary specifications, or we end up forced to make the libraries progressively more translucent. > > It may well be that properties tied > > to types are cleaner in these regards than properties more generally. > > I don't know what you mean by "properties tied to types". Aren't all > properties tied to the type of object they are properties of? > Certainly not! Global information flow properties are a counter-example. But it may be true that all properties that are expressible with refinement types are locally dischargeable. Control flow properties are often locally dischargeable as well. Bounds checking properties are locally dischargeable, but often at the cost that sub-parts of the discharge "leak" into the procedure specification. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
