История изменений
Исправление SZT, (текущая версия) :
О_о неужели возможно формально доказать корректность оптимизирующего компилятора?
А почему это должно быть невозможно? Если взять простой неоптимизирующий компилятор, то его работа сводится к тому, чтобы перевести прогрмму с одного языка на другой язык, при этом нигде не ошибиться. С доказательством подобного компилятора конечно же придется повозиться (если случай не тривиальный), но эта задача вполне решаемая. А сами оптимизации можно доказывать отдельно. Оптимизации компиляторов можно сравнить со всякими символьными вычислениями, например в той же Maxima, а такие вещи точно можно доказывать. Так что не вижу проблемы
В нем многие задачи NP-полные и решаются с эвристическими упрощениями, доказательство корректности тоже должно быть NP-полным.
Надо доказывать справедливость самой оптимизации вообще, что она никогда ни для какого кода не изменяет наблюдаемое поведение итоговой программы (если конечно нет UB в самом коде, тогда может быть что угодно).
Исходная версия SZT, :
О_о неужели возможно формально доказать корректность оптимизирующего компилятора?
А почему это должно быть невозможно? Если взять простой неоптимизирующий компилятор, то его работа сводится к тому, чтобы перевести прогрмму с одного языка на другой язык, при этом нигде не ошибиться. С доказательством подобного компилятора конечно же придется повозиться (если случай не тривиальный), но эта задача вполне решаемая. А сами оптимизации можно доказывать отдельно. Оптимизации компиляторов можно сравнить со всякими символьными вычислениями, например в той же Maxima, а такие вещи точно можно доказывать. Так что не вижу проблемы