If you can't give an example of unsafety easily, that's already quite important. Compare to C, where one can provide such an example easily. If you want to write a mathematical prover, that won't hurt, though such tools don't need language support, lints and provers were written even for C.