Re: Full Specification

[Paul Hudak <hudak-paul@YALE.ARPA>]

I understand the desire for underspecification in certain places (for 
example order-of-evaluation of arguments) but don't forget probably the 
most critical advantage of full specification:  portability.  To take 
the order-of-evaluation example, one can only say: "this program is portable 
as long as none of the arguments induce any side-effects."  Every place you 
decide to admit underspecification, you have to make this kind of qualifying 
remark.  People who want a STANDARD aren't going to like it.

Another comment, concerning Chris Hanson's comment:

    3. Full specification is a never ending game.  When have we finished
    specifying everything?  People will be forever noticing new details
    that we have missed and forcing us to specify some behavior for them.
    In fact, most of those details are uninteresting.
    
    In contrast, underspecification is automatic.  By overlooking some
    behavior, we have "underspecified" it.  This is appropriate, since the
    kind of thing that is likely to be overlooked is precisely the thing
    least interesting to specify.

The flip side of this argument is that many of those overlooked behaviors 
are VERY interesting; in fact critical.  The whole purpose in giving a formal 
semantics to a language is to uncover those subtle unspecified behaviors that 
raise havoc with users.  If you choose to underspecify something, then at least 
specify that you have chosen to underspecify!  In other words, make it a formal 
part of the language semantics.  

And by the way, if one *really* believes in underspecification, then I should 
point out that in the Scheme report the order of evaluation of arguments is 
not underspecified enough!  In particular, the order is informally said to
be "indeterminate" and in the formal semantics it is said to be dictated
by a fixed function called PERMUTE.  This is overspecified in two ways:

1) PERMUTE being fixed implies that for a given program a compiler must
   use the *same* (although arbitrary) evaluation order for every call.
2) Even without that constraint, the implementation is forced to perform
   the evaluations *sequentially*, thus precluding parallel evaluation
   of the arguments, unless the compiler can prove non-interference or
   guarantee correctness with respect to PERMUTE.

Both of these overspecifications constrain the implementor.  But I should
point out that fixing them in the formal semantics requires a shift from
a deterministic semantics to a non-deterministic one, most likely requiring
powerdomains, and not something to be taken lightly.

    -Paul
-------