История изменений
Исправление shkolnick-kun, (текущая версия) :
На SPARK в AdaCore cделали tcp-ip-стек, вроде с доказанной корректностью.
Думаю, что для микроядра можно сделать почти то же самое, но полностью пруфануть соответствие микроядра спецификации на SPARK ПМCМ не представляется возможным, ибо там есть ансейф полюбому.
Гоню! Можно написать на спарке эмулятор целевой платформы (ВМ), сделать «микроядро» «внешним» по отношению к памяти, пруфануть коррестность.
Потом можно написать ассемблерные вставки, перенести ядро внутрь ВМ, и доказать бинарную совместимость.
Сдается мне, что это будет быстрее, чем то, что сделали в команде SeL4
Команда разработчиков SeL4 для этого написали «микроядро» на Хаскеле, а потом написали микроядро на Си и пруфанули их полную бинарную совместимость в смысле работы с памятью.
Исходная версия shkolnick-kun, :
На SPARK в AdaCore cделали tcp-ip-стек, вроде с доказанной корректностью.
Думаю, что для микроядра можно сделать почти то же самое, но полностью пруфануть соответствие микроядра спецификации на SPARK ПМСМ не представляется возможным, ибо там есть ансейф полюбому.
Команда разработчиков SeL4 для этого написали «микроядро» на Хаскеле, а потом написали микроядро на Си и пруфанули их полную бинарную совместимость в смысле работы с памятью.