[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Full Specification
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.