[plt-scheme] Re: to define, or to let

Re the ambiguity in R5RS programs, the point that some are concerned about
is that it's difficult to prove that expressions with unspecified
evaluation order are not ambiguous, in the mathematical proof sense, even
though in practice it may be easy enough to check this.  The assertion of
the programmer that a program is correct is of little interest to a
semanticist, who wants to prove things about programs.

But I think this, and the last couple of posts, hints at an ongoing
confusion in this discussion, which mixes up at least two different
questions, and in fact up to four questions, which in many respects are
fairly orthogonal to each other.  The four questions are:

1. Should a specification like R5RS have unspecified evaluation order?

2. Should semanticists be able to restrict their analyses to languages
with fixed evaluation order?

3. Should a Scheme implementation (like MzScheme) fix a particular
evaluation order?

4. Regardless of actual evaluation order, should function application,
LET, and similar constructs act as assertions of order independence?

Two of these questions are fairly easy to answer:

#2: The answer is yes, if semanticists wants to simplify matters and deal
with fixed evaluation order, they should do so, and it makes sense to do
so.

#3: Yes, it is perfectly R5RS-compliant, and acceptable in other ways, for
an implementation like MzScheme to define a fixed evaluation order, and
left->right is a reasonable choice here.

The other two are more controversial:

#4, asserting order-independence: R5RS answers yes to this question, by
virtue of its default unspecified evaluation order.  However, function
application and LET can be treated as asserting order-independence even if
they are actually evaluated in a fixed order.  This means that a yes
answer to this question is not necessarily inconsistent with either answer
to *any* of the other questions!  I think that this "have your cake and
eat it" position has often been missed in this discussion.  Arguing
against a yes answer, however, are those who, once they have fixed
evaluation order in a language, would like to be able to rely on that
order anywhere, without requiring special constructs to be used.  This
really seems to be a matter of convenience at best.  Most of the arguments
I've given have been to show that this entails an unfortunate loss of
information and expressiveness.  The fact of that loss can't be denied,
and there's a simple proof of it: you can automatically convert any
program with order-independence assertions to one without such assertions,
but you can't, in general, automatically convert the other way.  However,
some people consider the information in question to be of insufficient
importance to warrant supporting the ability to express it.

#1, about R5RS, is also difficult to answer, because there are legitimate
pressures to fix evaluation order at that level, both to support the
requirements of #2 (semantic analysis), and to support the desires of
those who want to answer no to #4 (order-independence assertions).  Fixing
order at this level, however, also has its downsides, which were
recognized by the RRRS authors as far back as 1984.  IMO, one of the
biggest advantages to retaining unspecified order in R5RS is that it acts
as a strong enforcer of #4, for portable Scheme code.

Anton