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

Thanks, Brad.  I think I understand you, let me make sure:

   Some folks like [left-to-right eval] because it's easier to write
   formal proofs for programs with a known, fixed order of evaluation.

That would be especially Matthias's crew, who want to write proofs to
make better compilers, right?  As Matthias posted earlier, he can
often prove that it's OK to switch the order of evaluation, and then
the compiler can do so.  As opposed to a proof-challenged compiler,
which will just take whatever order of evaluation looks easier.

   I personally prefer to use sequential constructs (e.g., LET*) only when
   I really need them, and to use non-sequential, non-concurrent constructs
   (e.g., LET) the rest of the time, because that approach does a better
   job of encoding the program's design decisions (which include things
   like sequentiality).

Then here's a dumb question:  I do this all the time:

        (let* ([x (first L)]
               [p (first x)]
               [q (second x)]) 

The alternative seems to be nested lets, or not to use the shortcuts p
and q.  I don't like either one.  Even if I'm only going to use p and
q once, I still want to give 'em names!

   > Maybe it's safer to be forced to code so that order of evaluation
   > doesn't matter.  Taking this to the extreme, we get functional
   > programming, which everyone likes!

   Heh, that's my feeling on it.

So you're agreeing with me: left->right eval doesn't look safer, from
the programmer's perspective.  Maybe for the compiler writer...

   > What's this semantic ambiguity:
   > 
   >    letrec [with guaranteed left-to-right evaluation order for its
   >    initializers] with does not suffer from the semantic ambiguity
   >    which Matthias is concerned with.

   The "ambiguity" is the part where you don't necessarily know what order
   the compiler will use to lay out evaluations.

OK, thanks, I wouldn't call that an "ambiguity".  I'd say that
somebody's who's good at equivalence proofs might need to know the
order of eval, in order to drive their proofs.