<story><title>Unsoundness in Pin</title><url>https://internals.rust-lang.org/t/unsoundness-in-pin/11311</url></story><parent_chain></parent_chain><comment><author>withoutboats</author><text>(I was the primary designer of the Pin API.)&lt;p&gt;Since (to a first approximation) every individual who has the expertise and contextual knowledge to really evaluate this issue is a poster on internals.rust-lang.org, its pretty surprising to find this thread on the front page of Hacker News. I imagine some Hacker News users who upvoted this link did so out of technical interest, but I suspect a large portion of the attention comes from some combination of these misconceptions:&lt;p&gt;- The misconception that this could have a practical impact on users (the code being discussed on the thread is all obviously pathological &amp;amp; contrived).&lt;p&gt;- The misconception that Rust&amp;#x27;s type system and standard library never contain soundness issues and that this is an exceptional event (in fact we have a number of longstanding soundness issues).&lt;p&gt;We have a policy of fixing all soundness issues, so this issue will be fixed. In the meantime, while we decide the best solution, it will have no practical impact on Rust users. And none of the solutions we are considering would involve significant breakage to users, or invalidate any real code.&lt;p&gt;At a high level: the soundness issue occurs because the Pin API was designed based on certain reasoning about the behavior of pointers. This reasoning would be sound but for the fact that we have allowed certain exceptions in relationship to pointers to what are called the &amp;quot;orphan rules&amp;quot; (which usually enable local reasoning like this). These exceptions allow users to introduce code which, while contrived, allows them to violate the guarantees of the Pin API. Such is life.</text></comment>
<story><title>Unsoundness in Pin</title><url>https://internals.rust-lang.org/t/unsoundness-in-pin/11311</url></story><parent_chain></parent_chain><comment><author>mauricioc</author><text>Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust&amp;#x27;s safety guarantees, showing that Peyton Jones&amp;#x27; guess was not accurate.&lt;p&gt;There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn&amp;#x27;t be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word &amp;quot;unclear&amp;quot;, as I believe all three options are valid and appeal to different use cases. Almost all of the popular languages don&amp;#x27;t care about this, for instance.)&lt;p&gt;[0] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;youtu.be&amp;#x2F;t0mhvd3-60Y?t=130&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;youtu.be&amp;#x2F;t0mhvd3-60Y?t=130&lt;/a&gt;
[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;plv.mpi-sws.org&amp;#x2F;rustbelt&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;plv.mpi-sws.org&amp;#x2F;rustbelt&amp;#x2F;&lt;/a&gt;</text></comment>