On Wed, Jun 3, 2015 at 7:17 AM, Jonathan S. Shapiro <s...@eros-os.org> wrote:
> 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 tend to agree, this is in part why I was yammering about
constructors & first class constructors & the ability to wrap
constructors with regards to the
struct Triangle { Point a; Point b; Point c; }
vs struct RightTriangle { Point a; Point b; Point c;} example....
because it makes sense to put the constraint checking at the
constructor precisely so that every function that depends upon the
RightTriangle assertion relies on the fact that the assertion was done
at construction time, rather than doing the the assertion in every
function depends on RightTriangle constraint.
while at the same time, pure and non transforming constructors are
important as well, so it seems important that this assertion is
limited to assertions...
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
