Исходное сообщение
"Линус Торвальдс не исключил возможность интеграции поддержки..." Отправлено Аноним, 26-Июн-22 10:19
1. Пока не весь код Mumen написан на SOARK-2014 и ASM, есть немного кода на неверифицируемой ADA+2012: https://git.codelabs.ch/?p=muen.git;a=blob;f=README 2. Ядро OS это очень низкоуровневое ПО работающие напрямую с железом, асемблерными инструкциями процессора. На данном этапе эволюции процессоров и языков программирования пока необходимо использовать асеблерный код для написание некоторых частей OS. Да, поддержку CPU без асеблера не напишешь. Асемблерный код неверифицируется SPARK, весь Асемблерный код необходимо проверять руками, но его немного: https://git.codelabs.ch/?p=muen.git;a=tree;f=kernel/src/asm В отношении асемблерного кода нет гарантий безопасности и надежности. 3. Использование неверифицируемой ADA, влияет только на математические доказательства отсутствия ошибок и корректности работы с памятью на уровне исходных текстов. По надежности и безопасности ПО на ADA на порядок выше чем C и Rust. 4. Прикладное ПО, это не ядро ОС, можно писать на чистом SPARK без ASM.

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
	Введите код, изображенный на картинке: