"But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. " I thought that these worries about unsafe code in Rust indicated p

"But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. " I thought that these worries about unsafe code in Rust indicated people wanted a way to ensure it's as safd as possible. Traditionally, unsafety the language itself cant handle is dealt with via external tools for analysis, proving, and testing. These exist for unsafe code in Ada, C, C+×, Java, and SPARK. Tool-assisted, subsets of each are deployed in safety-critical industries. Anyone doing unsafe codd in them will get more robustness than unsafe code in Rust. So, you already have protection measures in safe Rust. Other tools, esp SPARK Ada and C enhancements, have them for unsafe code that Rust does nothing to protect. That's a gap in capabilities Rust needs to close. Until then, it's on the table when choosing which to use for unsafe code. Note that Im also a big fan of mixing and matching where we used the C or SPARK provers on unsafe Rust coded to be semantically equivalent. I just know most will prefer Rust to handle this itself. "By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P" Haha. I do plan to learn it for my Brute Force Assurance concept. Remember I have a brain injury, though, that knocked out memory and good chunk of learning pace on top of full-time job. That plus a shit-ton of broad R&D leaves little time for coding.