[TYPES] Declarative vs imperative

Martin Escardo m.escardo at cs.bham.ac.uk
Tue Apr 23 16:38:29 EDT 2013

On 23/04/13 19:32, Uday S Reddy wrote:
> If I paid
> good money for a C compiler, I would definitely demand that it should have
> an option to randomize the evaluation order of arguments.

You can compliantly randomize code generation for security purposes, as 
is well known --- see e.g.


So, yes, as Uday says, a compiler can be non-deterministic in practice, 
even deliberately (and I suspect non-deliberately too).

I haven't seen randomization for the resolution of unspecified 
evaluation order in the standard definition of C (or any underspecified 
language) yet, as Uday suggests, but I would be surprised if people 
working on (applied or theoretical) program verification didn't think of 
that already.


More information about the Types-list mailing list