Well, you have to trust something... Silicone manufacturer, CPU designer, the OS, the compiler... But the big difference is, if I can do proofs and the compile

Well, you have to trust something... Silicone manufacturer, CPU designer, the OS, the compiler... But the big difference is, if I can do proofs and the compiler breaks my trust, that's a bug in the compiler. On the orher hand, Rust disallows complex proofs entirely, so I have to use unsafe code and trust random humans!