That is trivially obvious, but writing a performant vector implementation is not solving the halting problem.

Let me restrict it to the faintly weaker "I hope we don't settle for unsafe being okay forever where we can prove safety".

You don't need to solve the halting problem just to verify an existing proof of a semantic property, nor to use smarter heuristics to avoid requiring such a proof. 100% safe is totally reachable, though I bet the syntax would be pretty hairy added to today's Rust.

Would need to get rid of C FFI, as that cannot be 'safe' in Rust?

Hmm, good point. You'd have to extend the formal verification into the C code, at least. If you can do that, it might be easier to just write verified C.

Inline ASM can't be verified either.

Inline ASM is exactly as verifiable as the underlying CPU, given an adequate model in the verifier. That's probably easier than verifying C, which introduces extra ambiguity in its semantics. But yeah, verifiable CPUs would be nice.