[plt-scheme] to define, or to let

Robby Findler wrote:
> Anton, you're asking to allow programmers to specify a (currently)
> uncheckable intent. So, clearly we need more research on how to make
> such intent checkable in order to detect buggy programs.

It's currently uncheckable statically.  Dynamically, it presumably wouldn't
be difficult to implement a torture-test argument-order randomizer for the
places marked order-independent, to at least force the program to fail if
it's buggy.  At that point, contracts kick in and pinpoint the problem.

On the flip side, you'd like to prevent programmers from specifying an
intent, even though specifying it can make static checkability easier for
humans.  Removing the specification of intent makes it harder for humans to
check, and impossible for machines to check.  Here's a table to summarize
checkability of side effect sequence dependency errors:

                Unspecified          Fixed
                Order                Order
                ======================================
Human                                Harder,
Checkability    Easier               but many possible
                                     errors are masked

Machine         Static, difficult;   Utterly
Checkability    Dynamic, possible    impossible


That left column appeals to me.


> Good, get cracking. :)

I'll take that under advisement.  But I thought the whole point of
discussing it here was if I could convince you, you'd save me the trouble.
;)

> But, until you are done and we can detect such errors we must take
> programmers at their "word" which, in my opinion, is a bad idea.
> In an implementation that is aggressive about re-ordering such things,
> it becomes very hard to ensure reliability since the behavior of the
> program may change in weird ways based on the environment in which
> it runs. To my mind, the safer point in the design space is a fixed
> order of evaluation. At least your program's behavior will be
> predictable so you can write test suites, etc.

Part of where I'm coming from is that I'm interested in using Scheme as a
functional language, avoiding mutation as much as possible, or at least
isolating it, since doing this has all sorts of benefits.  But Scheme
doesn't do much to help you enforce being functional.

One way to address the static checking issue would be to have the ability to
declare procedures mutation-free, which would then enable order-independent
constructs to do some real checking.  But that would require static
knowledge of the mutation-free status of procedures in other modules.

I know many Schemes would have a problem with achieving that.  I don't have
a good enough handle on the innards of PLT's module system and compilation
model to know whether it could support something like that, in theory.
Could it?

Anton