I imagine in that line of work, SW must consist of like 99% sageguards and checks of various kinds. Like rather double-check the thing the compiler already proved at runtime than discovering a rare compiler bug in 10 years during a complex oribital descent maneuver…