Diego Olivier Fernandez Pons a écrit :
>     Bonjour,
> 
> 
>>why should the evaluation order be specified: this is needed if you
>>want to formally reason about programs ... as far as I know.
> 
> 
> Could you elaborate more on this ?
> 
> I see the evaluation order in Caml more as a compiler optimization
> problem that a semantic one. If I need a specific evaluation order, I
> just sequencialize my program explicitelly.
> 

Let us say you want to prove a program using references ...
one possible way is to translate is automatically in a purely functional 
program using a state monad ... then you need to specify the evaluation 
order to define the translation of

let x = f a_1 ... a_n in

which could approximately be (x' denotes the translation of x) ans s 
denotes the states holding the map table assigning values to addresses

let s,a_n  = a'_n s in
let s,a_(n-1) = a'_(n-1) s in
..
let s,a_1 = a'_1 s in
let s,x = f' s a_1 ... a_n in

to define this translation, you need to know the evaluation order and it 
is not reasonnable to
assume that the program you want to prove if fully sequentialized (and 
if you want to force sequentialized program then you should only allow 
variables as function arguments in the language definition ;-).

Remark: clearly, a good proof system should not show the monadic 
translation and hide it behind the scene ... but  such a system for full 
ML does not exist yes (as far as I know).