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

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

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

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