История изменений
Исправление SZT, (текущая версия) :
А кто докажет, что нет ошибки в переводе?
А этот перевод осуществляется в автоматическом режиме некоей программой, написанной на Ocaml. Чтобы доказать отсутствие ошибок(ошибок перевода из одного представления в другое) в ней, нужно ввести некое формальное описание языка (т.е. попросту перевести описание стандарта Си на некий машинночитаемый язык) и потом каким-то образом доказать, что для всех валидных программ на Си будет полностью корректно и с полным сохранением смысла произведено преобразование в язык WhyMl http://why3.lri.fr/#documentation например. Это довольно нетривиальная задача, согласен. Даже в компиляторах порой ловят баги, когда компилятор в ответ на полностью корректный и не-UBшный C код генерирует машинный код, который этому самому С-коду не соответствует, а это очень и очень плохо т.к. на этом могут «жить» какие-нибудь трудноуловимые баги http://blog.regehr.org/archives/1036
https://gcc.gnu.org/bugzilla/buglist.cgi?keywords=wrong-code&list_id=1459...
Исходная версия SZT, :
А кто докажет, что нет ошибки в переводе?
А этот перевод осуществляется в автоматическом режиме некоей программой, написанной на Ocaml. Чтобы доказать отсутствие ошибок(ошибок перевода из одного представления в другое) в ней, нужно ввести некое формальное описание языка (т.е. попросту перевести описание стандарта Си на некий машинночитаемый язык) и потом каким-то образом доказать, что для всех валидных программ на Си будет полностью корректно и с полным сохранением смысла произведено преобразование в язык WhyMl http://why3.lri.fr/#documentation например. Это довольно нетривиальная задача, согласен. Даже в компиляторах порой ловят баги, когда компилятор в ответ на полностью корректный и не-UBшный C код генерирует машинный код, который этому самому С-коду не соответствует, а это очень и очень плохо т.к. на этом могут «жить» какие-нибудь трудноуловимые баги http://blog.regehr.org/archives/1036