Clifford Heath expounded in news:4e389b23$0$3035$ snipped-for-privacy@news.optusnet.com.au:
..
Ada is more than just a "good language". It is the software _engineer's_ language. It is very well thought out with an emphasis on engineering for correctness. Every language has a few design warts but Ada is really the only practical choice when code absolutely must work.
And the SPARK folks really do prove that their software is going to do what it is supposed to do. This is essential for air traffic control centers and fly by wire systems etc. They live with some pretty severe restrictions to do this- for example no dynamic memory allocation is permitted, since a memory request is potentially a failure point (it's also too difficult to prove that it will never fail).
In my own limited experience, every program I have ported from C or C++ to Ada has been shown by the _compiler_ to still have a subtle bug or two. This is at the _compiling_ stage, long before testing even begins. This is the best phase to discover problems.
One subtle case that sticks out in my memory was dealing with
16-bit integer sound samples. I forget now why it was necessary to invert the sample signal, but it was.The compiler dutifully pointed out that if the sample variable S when inverted as -S was problematic. It pointed out that if S was -32768 (16-bit signed) then -S is not representable as
+32768 and that an exception would be raised at run time were this allowed to happen.In the original C code -32768 gets inverted as -32768. So an incorrect value slips through the system in thousands of lines of code.
Of course a sharp programmer would catch this as it is being coded but no programmer is sharp all the time and never as sharp as the compiler for all details involved.
This example is not a serious error in sound sample code but it sure would be irritating- with the programmer wondering where on earth is that glitch coming from? Worse, the problem might be so rare that it goes unnoticed for a long time.
But in a life and death scenario, this kind of error is completely unacceptable.
Warren