Исправление Manhunt, (текущая версия) :
Даже если сам CompCert внтури себя почти верифицирован (на самом деле верифицированы фантазии авторов clight, поскольку формального описания семантики для Си тупо не существует, и на этом «верификацию» компиляторов Си можно заканчивать), на конечных устройствах работать будет не CompCert, а на наговняканная на Си прошивка (скомпилированная CompCert-ом).
Исходная версия Manhunt, :
Даже если сам CompCert внтури себя почти верифицирован (на самом деле верифицированы фантазии авторов clight, поскольку формального описания семантики для Си тупо не существует, и на этом «верификацию» компиляторов Си можно заканчивать), на конечных устройствах работать будет не CompCert, на наговняканная на Си прошивка (скомпилированная CompCert-ом).