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.
Author of the book here, thank you for your feedback!
Though not an Ada expert, I have used the SPARK subset. And I’ve worked on security assessment of military systems with components written in Ada. Although we looked at binaries and not source code, because our assurance model did not consider the Ada compiler to be part of the chain of trust (so we test the artifact the CPU will execute). I really like Ada and hope to use more of it in the future!
The HN community may be interested in this 1 hour presentation [1] on Nvidia's adoption of Ada, including why they chose it over Rust in 2019 (regulatory certification was one factor). There’s also a great academic paper [2] on the recent advances SPARK has made in heap memory verification, inspired in part by Rust’s type system.
There are currently efforts underway to certify Rust for usage in safety critical systems via an alternate, certified toolchain (among other pieces of the puzzle). Two related initiatives are linked through in FAQ question #7 (which someone already shared). I’ll be sure to add the Ferrous Systems and AdaCore collaboration when I have a chance to batch together some updates.
I, like many others, believe Rust is a technology that can deliver value in safety and mission critical verticals due to reduction in undefined behavior via principled static analysis (a type system for which there has been early success in formal verification of safety claims[3]). Looking forward to digging into Rust research tools for deductive verification in a later chapter(similar to SPARK - hand-written Hoare logic specifications, proven via SMT solving at compile-time).
We make comparisons to C and C++ in the book because they are the closest relatable analog for many developers. But I’m happy to add mention of Ada to not alienate potential readers like yourself, though my Ada knowledge is not currently deep enough to provide in-depth comparison.
This book is a best effort and an early-stage passion project. It strives to be technically accurate and data driven while remaining approachable to a range of readers. Like others have mentioned on this thread, this book does not claim to provide guidance for adherence with any particular standard or certification process. Although Chapter 3 does map concepts from MISRA C 2012 to Rust, in order to remain grounded in realistic, industry-adopted best practices.
The goal is to help readers build more secure and reliable software in general, to the furthest extent possible using entirely open-source tools. I look forward to iterating the content to meet high standards of quality, while keeping the entirety of the book freely available online.
Always open to critique and suggestions, thanks again!
Between the old-school hacker spirit and the short-form content, this is a real gem.