Ада 95.
Имеет транслятор в Си (опционально с исключениями C++) AdaMagic, но при этом экранирует программиста от специфичных для Си приколов, когда код на Си не другим транслятором создаётся, а человеком пишется. Вне зависимости от того, трансляция в Си или C++, есть RAII. И есть верификация SPARK. Хотя, если так подумать, в ядре RAII — не очень хорошая идея, а вот верификация — вполне.
У меня на уме как раз есть такая операционка. Это нужно для трансляции для браузеров. Я хочу зелёные потоки на WebAssembly натянуть. При выбранном подходе Wasm становится как бы микроконтроллером, а вызовы из JavaScript становятся прерываниями. User-space код — это код зелёных потоков, а так, как зелёных потоков может быть много, то какой-то код ещё должен переключать контекст. И это получается что-то вроде kernel-space операционной системы. Вот это самое ядро гипотетически ещё можно SPARK верифицировать.
