Как программисты гарантируют, что компиляторы создают правильный код?

Читая этот увлекательный (и получивший наибольшее количество голосов вопрос )на SO, Почему отсортированный массив обрабатывается быстрее, чем несортированный массив? заставил меня задуматься о корректности кода компилятора.

Например, ответ гласит, что:

Intel Compiler 11 does something miraculous. It interchanges the two loops...

Как программист компилятора узнает, когда циклы можно менять местами?

И вообще, используют ли они математические доказательства для демонстрации выводов?

Откуда программист компилятора знает, что его компилятор сгенерирует правильный код? Как они проверяют свой вывод? Должны ли они написать набор тестов, который запускает компилятор и проверяет,сгенерированный кодверно?