I have some sympathy for the idea that most modern software companies, especially VC-funded startups, tend to prioritize getting to market fast over making everything exactly right. I'm not even saying it's wrong for them and their market. But if we're looking for something that's well-designed and carefully tested before going to market, along with a process designed to produce that, this doesn't sound like it at all.
There should be ways of introducing new tech and features while slowly fading out the old ones however you don't switch from one to the other until it has been reasonably field tested.
One problem is they went to a defense contractor to build software instead of a software company.
I'm sure their software is great in their spy airplanes where it will never see the light of day and you can cover it up if it fails majorly however I wouldn't want it in the air traffic control computer.
That's not a problem. That's why it ever worked properly in the first place, let alone working correctly for 40 years. Why shouldn't your system last for 40 years?
FTA:
> Modernization, a struggle for any federal agency, is practically antithetical to the FAA's operational culture, which is risk-averse, methodical, and bureaucratic.
I don't understand the tone of this article. Risk-averse, methodical, bureaucratic.... that's exactly what I want them to be!!
Devil's advocate here:
Most software companies simply aren't up to the task. They're just not suited to building provable software from design through implementation often requiring the use of functional languages.
If you look at who does most aircraft software (or similar safety systems) it is mostly by certified engineers who just happen to "engineer" in software, rather than programmers who try to be engineers.
I'm a programmer, I am not ashamed of that. But realistically the way I work is in no way transferable to a safety critical system. In that situation every single function needs to have a unit test, it needs to have reliable input and output, and ideally it needs to self-identify hardware-caused undefined state and fail-safe.
I'm a programmer on a safety critical system. It doesn't require getting a PE, it requires a good quality system and a sizable amount of scorn towards the forces that want to reduce our profession to nothing more than a trendhopping slapdash self-congratulatory shitshow.
You also have to consider the compiler. Proving that your Haskell code is correct is largely pointless if you then compile it with a compiler that hasn't been proven correct. At a minimum that's going to mean compiling the code with a lot of the fancier optimizations turned off, which can lead to a rather severe degradation in performance in the case of a pure functional language.
My guess is that there are not currently any functional languages that (i) are significantly easier to formally verify than C or Ada, (ii) have predictable time and space behavior, and (iii) have implementations that are both extremely well-verified and reasonably performant.
A functional programming style or (almost) pure functional language would help to with (semi) automatic static code proofing.
Unless you are an engineer by accident, I would say you should be as prepared as you could be (albeit new to the field).
Honestly, the stance you share in this topic is why normal people historically has not seen computers and software as a reliable thing and continue to use half-assed software such as Windows for example.
But a bad example. Microsoft uses automatic proofing for their (and third party) device drivers. Windows NT series is very reliable and has one of the best OS designs. The Win32 subsystem and shell comes with a lot of legacy and is a different story.
Still a humongous undertaking, don't get me wrong. But at least it is a 5 year plan versus a 20-30 year plan which is the current thought plan as I see it.
* Don't bother, just let the planes fly wherever they want, but levy a fine when they crash.
* Put it out to tender every 5 years and fine commercial ATC operators when crashes occur.
Both of them shut the stable door after the horse has bolted, and would probably require them to operate at least a passive sort of ATC themselves in order to assess blame.
There's no conflict there.
Now NSA meant to keep US infrastructure safe, and attack US companies/people is a conflict. But the FAA being responsible for both safety and ATC is far from a conflict.
I'd prefer the FAA moved slowly and got it right. This isn't an area where young-hip 20 somethings re-invented the tech' in the latest web-2.0 fad. This is an area where you want mathematically provable correctness and unit testing up the ying-yang.
Get it right slow, don't get it wrong fast.