> Second, Rust by now has an extensive tradition of people discussing memory safety invariants, what soundness means, formal models of what is a valid memory access

Rust is still lacking a definitive formal model of "soundness" in unsafe code. I'm not sure why you're suggesting that this is not a valid criticism or remark, it's just a fact.