Ada does have useful things like a formal "denotational" semantics that make it easier than certain other languages.

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.