I was really interested in this sort of stuff for a year or two, but ended up coming to the conclusion the best thing is to use tried-and-tested tools with rigorous standards/practices such as C/C++ than theoretically interesting tools like formally verified Haskell/Rust. It's just far more practical and there's something to be said about those boring tools used in the wild > academic creations.
I think my problem with writeups like these are that they attack the problem from the wrong (or uninteresting) angle. Like, say I'm writing software for an airplane then I'm gonna be chained to DO-178C. How will using Rust help me achieve all the objectives it requires for e.g. Level A? Is Rust gonna get me there cheaper (I think it might one day)? Is it gonna enable me to build systems that use constructs that I wouldn't have dared (due to complexity, safety or whatever)? Of course it's kind of hard to present this without a particular system design in mind (maybe it's PSAC for an abstract system I'm really after...). I suspect the situation is similar when getting some kind of security certification/accreditation (haven't seen much of that side of the coin). I'm not saying this project isn't valuable (it is), I just miss the top-down perspective of the language in this context. :)
Thank you for this perspective, it's one I'll try to incorporate more of in a future revision.
While the content aims to be generally applicable to a broad range of software, further contextualization against a specific standard like DO-178C might make for a valuable appendix section.
There's a bit of a balancing act, however, since Rust is, at present, not a certified choice for such use cases.
Well, in my experience it is possible to claim Level A despite not using a certified compiler. Perhaps not if you're building a civilian airliner and you're probably still gonna have to do some kind of activities to show what goes into the compiler comes out as expected. So although certification may be an ultimate goal, I don't think I'd consider it to be a complete showstopper when it comes to getting Rust airborne and keeping whatever it executes on so. :)
But you can avoid these by following best practices and using tools to find them. These are known knowns and there are solutions. The issue with Rust and others is that there are so many unknown unknowns, because it hasn't had the same number of hours of development time and usage.
Have you ever used a language like Haskell in a formal verification environment? You still get memory issues but there are far less tools to tackle them.
