История изменений

Гарантии либо есть, либо нет.

Гарантии бывают разные. Есть большая разница между «мы всё посчитали и доказали, что тут всё норм» и «нууу.. я посмотрел код, подумал, покумекал и вроде всё ок».

Повторю в третий раз, в итоге всё всё равно упирается в переход от бытового описания функционала к какому-то формальному языку, в отношении которого строгие доказательства невозможны.

Повторяй хоть 10 раз. Доказательства по ссылке, можешь скачать и ознакомиться.

И я считаю, что компилятор Си вполне хорош в этой роли, несмотря на то что он не удовлетворяет каким-то твоим теоретическим критериям.

А не ты ли выше писал:

Да, [разработчики компилятора] не правы.

То что -O2 сломан я в курсе

Ты оперделись уже: либо у тебя компилятор Си вполне хорош, либо компиляторы Си сломаны и делают говнокод.

Кстати, для seL4 был написан специальный компилятор Си – Compcert, для которого тоже доказана корректность. Написан, к слову, не на Си.

То, что они его проверяли с помощью своей математики - уже вторично, и я не знаю насколько повлияло на итог.

Нет, это первичное свойство этого микроядра. Собственно, ради него весь проект и был затеян.

Вполне возможно, что если бы они просто проверяли его методом внимательного рассмотрения и трассировки - результат был бы тем же.

Нет. У других микроядер с аналогичными показателями надёжности затраты на разработку и тестирование в разы выше. Где-то читал, что в два-три раза, примерно. И там, конечно, не просто «посмотреть глазами и в уме прогнать», а очень долгое и тщательное тестирование. Верификация с помощью мат.инструментов позволяет на этом сэкономить.

Гарантии либо есть, либо нет.

Гарантии бывают разные. Есть большая разница между «мы всё посчитали и доказали, что тут всё норм» и «нууу.. я посмотрел код, подумал, покумекал и вроде всё ок».

Повторю в третий раз, в итоге всё всё равно упирается в переход от бытового описания функционала к какому-то формальному языку, в отношении которого строгие доказательства невозможны.

Повторяй хоть 10 раз. Доказательства по ссылке, можешь скачать и ознакомиться.

И я считаю, что компилятор Си вполне хорош в этой роли, несмотря на то что он не удовлетворяет каким-то твоим теоретическим критериям.

А не ты ли выше писал:

Да, [разработчики компилятора] не правы.

То что -O2 сломан я в курсе

Ты оперделись уже: либо у тебя компилятор Си вполне хорош, либо компиляторы Си сломаны и делают говнокод.

Кстати, для seL4 был написан специальный компилятор Compcert, для которого тоже доказана корректность. Написан, кстати, не на Си.

То, что они его проверяли с помощью своей математики - уже вторично, и я не знаю насколько повлияло на итог.

Нет, это первичное свойство этого микроядра. Собственно, ради него весь проект и был затеян.

Вполне возможно, что если бы они просто проверяли его методом внимательного рассмотрения и трассировки - результат был бы тем же.

Нет. У других микроядер с аналогичными показателями надёжности затраты на разработку и тестирование в разы выше. Где-то читал, что в два-три раза, примерно. И там, конечно, не просто «посмотреть глазами и в уме прогнать», а очень долгое и тщательное тестирование. Верификация с помощью мат.инструментов позволяет на этом сэкономить.