Then what would be a correct claim? Here are some equivalent formulations of an accurate description of the truth based on prior discussions:
- Safe code can cause UB outside its dependencies
- Safe code cannot cause UB in its dependencies
- Safe clients cannot cause UB (that's the formulation I used in the Rustonomicon)
Maybe you think about an orthogonal claim, namely that safe code cannot have UB. This claim is useful in the context of the type system (it defines what code must be unsafe), but it is useless in the context of verification (which this thread is about). What matters for verification is the location of the soundness bug, not the location of the UB. To review a program for soundness, you have to review safe code.
Or maybe you think that safe code means safe program? By safe code I mean a piece of code that doesn't contain an unsafe block, an unsafe impl, or an unsafe attribute, I don't mean a whole program (because then it would be just about the soundness of the type system, while here I'm talking about the encapsulation property of the type system, which Rust is only partially implementing by design).