You mean like Mariner I? "The post-flight review also showed that a missing hyphen (technically a bar in the variable r̄) in coded computer instructions in the data-editing program allowed transmission of incorrect guidance signals." https://www.edn.com/mariner-1-destroyed-due-to-code-error-ju...

Or Arianne 5[0]

Both had code reviews. Both catastrophically failed.

No I am not trying to draw causation that code reviewed software ends in tragedy :)

[0]: https://www.bugsnag.com/blog/bug-day-ariane-5-disaster

The Ariane software failure was slightly different because it only failed in the context of the differences in hardware between Ariane 1 and Ariane 5. It was perfectly valid code provided it was used within the constraints for which it was first designed. The Mariner code was simply wrong, and was destined to fail even under the conditions for which it was intended.

It's a subtle difference, but I think an important one, especially when considering the complexities for program proofs.

I'm sort of (not eagerly) awaiting the day when something written in Rust is implicated in a catastrophic failure. All the platitudes about safety and guarantees will smack hard against a wall like Wile E. Coyote in a Road Runner flick.