[TYPES] Declarative vs imperative

[Martin Escardo]

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.

  https://wiki.ubuntu.com/Security/Features#Userspace_Hardening
  http://en.wikipedia.org/wiki/Buffer_overflow_protection

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.

M.