The UB is the result of operations which assume invariants, when they are not met. Invariants are useless if you can't assume them. Having no UB in C would require having no way to break those assumptions but C is memory/type-unsafe so that's outright impossible.

Recently I've been trying to imagine what Rust's safe abstractions that use `unsafe` code internally would look like on top of some advanced mix of dependent type theory and proofs about state-manipulating imperative programs.

At that point, the optimizer would have proofs of the invariants it can rely on and it could even potentially emit proofs that every single transformation it performed preserves the (safe) semantics of the code being optimized.

But we're not there yet. Today, we need at least a small subset of the libraries of a systems language to prevent UB "by hand". And in C (or C++, although not necessarily for the same reasons), that's even harder, as there is no notion of a "safe abstraction" (one which you cannot misuse to produce UB).