I've noticed several articles about Ada and Rust here on HN recently. Summarizing one comment I saw: Ada has a subset that is provable and certified as such, and Rust is close but not provable nor certified.