<p><pre><code>    The scope of unsafe ends at the next abstraction boundary. This means that 
    everything outside of the std::vec module does not have to worry about Vec.
    ...
    Of course, this also means that everything inside std::vec is potentially 
    dangerous and needs to be proven to respect the semantics of Vec.
</code></pre>
So wait, in a nutshell, a module is &#x27;safe&#x27; if and only if you formally prove that every public interface into the module and every way that public interface can be invoked... is error free.<p>How is that any improvement on any other language?<p>If the burden of &#x27;safety&#x27; is formal proof of <i>the entire module</i>, then you&#x27;re (surely) no better off than using C++ and doing exactly the same thing.<p>I mean, obviously the borrow checker can help to some extent, but what you&#x27;re basically saying is that it&#x27;s not enough; you can&#x27;t trust the borrow checker for safety; you <i>must</i> formally verify a module in order to know it&#x27;s safe, if it contains any unsafe code.<p>In other words, if your rust program has <i>any module</i> in <i>any dependency</i> that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a &#x27;safe&#x27; function that has not be formally verified to be safe, and results in undefined behaviour despite being safe).<p>That&#x27;s quite a troubling conclusion.