Honest question: Is there something about Ada that makes it easier to mathematically prove that the code functions as intended?
http://www.google.com/search?client=safari&rls=en&q=...
Years ago, when I looked into it, an "operational" semantics hadn't been defined for Ada, but it seems that the modern language has a defined subset or profile.