<story><title>Some notes on Rust, mutable aliasing and formal verification</title><url>https://graydon2.dreamwidth.org/312681.html</url></story><parent_chain><item><author>Animats</author><text>That&amp;#x27;s a good article.&lt;p&gt;Having worked on program verification in the past, Rust looks like the most useful modern language to which formal methods can be applied. Rust&amp;#x27;s rules eliminate so many of the cases that are hard to formalize.&lt;p&gt;Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc&amp;#x2F;borrow sense. Those are somewhat equivalent. I&amp;#x27;d like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can&amp;#x27;t fail, you can eliminate most reference counts. That gives you free interior mutability when that&amp;#x27;s possible.&lt;p&gt;The author&amp;#x27;s comment on provers is interesting. The big problem with theorem provers is that they&amp;#x27;re developed by people who like to prove theorems. They&amp;#x27;re in love with the formalism. This leads to a UI disconnect with programmers.&lt;p&gt;You can knock off most things you have to prove with a SAT solver. But you&amp;#x27;ll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I&amp;#x27;ve been out of this for decades.&lt;p&gt;Machine learning may help in guiding theorem provers. Most programs aren&amp;#x27;t that original in terms of control flow and data usage. So inferring a proof plan from other code may work.
ML systems can&amp;#x27;t be trusted to &lt;i&gt;do&lt;/i&gt; the proof, but may take over guiding the process.</text></item></parent_chain><comment><author>nextaccountic</author><text>F* is this mythical language that proves stuff automatically (with an SMT solver, more powerful than SAT), but still lets you prove manually if the automated solver fails&lt;p&gt;The crypto routines in Firefox and Wireguard is actually written in F* (or more specifically Low&lt;i&gt;, a low level DSL embedded in F&lt;/i&gt;), not in Rust, and is fully verified&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;project-everest.github.io&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;project-everest.github.io&amp;#x2F;&lt;/a&gt;&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;mitls.org&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;mitls.org&amp;#x2F;&lt;/a&gt;</text></comment>
<story><title>Some notes on Rust, mutable aliasing and formal verification</title><url>https://graydon2.dreamwidth.org/312681.html</url></story><parent_chain><item><author>Animats</author><text>That&amp;#x27;s a good article.&lt;p&gt;Having worked on program verification in the past, Rust looks like the most useful modern language to which formal methods can be applied. Rust&amp;#x27;s rules eliminate so many of the cases that are hard to formalize.&lt;p&gt;Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc&amp;#x2F;borrow sense. Those are somewhat equivalent. I&amp;#x27;d like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can&amp;#x27;t fail, you can eliminate most reference counts. That gives you free interior mutability when that&amp;#x27;s possible.&lt;p&gt;The author&amp;#x27;s comment on provers is interesting. The big problem with theorem provers is that they&amp;#x27;re developed by people who like to prove theorems. They&amp;#x27;re in love with the formalism. This leads to a UI disconnect with programmers.&lt;p&gt;You can knock off most things you have to prove with a SAT solver. But you&amp;#x27;ll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I&amp;#x27;ve been out of this for decades.&lt;p&gt;Machine learning may help in guiding theorem provers. Most programs aren&amp;#x27;t that original in terms of control flow and data usage. So inferring a proof plan from other code may work.
ML systems can&amp;#x27;t be trusted to &lt;i&gt;do&lt;/i&gt; the proof, but may take over guiding the process.</text></item></parent_chain><comment><author>rtpg</author><text>I think that Coq&amp;#x2F;Agda&amp;#x2F;Lean and friends are really going to be the winners in the proof space. Interactivity is a pretty good model for the feedback loop, and they&amp;#x27;re systems that exist and work, without a lost of asterisks.&lt;p&gt;The biggest thing I think these tools are missing out of the box is, basically, &amp;quot;run quickcheck on my proof for me&amp;quot;. It&amp;#x27;s too easy to have some code, and try to prove some property that isn&amp;#x27;t true, and rip your hair out thinking &amp;quot;why can&amp;#x27;t I get the proof working!&amp;quot;&lt;p&gt;If halfway through your proof you end up in a thing that seems nonsensical, it would be nice for these tools to just have a &amp;quot;try to generate a counter-example from here&amp;quot; command that spits out a thing.&lt;p&gt;Proofs are so path-dependent, and it&amp;#x27;s not trivial to do in general. But I think they are all very close to greatness, and every time I&amp;#x27;ve gone through the effort to formally verify a thing, it&amp;#x27;s been pretty illuminating. Just... if you&amp;#x27;re trying to prove some code, the process should take into account the idea that your code might be buggy.</text></comment>