While I have personally never programed life critical stuff, I interacted closely (on the algorithmic side) with people who did. This was in the railroad indust

While I have personally never programed life critical stuff, I interacted closely (on the algorithmic side) with people who did. This was in the railroad industry. They used a subset of C (no malloc...) and had a safety certified compiler. If you crash two trains because of a compiler bug at least you can pass the bunk. They did not use formal proof methods. The documentation was massive, substantially longer than the code, to the extent that doing the actual implementation from the documentation seemed relatively trivial. Writing and analyzing the documentation on the other hand... I had the impression that writing documentation to that level of detail must have taken substantially longer than implementing it directly in code. And this was probably a good thing as it forced people to think more about every details. Once a system was written it had to be certified. Any changes, no matter how trivial, meant you had to go through the whole certification process again: slow, painful and expensive.