Здравствуйте, Слава, Вы писали:

С>Я не думаю, что вы найдёте более подходящий язык за исключением какой-нибудь экзотики вроде уже упомянутого F*

А как насчёт типизационных меток?

Не подскажете, что лучше почитать по Аде, чтобы было понятно и, желательно, на русском?

И какой лучше использовать бесплатный компилятор (желательно, чтобы он умел для UEFI делать программы — это специально подготовленные PE32+ файлы; Linux/Windows тоже не помешает)
И, собственно, бесплатные компиляторы такое умеют вообще делать???

Здравствуйте, Слава, Вы писали:

С>Я не думаю, что вы найдёте более подходящий язык за исключением какой-нибудь экзотики вроде уже упомянутого F*

А как насчёт типизационных меток?

Не подскажете, что лучше почитать по Аде, чтобы было понятно и, желательно, на русском?

И какой лучше использовать бесплатный компилятор (желательно, чтобы он умел для UEFI делать программы — это специально подготовленные PE32+ файлы; Linux/Windows тоже не помешает)
И, собственно, бесплатные компиляторы такое умеют вообще делать???

Что-то посмотрел я на модуль SPARK в GNAT, и вообще не понял, где на него документация. Что и как он делает "prove"