Coq is great. Now the problem is developers having the sharpest, greatest tools but not understanding the spec, or working to a stupid spec and not calling it out.
I've done security auditing of ADA and C avionics code. (including for DAL-A components). As a language, I'd take Rust any day (in terms of security/robustness properties).
However, the rust/LLVM compiler pipeline is nowhere near mature enough for use in high-criticality environments.
> However, the rust/LLVM compiler pipeline is nowhere near mature enough for use in high-criticality environments.
I don't know about Rust, but LLVM isn't mature? Nearly ever program running in the Apple ecosystem was compiled using LLVM. Swift is compiled using LLVM. Since Xcode 4.2, Clang is the default compiler. So iOS and macOS apps are built with LLVM. I'd also wager a guess that Apple uses Clang to compile key system code (Darwin, macOS, and iOS, etc) as well.
Not mission-critical, must-never-fail mature, no. All of these systems contain tens (if not thousands of bugs), some of these probably come from compiler issues sometimes.
At least a lot of it was due to having to specify around the weird quirks of existing compiler implementations. C has far more undefined behavior than it needs for optimization, and modern programming language theory and compiler research has shown that most undefined behavior isn't really necessary at all. [0] For example, safe Rust has extremely close (and sometimes superior) performance to C, and has almost* no undefined behavior at all. [1]
* Some is inherited from LLVM, some is bugs, some is dumb corner cases like using kernel syscalls to overwrite the program's own memory with random bits.
Name one example where UB is necessary for useful optimizations where simply having unspecified values or platform dependent behavior wouldn't be enough.
MacOS and related don't run the airplane. Pilots have an iPad for some checklists and other things where "have you tried turning it off and on again" works as failure prcedure. If a failure, caused by a compiler bug leading to an overflow in a rare flight situation, happens on an airplane system a reboot is not really the option you want to depend on.
That might work in a stable situation - many (not all) planes are good gliders. (I.e. somewhere I read that the A380 is a quite good glider, among other reasons since the wings were designed for larger versions; an F-16 however won't really glide)
In a critical situation this is impossible, though.
That will not always work very well, inertial navigation systems often wants to be completely still for a couple of minutes to calibrate themselves.
I have heard about just flying with no G-load for a while and getting some basic instruments working. But I dont think you will get full nav functionality back.
I write software for in cockpit ipad apps - they are becoming more and more integral to the workload of pilots, everything from route planning, guidance, checklists, manifests and ordering fuel.
There was actually an incident posted on HN a while ago where IIRC an ipad did a software update or similar at a critical moment, and caused complications bad enough to get an incident report published on some aviation agency's website.
> However, the rust/LLVM compiler pipeline is nowhere near mature enough for use in high-criticality environments.
I love Rust, but I wouldn't want it to fly a plane I'm on. For instance, here's a bug in LLVM that Rust developers happened to discover - before they disabled their use of the buggy features, Rust/LLVM was producing _numerically incorrect_ code. https://github.com/rust-lang/rust/issues/54878#issuecomment-...
I'd take a compiler backend that compiles large parts of the modern software ecosystem every day and has countless programmers using it over some niche compiler that is used only for a vanishing fraction of all applications but boasts some kind of official stamp of applicability in safety relevant contexts.
I'm not so sure I would. For one, Ada is in no way a niche language. For two, C (and C++ by extension) simply were not designed with safety or reliability in mind. I happen to think that it's fair to say that they weren't designed at all, in that C compilers existed before the first language specification, and the language specification was forced to accommodate their quirks. Cargo culting about C is fine and all, but it often leads to absurd claims that it is more suitable in any arbitrary domain than languages and compilers designed specifically for the domain.
I think I'd prefer that safety-critical code be written in languages that don't allow pointer arithmetic except in scenarios that can be proved via static analysis not to introduce multiple memory aliases. Expecting program writers and compiler authors to get these sorts of things right in C/C++ is just unreasonable.
I'd argue that you would probably never find a bug such as that in a certified compiler, not because of the certification, but because far, far fewer eyes look at its output. I have worked in safety critical software and used a certified compiler. It had enough bugs that I personally found four in my first year.
Isn't ADA required? I worked with Air Force C2 platforms for east European NATO programs and the systems I was working with (one was called ASOC) was, at it's core, ADA. We also had civilian ATC in our facility and a few of those devs played on our softball team all writing ADA as well. But, it was part of the design spec and non-negotiable per FAA, Air Force, etc as far as I remember.
reply