determinism question

[Don Smith]

>But I don't think the legality of a program should depend on optimizations.
>The compiler should check the legality first, and then optimize afterwards.

I declare a procedure "det"; by looking just at the definition of
that procedure, and at the type, mode, and determinism declarations
of other procedures, the compiler can't prove that it is deterministic.
Is it fair to look at the other procedures' definitions as well?  Within 
a module, I'd say "Yes!"    The compiler's ability to verify determinism
declarations can never be perfect, but all sorts of inter-procedural
information should be accessible, including the specific clauses used.
Accessing that information is not an "optimization"; it's just doing
reasoning based on the procedure's logical definition, which is an 
executable, logical specification.  After all, the type, mode, and 
determinism declarations aren't a specification of the procedure's meaning,
just some sort of approximation.

> For example, you don't want to transform a terminating program
> into one that doesn't terminate.  Nor do you want to transform ...
> So [??????????] the transformations should preserve mode-correctness and 
> determinism-correctness: you don't want to transform a mode-correct 
> program into one containing mode errors, and you don't want to transform
> a determinism-correct program into one containing determinism errors.

I don't see how doing optimizations within a module could lead to errors
of these sorts.  Even if you reimplemented a called procedure so as to change
its clauses (but not its declarations), then as long as that procedure
is in the same module, which I am assuming, the changes would be visible.

That the allowed between-module optimizations differ from the allowed
within-module optimizations is no surprise, given the purpose of modules
(and the purpose of determinism declarations).

   Don