Oh, yes, that's what the SPARK language does. There's also CodePeer, which does a static analysis of your Ada code. GNAT itself also does many static checks.
Oh please, the comparison of Ada to COBOL is invidious. Ada simply requires you to be explicit about your intent. This is a feature, not a flaw. You mean to say that you've never been burned by an implicit conversion in C, or a misplaced semi-colon? Ada is no less verbose than Java.
I am an Ada developer, but I think it is objective to say that anyone who opposes a language because there fingers will have extra work probably doesn't belong in this field. If you consider the development process as a whole—research, planning, development, verification, etc.—those extra keystrokes add an exceptionally marginal amount of time to the development process, but reduce time so much more by making the code more intuitive to read. Don't let me lead you to believe that Ada's words make it intuitive; that would be disingenuous, but the syntax has been formed since its inception to be readable by developers and non-developers alike. This is an important distinction with something like Java, neverminding that you don't have to explicitly instantiate generics in Java. One of the key objectives of Ada is code that is especially intuitive to non-developers. There's a lot going on in the language. I hope this helps.
Right. Also note that GNAT is just GCC. The most recent language standard is Ada 2012. (I was involved in the design of the Ada standard container library, which originally appeared in Ada 2005.)
Right, VHDL designed by the team at Intermetrics (which has also had a long association with Ada -- Ben Brosgol was the designer of the Red language that lost out to Green).
