Rust doesn't want to add any proof-system that isn't 100% repeatable, reliable, and forwards compatible to the language. The borrow checker is ok, because it meets those requirements. The optimizer based "no panic" proof system is not. It
will break between releases as LLVM optimizations change, and there's no way to avoid it.
Trying to enforce no-panics without a proof system helping out is just not a very practical approach to programming. Consider code like
some_queue.push_back("new_value");
process(some_queue.pop_front().unwrap());
This code is obviously correct. It never panics. There's no better way to write it. The optimizer will instantly see that and remove the panicing branch. The language itself doesn't want to be in the business of trying to see things like that.
Or consider code like
let mut count: usize = 0;
for item in some_vec {
// Do some stuff with item
if some_cond() {
count += 1;
}
}
This code never panics. Integer arithmetic contains a hidden panic path on overflow, but that can't occur here because the length of a vector is always less than usize::MAX.
Or so on.
Basically every practical language has some form of "this should never happen" root. Rust's is panics. C's is undefined behavior. Java's is exceptions.
Finally consider that this same mechanism is used for things like stack overflows, which can't be statically guaranteed to not occur short of rejecting recursion and knowledge of the runtime environment that rustc does not have.
---
Proof systems on top of rust like creusot or kani do tend to try to prove the absence of panics, because they don't have the same compunctions about not approving code today that they aren't absolutely sure they will approve tomorrow as well.