Earlier quoted context omitted.
I find it interesting that such critical code is written in C. Why not use something with a lot more (easily)statically provable properties. Like Rust or Agda?
You’ll find that for very serious, industrial applications, a conservative mindset prevails. C may not be trendy at the moment, but it powers the computing world. Its shortcomings are also extremely well known and also statically analyzable. Also, think about when flight software started being written. Was Rust an option? And once it came out, do you expect that programmers who are responsible for millions of people’…
Nuclear reactors?