But if you can manually identify an invariant inside an abstraction it can greatly improve performance for callers/users, additionally, tools like Kani use comprehensible macros to facilitate automatically proving safety of `unsafe` code. Not to mention built in linting, package management, docs, and FP that rust/std provides. Lots has been said about unsafe rust, but the most basic libc tools require the whole cascade of upstream callers to check safety, it's basically backwards from the ground up from a resources and an outcomes perspective.