We didn't formally verify the code, its way too complex, but everything was reviewed and heavily tested. And tested again. Then integrated and tested...
Ada is pretty strict and if it compiles you usually had some confidence it was going to at least run ok.
The industry was moving to C/C++ because developers know it and promises of higher productivity.
I did kinda grow to like ada. It had its warts, but it was good. It reminds me a bit of GO with its packages.
Ada Tasks also bear some semblance to goroutines. (In the sense that they share memory by communicating instead of communicating by sharing memory.)
It's definitely a nice and well-designed language IMO—with a share of annoyances[1] and flaws—but overall deserving of more attention than it gets. Lately I've gotten comfortable enough with it that I have been making a habit of reaching for Ada for side-projects where I would formerly use C. (For example, I'm writing a toy X window manager in Ada at the moment—using XCB from Ada is a little ugly at times but definitely bearable.)
1. For example, why can't a record discriminant be a range bound? Answer: standards committee didn't think people would use it. Of course, this means if you have an array of discriminated size, you can't conveniently have a type for a position in it. e.g.
type Thing_Stack (Max_Size : Positive) is record
Elements : array (Positive range 1 .. Max_Size) of Thing;
Top_Index : Positive range 0 .. Max_Size := 0; -- 0 = Empty stack
end record;
> This restriction is left over from Ada 83 (RM83 3.7.1(6)). We considered removing this restriction in Ada 95, but ultimately decided that the implementation effort to support this modest extension would outweigh the (more?) modest benefits. Perhaps a short-sighted decision, in retrospect...
> As for why the original Ada 83 restriction existed, noone knows for sure, but it probably relates to the historical purpose of discriminants as only for controlling the "shape" of the record, rather than being seen (as in Ada 95) as more general type "parameters."
And apparently it got left in Ada 2012 also.
(For C people, this is basically:
typedef struct {
size_t max_size, top_index;
thing elements[];
} thing_stack;
2. http://computer-programming-forum.com/44-ada/82b646ab38d529a...
I liked the records in ada. You could control the position and size of each field (which was really usefully for dealing with in binary messages) We had a ton of constrained types.
If I remember we has assert 'size on some of the records to make sure type changes didn't cause some records to become unexpected sized in case the types that made up the record changed.
variant records were fun, but when you start trying to do much (array of variant records?) it fell down.
The string handling left a little to be desired though..
Not that alien a comparison, since Ada and Go both descend from Niklaus Wirth's languages. Ada was directly based on Pascal, whereas Go (and its precursors) is strongly influenced by Modula and Oberon, themselves successors to Pascal. Aside from some superficial syntax differences, Go looks a lot like Modula and Oberon.
The slightly sarcastic answer would be "C++, of course". There is even a code standars document that's floating around. (Edit) Link: http://www.stroustrup.com/JSF-AV-rules.pdf
That said, I don't really think the troubles come from the technology side of things.
Please nobody tell them.
http://www.militaryaerospace.com/articles/2013/10/software-c... -- but a Google search reveals much the same from any article I can find, and just reiterates what I've read in past articles on F-35 software.
As the article states: “ALIS is the ground-based computer system meant to diagnose mechanical problems, order and track replacement parts, and guide maintenance crews through repairs. It also allows pilots to plan missions and later review their performance.”
https://www.csiac.org/wp-content/uploads/2016/02/2010_03_30_...
Boeing writes (nearly) everything in Ada and as far as I know has never had any software problems of this scale. Most of it is in SPARK as well, a restricted subset of Ada that can be partially formally verified[1]. Frankly, not formally verifying mission-critical software where a failure can potentially threaten someone's life seems rather irresponsible.
1. Contrary to what seems popular opinion, regular Ada is not particularly strict (less so than Rust). SPARK is very, very strict about what you can compile, and if it compiles it follows the spec (which is usually easier to audit).