Исправление Manhunt, (текущая версия) :
Ты так говоришь, будто сказанное тобой должно резко сделать CompCert ненужным. На баги оптимизирующих компиляторов никогда не натыкался?
По моим подсчетам, на каждый на практике помешавший моей команде баг в gcc, приходится никак не меньше 1000 серьезных багов в коде, который в этот gcc скармливали. Так что абсолютно непогрешимый компилятор Си сам по себе качественной разницы не сделает.
Исправление Manhunt, :
Ты так говоришь, будто сказанное тобой должно резко сделать CompCert ненужным. На баги оптимизирующих компиляторов никогда не натыкался?
По моим подсчетам, на каждый на практике помешавший баг в gcc, приходится никак не меньше 1000 серьезных багов в коде, который в этот gcc скармливали. Так что абсолютно непогрешимый компилятор Си сам по себе качественной разницы не сделает.
Исправление Manhunt, :
Ты так говоришь, будто сказанное тобой должно резко сделать CompCert ненужным. На баги оптимизирующих компиляторов никогда не натыкался?
По моим подсчетам, на каждый на практике помешавший баг в gcc, приходится никак не меньше 1000 багов в коде, который в этот gcc скармливали. Так что абсолютно непогрешимый компилятор Си сам по себе качественной разницы не сделает.
Исходная версия Manhunt, :
Ты так говоришь, будто сказанное тобой должно резко сделать CompCert ненужным. На баги оптимизирующих компиляторов никогда не натыкался?
По моим подсчетам, на каждый на практике помешавший баг в gcc приходится никак не меньше 1000 багов в коде, который в этот gcc скармливали. Так что абсолютно непогрешимый компилятор Си сам по себе качественной разницы не сделает.