История изменений
Исправление firkax, (текущая версия) :
as specified in the seL4 specification
Возвращаемся.
1) На каком языке написана спецификация?
2а) Если она написана на обычном английском - их доказательство включает в себя его строгий интерпретатор?
2б) Если она написана на каком-то формальном языке - чем это лучше ситуации, когда мы код на Си объявим спецификацией, и он автоматически будет сам себе соответствовать?
Зачем нужно ядро, которое 100% гарантированно не вылетит с паникой? Чувак, я даже не знаю.
Нет там таких гарантий, не выдумывай. Битое железо, битовые флуктуации в небитом железе и уязвимое железо никто не отменял. Что касается чисто алгоритма, то просто ручная проверка кода без всего этого теоретического задротства даст тот же результат. Разумеется, к огромным ядрам современных ОС она непосильна, но они и не написали такое ядро.
Исходная версия firkax, :
as specified in the seL4 specification
Возвращаемся.
1) На каком языке написана спецификация?
2а) Если она написана на обычном английском - их доказательство включает в себя его строгий интерпретатор?
2б) Если она написана на каком-то формальном языке - чем это лучше ситуации, когда мы код на Си объявим спецификацией, и он автоматически будет сам себе соответствовать?