MO
Это можно запилить
Size: a a a
2020 May 14
MO
Потому что компилятор C там сравнительно маленький
MO
Я ща без шутеек
.
Потому что компилятор C там сравнительно маленький
Simpl
.
CompCert C
.
И why3
.
Проблема продумать микроядро
.
Набор команд
.
Совместимость с написанным софтом
MO
Кста компилятор же посути не нужен
.
Который развивался в течении 50 лет
.
Совместимость с написанным софтом
Мы же хотим драйвера для nvidia использовать
MO
Тебе нужен парсер кода который будет проверять определенные аксиомы
MO
Проблема продумать микроядро
Микроядро не нужно
.
Тебе нужен парсер кода который будет проверять определенные аксиомы
Why3
MO
Опять же отсылаю к plan9
.
Опять же отсылаю к plan9
Его верифицировать?
MO
Нахуя сначала все выносить в юзерспейс, а потом решать проблемы свитчконтекста
MO
Если можно ситуативно располагать серверы
MO
В ядре и вне ядра