[r6rs-discuss] Re: [Formal] Allow compilers to reject obvious violations

From: William D Clinger <will>
Date: Sun Feb 25 23:33:04 2007

I am posting this as an individual member of the Scheme
community. I am not speaking for the R6RS editors, and
this message should not be confused with the editors'
eventual formal response.

Matthias Felleisen wrote:
> You keep evading my real question. So can you produce an algorithmic
> description of when you will allow compilers to give up?

I could, but I quite purposefully did not and will not.
If I did, it would probably take the form of a complete
proof procedure for some logic that incorporates a formal
semantics such as the one in the draft R6RS, and any such
thing would be partly arbitrary, inasmuch as it could be
replaced by a stronger system. (For those of you who are
still following along at home, that's a corollary of one
of Goedel's incompleteness theorems.) A formal statement
of that kind of algorithm would not be very enlightening;
the paragraph I suggested in my formal comment says it
better.

The important thing is the word "allow". I do not wish
to require any compiler to implement a complete proof
procedure for the predicate described in my formal
comment, and I certainly do not wish to require any
compiler to decide how such attempted proofs will come
out, since that is recursively undecidable.

Some have argued, quite reasonably, that the criterion
for rejecting a program should be the same in every
implementation. Reasonable though it be, that seems
a little odd to me, since the result of macro expanding
(let alone executing) a program will differ between
implementations, with some programs blowing up at macro
expansion time (or run time) in some implementations
but not others, while some will blow up some but not
all of the time in yet others. I do understand the
sentiment, however whimsical it may seem to me.

If we accept that the criterion for rejecting a program
should be the same in all implementations, then the
criteria should be decidable. In my opinion, criteria
that are supposed to be the same in all implementations
should also be simple; otherwise it is hard to reason
about the criteria, which seems like the main benefit
we could hope to achieve by requiring the criteria to
be the same. (I am discounting portability somewhat,
because absolute portability is a lost cause in the
presence of low-level macros.) As at least one person
has argued, the implementation-independent criteria
for rejection that are laid down in the draft R6RS
might already be too complicated.

Will
Received on Sun Feb 25 2007 - 23:32:59 UTC