> I don’t understand why Rust even has panics if its primary goal is safety. We should be able to prove that the code has no paths that may panic ever. I’ve been looking at this all week. It’s very difficult to make a program that is guaranteed not to panic.

The Rust-in-Linux folks are working on this with things like failable memory operations. It's required for their own use. Increased use of proof (such as proving that an array is non-empty) is also being slowly worked on.