[Gaelan]

Generally, the idea is that you use a small amount of unsafe code to build a safe abstraction to do what you need, then use that abstraction in many places. So now you only have a few unsafe sections you have to verify for correctness, instead of the entire program like you'd need in C/C++.