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

Anton, I said I was out, but you're so sharp & so much fun:

   Remember, too, that in our functionally-oriented programs, we want
   to keep side effects to a minimum.  

I have a related opinion: There's nothing special about Scheme, other
than the Lambda Calculus, or really, Plotkin/Felleisen LC_v.  That's
why RnRS is busted.  It's not because Clinger et al did did a bad job.
It's because we haven't figured out the right language yet.  That is:

LC_v is great, and Scheme is LC_v with some mutation slapped on.
Users demand mutation, but there's various ways to slap it on, and I
don't think anyone's figured out the "right" mutation-ality.  So RnRS
isn't a language spec, but a historical description.  There's no
reason to follow it.  Mzscheme forges ahead in a new mutation-ality
direction: uniform left->right eval order, sequencing in letrec, etc.
These are features to take advantage of, and no longer bugs.  I don't
have an opinion about whether this is better for the Scheme
programmers.  But it's better for the PLT maintainers, because their
Math skills require fixed algorithms.  Quite likely, it will turn out
to be better for schemers.  If not, it will be a good experiment.

   > 2) As you explained, the historical reason for unspecified eval
   > order is C compiler speed.  It's not even a Scheme idea!

   I don't think I explained that, since I don't believe that's the
   "historical reason for unspecified eval order" in general.  I've
   previously given C as an example of a language with unspecified
   eval order.  

Sorry I misquoted you.  I bet speed's why C has unsp eval order.

   > Again, MF's crew of theorem provers are sharp enough to overcome
   > the disadvantage of fixed left->right eval order.  So they do it.
   > They can & they must.

   PLT isn't analyzing user programs for side effect sequence
   dependencies.

Maybe you misunderstood me.  I meant that the PLT folks can reason
successfully about algorithms, including their left->right
interpreter.  As MF posted, they can even optimize Mzscheme, e.g. by
proving sometimes that they can safely switch the order of evaluation.

   > As John Clements explained, an R5RS Scheme program isn't valid
   > until the programmer proves to him or herself that their program
   > does not depend on order of evaluation!

   In mzscheme, your program isn't proved valid, with respect to its
   requirements, until you've proved that there are no places where
   you have depended on order of evaluation unintentionally.  

No, I don't want to say a program is invalid if the user doesn't fully
understand why the program works.  John's meaning of invalidity is if
the R5RS program won't run correctly if compilers switch the order.