Ада — совершенно не тот язык, корректность программ на котором удобно доказывать. А удобно это, насколько я понимаю, для чего-нибудь типа OCaml и Haskell.
Кто-то из апологетов ФП (
smilga@lj, кажется, хотя не скажу наверняка) как-то сказал замечательную фразу: "И Perl, и Ада — помойка; просто Perl — это помойка университетского кампуса, а Ада — помойка казармы". Сразу скажу, что я с ним не полностью согласен, по результатам недолгих экспериментов с GNAT Ада мне вполне глянулась — этакий доведённый до ума Паскаль (хотя Оберон в этом смысле ещё симпатичнее, да и синтаксис там поприятнее), но до
действительно строгих языков типа того же Haskell ей и правда
очень далеко.