<story><title>The Rustonomicon: The Dark Arts of Advanced and Unsafe Rust</title><url>https://doc.rust-lang.org/nightly/nomicon/</url></story><parent_chain></parent_chain><comment><author>Animats</author><text>Interesting.  Other than interfaces to non-Rust code, the big safety issues revolve around partial allocation of arrays.  That&amp;#x27;s the machinery underneath the ability to grow a vector, and comes up with some other data structures.&lt;p&gt;It&amp;#x27;s not that hard to formalize safety in that area.  You need some way to talk about an array being partially initialized. This requires some simple design-by-contract machinery - object invariants, basically.  With some proof machinery, it should be possible to determine at compile time that a data manipulation is safe.&lt;p&gt;Rust already has the concept of raw memory space, which is treated as write-only.  That takes care of initialization for non-array types. Partially initialized arrays require some additional annotation.&lt;p&gt;Suppose we have a primitive for talking about initialization:&lt;p&gt;&lt;pre&gt;&lt;code&gt;    isvalid(T, arr, lo, hi)
&lt;/code&gt;&lt;/pre&gt;
This means that array &lt;i&gt;arr&lt;/i&gt; consists of valid values of type &lt;i&gt;T&lt;/i&gt; is initialized and valid for subscripts in the range &lt;i&gt;lo&lt;/i&gt; to &lt;i&gt;hi&lt;/i&gt; inclusive.&lt;p&gt;Now there&amp;#x27;s a way to talk about partially initialized arrays:&lt;p&gt;&lt;pre&gt;&lt;code&gt;    pub struct Vec&amp;lt;T&amp;gt; {
        ptr: *mut T,   &amp;#x2F;&amp;#x2F; oversimplifying here
        cap: usize,
        len: usize,
        invariant isvalid(T, *ptr, 0, len-1)
    }
&lt;/code&gt;&lt;/pre&gt;
This says that the array is only initialized up to len-1. The current requirement for &amp;quot;unsafe&amp;quot; comes from the lack of any way to talk about partial initialization.  It&amp;#x27;s an expressive problem.  Much of Rust&amp;#x27;s success comes from finding ways to talk about safety issues such as ownership within the language.  This is an extension to that.&lt;p&gt;Then, a minimal theorem prover is needed, one which at least knows these theorems:&lt;p&gt;&lt;pre&gt;&lt;code&gt;    j &amp;lt; i ==&amp;gt; isvalid(T, a, i, j) &amp;#x2F;&amp;#x2F; the null case
    isvalid(T, a, i, j) and k &amp;gt;= i and k &amp;lt;= j ==&amp;gt; isvalid(T, a[k]) &amp;#x2F;&amp;#x2F; element valid in range
    isvalid(T, a, i, j) and isvalid(T, a[j+1]) ==&amp;gt; isvalid(T, a, i, j+1) &amp;#x2F;&amp;#x2F; extend by adding new valid element
&lt;/code&gt;&lt;/pre&gt;
With that info, it&amp;#x27;s possible to check operations such as push, pop, and array growth, where an array is partially initialized in a controlled way.  Array references can also be checked; this implies that access to an element index &amp;gt;= len is an error, and the compiler now knows this.&lt;p&gt;When the compiler knows something like that, it can optimize.  If you&amp;#x27;re iterating a vec, from 0 to len-1, the subscript check required is&lt;p&gt;&lt;pre&gt;&lt;code&gt;   i &amp;lt; len
&lt;/code&gt;&lt;/pre&gt;
Within a FOR statement, the compiler already knows the range of i is within 0..len-1,
so the subscript check becomes&lt;p&gt;&lt;pre&gt;&lt;code&gt;   len-1 &amp;lt; len
&lt;/code&gt;&lt;/pre&gt;
which simplifies to True, eliminating the subscript check.  That gets rid of the need for most unchecked subscripting.&lt;p&gt;This sort of proof machinery used to be exotic technology.  (I was doing this kind of thing 35 years ago.[1]) Now it&amp;#x27;s well understood.  It&amp;#x27;s quite possible to do this in a compiler today.&lt;p&gt;[1] &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&lt;/a&gt;</text></comment>
<story><title>The Rustonomicon: The Dark Arts of Advanced and Unsafe Rust</title><url>https://doc.rust-lang.org/nightly/nomicon/</url></story><parent_chain></parent_chain><comment><author>noobymatze</author><text>Am I right in assuming, that the name is a reference to the Normanomicon from Fable II and Fable III? It&amp;#x27;s just priceless.&lt;p&gt;Thanks to all involved with Rust (also in light of the 1.3 release). From what I can tell (passively reading about language decisions and seeing the responsiveness of all involved on various communication channels), it&amp;#x27;s a great lesson in building a community while simultaneously creating a fun programming language.&lt;p&gt;I hope, I&amp;#x27;ll come to use it at work at some point.&lt;p&gt;P.S. First comment ever on the internet anywhere, hope I didn&amp;#x27;t violate any guidelines.</text></comment>