On Wed, Jun 3, 2015 at 10:17 AM, Jonathan S. Shapiro <[email protected]> wrote: >> > - 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.
I'm not sure what you're saying here. I made three attempts to make a better reply to this paragraph, and each time, I realized I'm making an unsafe assumption about what you're getting at. > 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. A nice thing about refinement types is that they have an entirely common-sense notion of subtyping: a subtype's properties imply the supertype's properties. If the fully-annotated, most specific type is TMI most of the time, you can also point out a supertype with fewer properties, leaving out the rarely-used ones. And if you buy into refinement types as an application of proofs, you can also just have proofs of the properties be separate module members from the object itself. This is technically not _just_ refinement types anymore, I guess. Well actually, you could consider it refinement of module types. > 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! Hmm. Sounds like the result of bad automation. It's the job of a human (or much smarter automation) to find sufficient preconditions that are understandable, and can be met in practice. If there don't seem to be such sufficient preconditions, I'd just say the code is impractical. > 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. That's true, I guess. But _someone_ understands them, right? Or else how did they get there? Bad automation again? Bad automation can find weakest preconditions that are needlessly weak, and hard to understand, or strongest postconditions that are excessively strong, and hard to understand. If that's the best automation can do for now, it just sounds to me that it's up to the programmer to find the right conditions. Maybe the automation is handy sometimes. But if only sometimes, then maybe it belongs in an IDE, and not the language itself. > 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. That sounds like a great argument for nice, strong property languages. :) But actually, you always have to worry about specs not saying what you thought they said. That's a hard problem, and there doesn't seem to be a silver bullet for it. > 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. Yeah. The assumption behind my whole project is that real cases will have reasonable solutions, and programmers can learn to do this, and it will be worth it. But that's just what feels true to me. I will accept honorable defeat if my project technically works, but it turns out my assumption that it's useful is false. (And I'll have to accept dishonorable defeat if I can't get it working. :) ) >> > 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. That makes it sound like you are expecting premature abstractions. Come to think of it, that's perhaps a reasonable expectation. Programmers are sort of "spoiled" by the fact that they don't need to fully understand their code to get it running. You can try stuff that might not work. This attitude is not bad, in and of itself, but it conflicts with the documentation burden of stronger types. I think programmers should give their programs strong types _after_ they informally seem to be working and properly-structured. In short, I don't think strong typing is good for prototyping. Regarding translucent libraries in particular, in Coq, I use mostly translucent libraries (the default). You usually _don't_ know what properties you'll need in advance, and what's so bad about translucent libraries? You only need abstraction once you have two libraries, both proven compatible with the client. And at that point, you do know what properties the client relies on. >> > 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. Derp. Yes, of course, there are plenty of counter-examples. I said "property", but I was thinking "property of a value". I think the properties included in a refinement type are always properties of a prospective element of the type. > 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. As long as you count controlled leakage of obligations to the procedure specification as locally-dischargeable, then yeah, I think all refinements are locally-dischargeable. But I dunno, it's not the way I'd normally think about it. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
