Без заголовка

> Хотя я не поверю, что выбор языка программирования для истребителя будет зависеть от выбранного способа верификации. Ну для промышленной верификации вообще выбор языка невелик: Си, Джава и С# :). Ну может еще OCaml или еще какие функциональные. Си и так используется в embedded и real-time programming. Джава потихоньку тоже. Про С# не в курсе, зотя вполне возможно что Windows CE будут рано или поздно использовать и в истербителях (страшно, конечно, но на атомных подлодках уже используют) . С другой стороны в данном случае велика польза от верификации. Так что затраты на доказательство корректности императивных операций окупаются. У самолетов софт кстати тоже верифицируется. Точнее там активно используют static checking и abstract interpretation - т.е. в некотором смысле ограниченную верификацию. Французы целую школу Abstract Interpretation сделали как раз похоже в процессе создания софта для Airbus'ов. Немцы использовали верификацию Жабы для железнодорожного софта - чтобы поезда тормозили и не врезались в друг друга. Верифицировали эти модели на Жабе. Шведы и немцы верификацией очень активно занимаются.