That's not surprising, given that safety-critical software is very often programmed in Ada or SPARK.
I did a little bit of Ada programming, and one of the distinct features it has is you can't do anything clever without being extremely explicit about it. This language has the most aggressive type-correctness checking I have ever seen. When you finally get your code to compile, it's likely that it will work reliably.
I don't think Ada is that strict.
Also, at least back then, Ada has no garbage collection, so you know what latencies are.
It doesn't do any of the fancy/confusing inference stuff that Haskell does in order to verify that type conversions/transformations progress along the intended paths, but instead requires you to be very explicit about what you're doing.
E.g. (1) Trying to read something from stdin is a minor challenge, because of how Strings are usually fixed-length and don't interoperate with special arbitrary-length strings. (2) If you want to do dynamic memory stuff yourself, you need to declare your packages as such (with the intent of this showing up during reviews and thus leading to the code being more thoroughly scrutinized.) (3) It allows for creating special sub-types of primitives, like integers of a limited/well-speicified range, so that they can be put into APIs intead of ordinary machine/compiler-dependent integers. (4) Conditions (in IFs and such) don't (by default) short-circuit evaluate, and you have to use speical key words if you want short-circuit evaluation. And the list goes on..
All in all, Ada is quite enjoyable imho. It allows you to write code without thinking too much about it, since you won't be missing (many) corner cases.
On the other hand of course all of this results in more work, which can feel tedious to some - but at least it's not the mind-boggling "what is this *?!" strictness that has you pulling your hairs out in confusion/desperation, that usually accompanies Haskell.
No casting.
Probably rather alien to the HN crowd ;)
The only fully automated lines are 1 and 14.
First real success was Meteor line 14 driverless metro in Paris: Over 110 000 lines of B models were written, generating 86 000 lines of Ada. No bugs were detected after the proofs, neither at the functional validation, at the integration validation, at on-site test, nor since the metro lines operate (October 1998). The safety-critical software is still in version 1.0 in year 2007, without any bug detected so far.
From: http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf
|bool foo(bool i, bool j) {
2| return i ||
1| j;
|}
|
|void main() {
1| foo(true, false);
1| foo(false, false);
|}
But, for Avionics and Space System, Ada is a well known, and continues to be a well known implementation language.
On the other hand, failure is much less of an option when it comes to things like avionics, so much more focus is placed on reliability. In these cases that price starts looking like a bargain, if the use of Ada isn't already mandated (which it probably is).