История изменений
Исправление SZT, (текущая версия) :
При чем тут вообще SMT солверы? Там ничего никто не доказывал в отношении самого компилятора и процесса компилирования, там просто сравнивалась скорость солвера на разных процессорах. Если тебе нужен компилятор с доказанной корректностью, вот он - http://compcert.inria.fr/compcert-C.html
What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues.
Только это Си, для плюсов такого еще не создано, да и вряд ли создадут в ближайшее время, учитывая сложность самих плюсов
Исходная версия SZT, :
Причем тут вообще SMT солверы? Там ничего никто не доказывал в отношении самого компилятора и процесса компилирования. Если тебе нужен компилятор с доказанной корректностью, вот он - http://compcert.inria.fr/compcert-C.html
What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues.
Только это Си, для плюсов такого еще не создано, да и вряд ли создадут в ближайшее время, учитывая сложность самих плюсов