Оказывается, язык Ада не умер, а плавно превратился в SPARK.
SPARK 2014 Reference Manual: http://docs.adacore.com/spark2014-docs/html/lrm/
Книга, объясняющая методологию использования языка SPARK для разработки систем высокой надёжности: https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf
Исходники микроядра Muen, написанного на SPARK: https://muen.codelabs.ch/
SPARK 2014 Reference Manual: http://docs.adacore.com/spark2014-docs/html/lrm/
Книга, объясняющая методологию использования языка SPARK для разработки систем высокой надёжности: https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf
Исходники микроядра Muen, написанного на SPARK: https://muen.codelabs.ch/
