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
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.
It doesn't panic within the code you typed, but it absolutely still can panic on OOM. Which is sort of the problem with "no panic"-style code in any language - you start hitting fundamental constructs that can can't be treated as infallible.
> Basically every practical language has some form of "this should never happen" root.
99% of "unrecoverable failures" like this, in pretty much every language, are because we treat memory allocation as infallible when it actually isn't. It feels like there is room in the language design space for one that treats allocation as a first-class construct, with suitable error-handling behaviour...
Assuming memory is infinite for the purposes of a program is a very reasonable assumption for the vast majority of programs. In the rare contexts where you need to deal with the allocation failure it comes at a great engineering cost.
It's not really what this is about IMV. The vast majority of unrecoverable errors are simply bugs.
A context free example many will be familiar with is a deadlock condition. The programmer's mental model of the program was incomplete or they were otherwise ignorant. You can't statically eliminate deadlocks in an arbitrary program without introducing more expensive problems. In practice programmers employ a variety of heuristics to avoid them and just fix the bugs when they are detected.
Deadlocks also don’t result in panics in most environments. The problem isn’t so much bugs - those can be found and fixed. The problem is more that no_panic in most languages implies no_alloc, and that eliminates most useful code
Trying to enforce no-panics without a proof system helping out is just not a very practical approach to programming. Consider code like
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
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.