[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Why are byte ports "ports" as such?



On Sun, 2006-05-21 at 07:31 -0700, bear wrote:
> ...or at least, invoke implementation-defined behavior..

With apologies to Bear, I experience severe nausea when this type of
thing is written. Scheme is completely useless for verification purposes
precisely because R5RS and Common LISP adopted this stance. It is within
the standard for a particular implementation to explicitly define
behavior in all such cases. The problem is that we cannot, in the
absence of static types, check whether an arbitrary scheme program has
defined results. Indeed, a review of the standard suggests that nearly
all occurrences of undefined behavior are a consequence of dynamic
typing.

Note: I am NOT suggesting a change to static typing. Only to defined
behavior.

This may reflect the fact that I seem to be working on software
verification at the moment, rather than any inherent problem with
Scheme. I will note only that ACL2 had to fix this issue in some very
ugly ways w.r.t. its subset of Common LISP, and drop the topic of
verification.

Speaking purely as a programmer and with a view to pragmatics, I think
that

  It is an error whenever undefined behavior is not signaled.

My reasoning is this: it is one thing to say "we do not define the
outcome of a computation". It is quite another to say "but we therefore
leave open the possibility that an implementation may run an ill-behaved
program in such a way that its ill behavior goes undetected."

>From a purely pragmatic perspective, the second part is somewhat
nauseating.

I do not believe that a well-founded standard in this day and age should
admit undefined behavior. Further, I think that the mechanism of
signaling such an error must be defined and unsuppressable. This is why
tinyscheme has abandoned indefinite-extent continuations.

I recognize that my views on this matter will not prevail, but I needed
to get them off my chest. :-)


shap