Re: Formal semantics for C

  > Compiler optimization researchers perform non-trivial analyses of C
  > programs (e.g., a pointer alias analysis) by ducking the issue of unsafe
  > operations: the simply assume that unsafe operations are never executed.

  This is not "ducking the issue".  On the contrary, this is an approach
  whose correctness can be proven from the semantics of C, as specified
  in the C standard or more formally in the works referred to earlier.

Nonsense!  These optimizations are incorrect (do not preserve the
meaning of programs) because they presume programs never perform unsafe
operation, but in fact they do.  

-- Corky Cartwright

Follow-Ups: References: