Reading this fascinating (and highest voted question) on SO, Why is it faster to process a sorted array than an unsorted array? made me wonder about compiler code correctness.
For example, the answer states that:
Intel Compiler 11 does something miraculous. It interchanges the two loops...
How does a compiler programmer know when it's OK to interchange loops?
And, in general, do they use mathematical proofs to demonstrate conclusions?
How does a compiler programmer know that their compiler will generate correct code? How do they test their conclusion? Do they have to write a test suite that runs the compiler, and checks that the generated code is correct?