Исходное сообщение
"Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..." Отправлено hummermania, 25-Июн-14 17:57
Всё как обычно - мгновенное и "глубоко компетентное" суждение о ранее незнакомом предмете при его поверхностном обзоре. Выше в комментах в PDF-ке в разделе References есть достаточно интересные документы. Особенно из свежих. Что нарылось при беглом обзоре некоторых из них:   - С-шные функции перед реализацией пишутся на языке типа Haskell (есть на него ссылки в доках) - походу функциональный стиль рулит.   - Любые конструкции языка приводящие к сайд-эффектам либо не используются вовсе, либо имеют ограниченное применение.   - Работа с типами, выделением памяти, IPC, threading и пр. объекты проверяются матаппаратом и в случае нессответствия вручную оптимизируются (вроде так)   - Для верификации кода юзают какой-то хитрый комплекс Isabella/HOL   - Плюс еще очень много мат.теории - надо копать в доках до просветления. Может где-то и ошибаюсь, поправьте предметно...