Rust: Beyond the Typechecker

This has been done so many times.<p>The Stanford Pascal Verifier was probably the first[1] The Pascal-F Verifier, a project I headed around 1980,[2][3] used preconditions and postconditions very similar to what this guy is doing in Rust. &quot;Specifically, full functional correctness with properties like arithmetic correctness, in-bounds array accesses, state machines correctness, functional correctness with respect to an abstract specification or security properties.&quot; - we had all that in 1983. Look at the example starting at page 56 in [2].<p>DEC did a lot of work on this for Modula, and later Java, in the late 1980s.[4] Modula went down with DEC. The work was mostly lost. Dafny is probably the most modern system in this line.<p>Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C.<p>The &quot;array is a pointer&quot; mindset of C set programming back by <i>decades</i>. In Pascal, <i>there were no buffer overflows</i>. Pascal, Modula, Ada, and on to Rust - no buffer overflows. Everything carried along size information. Subscript checking optimizations had been figured out by the 1980s, so the performance penalty was coming down.<p>The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It&#x27;s hard to find.) Massive amounts of effort are being applied to try to infer information that C just can&#x27;t express. This would be a lot more worthwhile if it resulted in translation of C to something better.<p>Forty years, and this <i>still</i> isn&#x27;t fixed.<p>[1] <a href="http:&#x2F;&#x2F;i.stanford.edu&#x2F;pub&#x2F;cstr&#x2F;reports&#x2F;cs&#x2F;tr&#x2F;79&#x2F;731&#x2F;CS-TR-79-731.pdf" rel="nofollow">http:&#x2F;&#x2F;i.stanford.edu&#x2F;pub&#x2F;cstr&#x2F;reports&#x2F;cs&#x2F;tr&#x2F;79&#x2F;731&#x2F;CS-TR-79...</a> [2] <a href="http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf" rel="nofollow">http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf</a> [3] <a href="https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;pasv" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;pasv</a> [4] <a href="https:&#x2F;&#x2F;link.springer.com&#x2F;content&#x2F;pdf&#x2F;10.1007&#x2F;BFb0026441.pdf" rel="nofollow">https:&#x2F;&#x2F;link.springer.com&#x2F;content&#x2F;pdf&#x2F;10.1007&#x2F;BFb0026441.pdf</a>

Here&#x27;s the Servo pull request that came from formal verification of Rust code:<p><a href="https:&#x2F;&#x2F;github.com&#x2F;servo&#x2F;servo&#x2F;pull&#x2F;22458" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;servo&#x2F;servo&#x2F;pull&#x2F;22458</a>

The example given with the `Point` struct is interesting. As a self taught developer with admittedly little language design knowledge, it almost seems like unit tests without all of the boiler plate.<p>For instance, the `is_diagonal` function provided as the &quot;correctness checker&quot; looks to me like something that would be in a unit test for the `double` function. However, I think it goes a little bit deeper than that. In a unit test, you are somewhat required to pass specific values to the constructs you are testing. The given example is more complete than a unit test in that it doesn&#x27;t just test for the correct value being produced by the `double` function when given specific values, it actually checks all possible outcomes by asserting that the `double` function always produces a `Point` where `p.x == p.y`.<p>Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.

My biggest wish for Rust right now is dependent types, I find myself wanting them in almost everything I write to ensure it is correct for all possible inputs. It could also improve performance eliminating out of bounds checks in many places.<p>I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.

I&#x27;m surprised there is no name dropping of `Hoare logic&#x27; here or in the article so i&#x27;m gonna do it. Hoare logic is made of triplets (precondition, command, postcondition). A whole bunch of things are based on that. To go further one can also search about separation logic which adds an account for abstract memory locations into hoare logic.<p>But actually i must say i&#x27;m not very fond of these kind of approaches. As is rightly made explicit in the post, a lot of nice properties of Rust come from it&#x27;s type system. A type system is a way to annotate usual programming constructs with additional infos (types) together with a decidable procedure for testing whether or not a particular program is well-typed. And then we provide several key lemmas asserting that all well-typed program enjoy such and such property. On the other hand, program verification is a different beast: you annotate parts of your program with some form of specification (hoare triplets and the like) and then you try to solve the (in most case undecidable) problem of coming up with proofs that your program satisfies the specifications you gave.<p>The approach is very different: on one hand you restrict (maybe severely) the programs so that you can decide whether or not some properties hold, on the other hand you (mostly) don&#x27;t restrict the programs and you hope to give enough hints so that the solver doesn&#x27;t get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust&#x2F;reliable&#x2F;simple whereas verification is a black-box which isn&#x27;t easy to understand and thus never feels very &quot;principled&quot;. Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent.<p>My 2cts... Anyway i&#x27;m not saying i think this project is useless or anything, most systems actually live somewhere between bottom-up and top-down, ideas from one side may help the other, and deductive verification may arguably be much more bottom-up than other verification techniques (all flavors of model checking, abstract interpretation etc).

Code-level specifications (sometimes called contracts) that can be verified by various means (including manual deductive proofs, and automated solvers) exist for mainstream programming languages. The most mature ones are probably JML for Java (verified with <a href="https:&#x2F;&#x2F;www.openjml.org&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.openjml.org&#x2F;</a> and various other tools) and ACSL for C (verified with <a href="https:&#x2F;&#x2F;frama-c.com&#x2F;" rel="nofollow">https:&#x2F;&#x2F;frama-c.com&#x2F;</a>). C# has Spec#, but I&#x27;m not sure it&#x27;s still used.<p>It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it&#x27;s unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.

I found this case study by the author, linked from the article, more interesting: <a href="https:&#x2F;&#x2F;blog.merigoux.ovh&#x2F;en&#x2F;2019&#x2F;04&#x2F;16&#x2F;textinput.html" rel="nofollow">https:&#x2F;&#x2F;blog.merigoux.ovh&#x2F;en&#x2F;2019&#x2F;04&#x2F;16&#x2F;textinput.html</a>

Looking at examples of syntax for pre&#x2F;post-conditions and invariants, it&#x27;s all Rust expressions inside strings. Is there no other way for an attribute to have some associated inline code? Strings are not optimal for this, because they break tooling (syntax highlighting, code completion and navigation, refactoring etc).

There&#x27;s actually already a library that does what the author is talking about: <a href="https:&#x2F;&#x2F;github.com&#x2F;nrc&#x2F;libhoare" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;nrc&#x2F;libhoare</a><p>They call it &quot;design by contract&quot; rather than &quot;deductive verification&quot; though.<p>Wish there wouldn&#x27;t be so many terms for the same thing.<p>edit: There&#x27;s also an existing RFC for this: <a href="https:&#x2F;&#x2F;github.com&#x2F;rust-lang&#x2F;rfcs&#x2F;issues&#x2F;1077" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;rust-lang&#x2F;rfcs&#x2F;issues&#x2F;1077</a>

<p><pre><code> Why doesn’t this category of bugs exist for Rust programs? Simply because you cannot write a program that contains a null-pointer error. </code></pre> Hate to be <i>that guy,</i> but this is strictly not true. Observe:<p><pre><code> $ nl -ba nulltmp.rs 1 use std::ptr; 2 3 fn main() { 4 unsafe { 5 let p = ptr::null::&lt;i64&gt;(); 6 println!(&quot;{}&quot;, *p); 7 } 8 } $ rustc nulltmp.rs $ .&#x2F;nulltmp Segmentation fault (core dumped) </code></pre> Raw pointers exist. Unsafe Rust exists. Any large enough Rust project will end up with some unsafe code. That doesn&#x27;t mean that the things OP is doing aren&#x27;t great—they are—but merely that, when considering tools to be used for real-world Rust, people shouldn&#x27;t assume that their tools will only be used in a shiny rainbow unicorn world of Safe Rust.