If unsafe is not used, then no one has to determine whether the unsafe parts are actually safe.

Sure, but taken to an extreme you see the absurd degree you have to contort yourself. And that’s to the current version of the proof checker - some unsafe’s are even only temporary until a better prover comes by.

You shouldn’t go out of your way to use unsafe, but between that and 2 weeks refactoring, I’ll take the unsafe and use tools like miri or ASAN to provide extra guards. Engineering is inherently about making practical choices.