I agree with you that my original message was sloppy, and also with your claim that full Rust has not been mechanically proven sound. But that is not the same

I agree with you that my original message was sloppy, and also with your claim that full Rust has not been mechanically proven sound. But that is not the same claim as “safe Rust can cause UB" If you are claiming the latter, please provide a minimal safe Rust program that causes UB without unsafe, FFI, proc-macro tricks, compiler bugs, or an unsound safe API implemented using unsafe? If you can produce such a program, of course you are right.