3 ms·
I completely agree with you safety should never be compromised just for the sake of modernization however when it takes 40 years to upgrade you're doing it wron
by Fuxy 12y ago
I completely agree with you safety should never be compromised just for the sake of modernization however when it takes 40 years to upgrade you're doing it wrong.
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.
- Someone1234 12y ago> One problem is they went to a defense contractor to build software instead of a software company. 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.
- forgottenpass 12y agoI'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. 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.
- 0xdeadbeefbabe 12y agoI'll guess that you don't use "provably correct" functional programming out of scorn for trendhopping etc. Am I right?
- frik 12y agoMost such critical software is written in Ada or C and run on an real time operating system. A functional programming style or (almost) pure functional language would help to with (semi) automatic static code proofing.
- foldr 12y agoIt's possible to prove the correctness of non-functional code too. It also tends to be much easier to reason about the time and space behavior of code written in, say, C. In a system with hard real time requirements that's very important. 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.
- viccuad 12y agoI studied CS, and mathematical software verification and functional languages where mandatory in my uni. 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.
- emodendroket 12y agoWindows, as it exists today, has stronger engineering and reliability than the vast majority of software on the market, despite being saddled with legacy baggage. You definitely could have chosen a better example.
- frik 12y agoTrue. 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.
- viccuad 12y agoThat's a bad example, true. In my defense I have to say that I jumped ship before NT, but I remember how people looked at NT's Blue Screen of Death(™) as if it were a normal thing to have in computers and software.
- nfoz 12y ago> One problem is they went to a defense contractor to build software instead of a software company. 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!!