> Who else is using formal methods or safety critical stacks like ADA/Spark?
This is not actually as common as many people seem to believe. The mandate died almost two decades ago. DOD aircraft fly on Fortran, JOVIAL, C, and C++ more than Ada. And DOD IT systems are a clusterfuck.
> It's one of the few sectors that still plan software upfront waterfall style
That's not the good thing you seem to think it is.
Also, why do you call it ADA? It's not an acronym. Amusingly, SPARK is, or was, and you write it as "Spark". It originally stood for "SPADE Ada Kernel" and the language continues to be stylized as SPARK.
Pedantics aside, not much reasoning against quality. Perhaps I've lucked out, but I've worked in many sectors and do not at all agree with sentiment here about DOD software quality. There is significant formal investment/research in DOD to improve operations, including taking the best of practices in commercial. In my experience, the worst of software is written by teams with little experience improvising under Agile and taking on tech debt with no time/resources to get things done the right way.
Can you point to a successful Waterfall project? A multi-million or billion dollar, 3+ year software development effort where a team figured out all the requirements correctly before writing a single line of code. Where they wrote every line of code correctly before testing it. And where testing was so spectacularly successful that they didn't have to go back and renegotiate the project requirements or dates to get extensions or reduced project scope.
If you can do this, then I might believe you about Waterfall being the best approach out there.
Right now your counter example is "teams with little experience" which is not much of an argument. Teams with little experience fail all the time, because they are inexperienced. Give them a $100 million Waterfall project to plan and execute over 3+ years and their failure would be even more spectacular.
> In my experience, the worst of software is written by teams with little experience improvising under Agile and taking on tech debt with no time/resources to get things done the right way.
Sounds like every DoD software project I've worked on for the past 5 years.
This is not actually as common as many people seem to believe. The mandate died almost two decades ago. DOD aircraft fly on Fortran, JOVIAL, C, and C++ more than Ada. And DOD IT systems are a clusterfuck.
> It's one of the few sectors that still plan software upfront waterfall style
That's not the good thing you seem to think it is.
Also, why do you call it ADA? It's not an acronym. Amusingly, SPARK is, or was, and you write it as "Spark". It originally stood for "SPADE Ada Kernel" and the language continues to be stylized as SPARK.