14 ms·

Rust: Beyond the Typechecker

273 points by UkiahSmith 8y ago

ChrisSD 8y ago
Here's the Servo pull request that came from formal verification of Rust code: https://github.com/servo/servo/pull/22458 https://github.com/servo/servo/pull/22458
- gpm 8y ago
  And it looks like the annotated rust code (with commented out invariants) and f* code for that example can be found here: https://github.com/denismerigoux/rox-star/blob/master/textinput/ https://github.com/denismerigoux/rox-star/blob/master/textin...
scriptkiddy 8y ago
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. For instance, the `is_diagonal` function provided as the "correctness checker" 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'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`. Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.
- pjc50 8y ago
  There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
  - seanwilson 8y ago
    > There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones. Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
    - draw_down 8y ago
      The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
      - seanwilson 7y ago
        > The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
      - giornogiovanna 7y ago
        The simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
- _Codemonkeyism 8y ago
  Something in between what you describe and what the article does with F* would be Haskell QuickCheck or Scala ScalaCheck [1] testing where the framework determines the test parameters for your tests. [1] https://www.scalacheck.org/ https://www.scalacheck.org/
- ChrisSD 8y ago
  Does the linked case study[0] help at all? It's real code that already had debug assertions that acted as a postcondition. It was than formally proved that those conditions held (or didn't hold in one case) for all the relevant functions. [0] https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html
  - scriptkiddy 8y ago
    It does help. what I find interesting here is that the prover was able to find a potential bug that the test cases were not able to find. That's powerful.
- rotcev 8y ago
  You might be interested in clojure.spec [1] too :) [1] https://clojure.org/guides/spec https://clojure.org/guides/spec
- max76 8y ago
  The rust compiler will help you avoid a lot of common runtime errors. It comes at a cost of extra development time. The Rust philosophy values code correctness over developer efficiency.
  - im_down_w_otp 8y ago
    I'm confused by this sentiment. How efficient is a developer when producing things that are incorrect? Unless the goal is produce incorrect things, which seems unlikely. It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
    - swsieber 8y ago
      There are many times where you don't need 100% correctness (e.g. prototypes, or edge cases that in practice are never hit) - I'd say it might be more accurate to say that Rust makes it harder/less convenient to take out technical debt. I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old. You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
      - melling 8y ago
        I think we're talking about typing time, right? Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write. If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
        learc83 8y ago
        No, no one is talking about typing time--well at least not just typing time.
        bluGill 8y ago
- int_19h 7y ago
  Look up "design by contract" for more background on these. I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
  - nemlog 7y ago
    Design by Contract (DbC) was seamlessly embedded into the Eiffel Language and Method right from the start, way back in 1986. The ideas gained by using Eiffel and Design by Contract can be formative and help us in our approach to using other languages. The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published .. AutoReq: Expressing and verifying requirements for control systems https://www.sciencedirect.com/science/article/pii/S1045926X18301514?dgcid=author https://www.sciencedirect.com/science/article/pii/S1045926X1...
mavelikara 8y ago
I found this case study by the author, linked from the article, more interesting: https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html
pron 8y ago
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 https://www.openjml.org/ https://www.openjml.org/ and various other tools) and ACSL for C (verified with https://frama-c.com/ https://frama-c.com/). C# has Spec#, but I'm not sure it's still used. It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.
- garethrowlands 8y ago
  Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`. Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-basic.html https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
  - pron 7y ago
    The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).
Datenstrom 8y ago
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. I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.
- 0815test 8y ago
  Not very likely so far. Adding dependent types to the sort of uniqueness- and 'lifetime'/region-based typing that's used in Rust is very much a matter of research.
- steveklabnik 8y ago
  We had an RFC for Pi types [1] but in the ended, decided it was too much, too soon [2]. The "const generics" RFC [3] adds a minimal, forward-compatible from of this, and is on track to land this year. 1: https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 2: https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268915104 https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268... and https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304105162 https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304... 3: https://github.com/rust-lang/rfcs/blob/master/text/2000-const-generics.md https://github.com/rust-lang/rfcs/blob/master/text/2000-cons... We may or may not end up with them someday, but we need experience with RFC 2000 first.
  - tomjakubowski 7y ago
    Holy crow! As someone who remembers when the rust-lang/rfcs repo was created, I can't believe we're over 2000 RFCs submitted!
    - steveklabnik 7y ago
      Issues and PRs are the same thing in GitHub internals, and the RFC number is the PR number. There haven’t been 2000 accepted PRs :)
Animats 8y ago
This has been done so many times. 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. "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." - we had all that in 1983. Look at the example starting at page 56 in [2]. 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. Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C. The "array is a pointer" mindset of C set programming back by decades. In Pascal, there were no buffer overflows. 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. The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It's hard to find.) Massive amounts of effort are being applied to try to infer information that C just can't express. This would be a lot more worthwhile if it resulted in translation of C to something better. Forty years, and this still isn't fixed. [1] http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79-731.pdf http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79... [2] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv [4] https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf
- skywhopper 8y ago
  Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial software, and you end up with a provably correct piece of software that is still full of business logic bugs and which inevitably fails to keep up with ever-changing business processes. I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.
ainar-g 7y ago
Why doesn’t this category of bugs exist for Rust programs? Simply because you cannot write a program that contains a null-pointer error. Hate to be that guy, but this is strictly not true. Observe: $ nl -ba nulltmp.rs 1 use std::ptr; 2 3 fn main() { 4 unsafe { 5 let p = ptr::null::<i64>(); 6 println!("{}", *p); 7 } 8 } $ rustc nulltmp.rs $ ./nulltmp Segmentation fault (core dumped) Raw pointers exist. Unsafe Rust exists. Any large enough Rust project will end up with some unsafe code. That doesn't mean that the things OP is doing aren't great—they are—but merely that, when considering tools to be used for real-world Rust, people shouldn't assume that their tools will only be used in a shiny rainbow unicorn world of Safe Rust.
- int_19h 7y ago
  The article mentions unsafe more than once, and specifically says: "I do not intend to tackle the difficult problem of interaction between unsafe and safe Rust code; Rustbelt is the correct way to do it." The statement you quoted is clearly in the implied context of safe code.
- Dylan16807 7y ago
  > Hate to be that guy Clearly you don't.
int_19h 7y ago
Looking at examples of syntax for pre/post-conditions and invariants, it'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).
- steveklabnik 7y ago
  Until the release Thursday, it was not. As of the last release, it now is. This was probably written before that was available generally.
  - int_19h 7y ago
    Thanks! For the curious, more details here: https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custom-attributes-accept-arbitrary-token-streams https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custo... From tooling perspective, this isn't perfect, because there's still no guarantee that the token stream is a valid expression. So e.g. an IDE trying to highlight them or do a global rename refactor has to assume, which might not always be correct for token-based DSLs. It would be nice to have some metadata to distinguish those. Or perhaps there is an idiomatic way to express it in a contract on the macro itself, that tools could look at?
    - steveklabnik 7y ago
      Not sure, to be honest.
lapinot 7y ago
I'm surprised there is no name dropping of `Hoare logic' here or in the article so i'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. But actually i must say i'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'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. 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't restrict the programs and you hope to give enough hints so that the solver doesn't get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust/reliable/simple whereas verification is a black-box which isn't easy to understand and thus never feels very "principled". Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent. My 2cts... Anyway i'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).
kaiby 7y ago
There's actually already a library that does what the author is talking about: https://github.com/nrc/libhoare https://github.com/nrc/libhoare They call it "design by contract" rather than "deductive verification" though. Wish there wouldn't be so many terms for the same thing. edit: There's also an existing RFC for this: https://github.com/rust-lang/rfcs/issues/1077 https://github.com/rust-lang/rfcs/issues/1077
- rrobukef 7y ago
  Deductive verification is a large extension of designing by contract: The addition of a SMT solver to verify the contracts at compile time for instance. On the other hand libhoare only adds the contracts as a runtime addition with no mention of formally verifying these. The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet." This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816 https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.
pacemaker 7y ago
If you build Pacemakers see me - Pacemakers.com - lol

273 points by UkiahSmith 8y ago

Here's the Servo pull request that came from formal verification of Rust code: https://github.com/servo/servo/pull/22458 https://github.com/servo/servo/pull/22458

gpm 8y ago
And it looks like the annotated rust code (with commented out invariants) and f* code for that example can be found here: https://github.com/denismerigoux/rox-star/blob/master/textinput/ https://github.com/denismerigoux/rox-star/blob/master/textin...

scriptkiddy 8y ago

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. For instance, the `is_diagonal` function provided as the "correctness checker" 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'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`. Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.

pjc50 8y ago
There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
- seanwilson 8y ago
  > There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones. Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
  - draw_down 8y ago
    The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
    - seanwilson 7y ago
      > The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
    - giornogiovanna 7y ago
      The simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
_Codemonkeyism 8y ago
Something in between what you describe and what the article does with F* would be Haskell QuickCheck or Scala ScalaCheck [1] testing where the framework determines the test parameters for your tests. [1] https://www.scalacheck.org/ https://www.scalacheck.org/
ChrisSD 8y ago
Does the linked case study[0] help at all? It's real code that already had debug assertions that acted as a postcondition. It was than formally proved that those conditions held (or didn't hold in one case) for all the relevant functions. [0] https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html
- scriptkiddy 8y ago
  It does help. what I find interesting here is that the prover was able to find a potential bug that the test cases were not able to find. That's powerful.
rotcev 8y ago
You might be interested in clojure.spec [1] too :) [1] https://clojure.org/guides/spec https://clojure.org/guides/spec
max76 8y ago
The rust compiler will help you avoid a lot of common runtime errors. It comes at a cost of extra development time. The Rust philosophy values code correctness over developer efficiency.
- im_down_w_otp 8y ago
  I'm confused by this sentiment. How efficient is a developer when producing things that are incorrect? Unless the goal is produce incorrect things, which seems unlikely. It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
  - swsieber 8y ago
    There are many times where you don't need 100% correctness (e.g. prototypes, or edge cases that in practice are never hit) - I'd say it might be more accurate to say that Rust makes it harder/less convenient to take out technical debt. I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old. You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
    - melling 8y ago
      I think we're talking about typing time, right? Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write. If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
      - learc83 8y ago
        No, no one is talking about typing time--well at least not just typing time.
      - bluGill 8y ago
int_19h 7y ago
Look up "design by contract" for more background on these. I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
- nemlog 7y ago
  Design by Contract (DbC) was seamlessly embedded into the Eiffel Language and Method right from the start, way back in 1986. The ideas gained by using Eiffel and Design by Contract can be formative and help us in our approach to using other languages. The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published .. AutoReq: Expressing and verifying requirements for control systems https://www.sciencedirect.com/science/article/pii/S1045926X18301514?dgcid=author https://www.sciencedirect.com/science/article/pii/S1045926X1...

mavelikara 8y ago

I found this case study by the author, linked from the article, more interesting: https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html

pron 8y ago

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 https://www.openjml.org/ https://www.openjml.org/ and various other tools) and ACSL for C (verified with https://frama-c.com/ https://frama-c.com/). C# has Spec#, but I'm not sure it's still used. It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.

garethrowlands 8y ago
Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`. Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-basic.html https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
- pron 7y ago
  The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).

Datenstrom 8y ago

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. I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.

0815test 8y ago
Not very likely so far. Adding dependent types to the sort of uniqueness- and 'lifetime'/region-based typing that's used in Rust is very much a matter of research.
steveklabnik 8y ago
We had an RFC for Pi types [1] but in the ended, decided it was too much, too soon [2]. The "const generics" RFC [3] adds a minimal, forward-compatible from of this, and is on track to land this year. 1: https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 2: https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268915104 https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268... and https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304105162 https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304... 3: https://github.com/rust-lang/rfcs/blob/master/text/2000-const-generics.md https://github.com/rust-lang/rfcs/blob/master/text/2000-cons... We may or may not end up with them someday, but we need experience with RFC 2000 first.
- tomjakubowski 7y ago
  Holy crow! As someone who remembers when the rust-lang/rfcs repo was created, I can't believe we're over 2000 RFCs submitted!
  - steveklabnik 7y ago
    Issues and PRs are the same thing in GitHub internals, and the RFC number is the PR number. There haven’t been 2000 accepted PRs :)

Animats 8y ago

This has been done so many times. 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. "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." - we had all that in 1983. Look at the example starting at page 56 in [2]. 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. Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C. The "array is a pointer" mindset of C set programming back by decades. In Pascal, there were no buffer overflows. 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. The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It's hard to find.) Massive amounts of effort are being applied to try to infer information that C just can't express. This would be a lot more worthwhile if it resulted in translation of C to something better. Forty years, and this still isn't fixed. [1] http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79-731.pdf http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79... [2] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv [4] https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf

skywhopper 8y ago
Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial software, and you end up with a provably correct piece of software that is still full of business logic bugs and which inevitably fails to keep up with ever-changing business processes. I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.

ainar-g 7y ago

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

int_19h 7y ago
The article mentions unsafe more than once, and specifically says: "I do not intend to tackle the difficult problem of interaction between unsafe and safe Rust code; Rustbelt is the correct way to do it." The statement you quoted is clearly in the implied context of safe code.
Dylan16807 7y ago
> Hate to be that guy Clearly you don't.

int_19h 7y ago

Looking at examples of syntax for pre/post-conditions and invariants, it'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).

steveklabnik 7y ago
Until the release Thursday, it was not. As of the last release, it now is. This was probably written before that was available generally.
- int_19h 7y ago
  Thanks! For the curious, more details here: https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custom-attributes-accept-arbitrary-token-streams https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custo... From tooling perspective, this isn't perfect, because there's still no guarantee that the token stream is a valid expression. So e.g. an IDE trying to highlight them or do a global rename refactor has to assume, which might not always be correct for token-based DSLs. It would be nice to have some metadata to distinguish those. Or perhaps there is an idiomatic way to express it in a contract on the macro itself, that tools could look at?
  - steveklabnik 7y ago
    Not sure, to be honest.

lapinot 7y ago

I'm surprised there is no name dropping of `Hoare logic' here or in the article so i'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. But actually i must say i'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'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. 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't restrict the programs and you hope to give enough hints so that the solver doesn't get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust/reliable/simple whereas verification is a black-box which isn't easy to understand and thus never feels very "principled". Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent. My 2cts... Anyway i'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).

kaiby 7y ago

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

rrobukef 7y ago
Deductive verification is a large extension of designing by contract: The addition of a SMT solver to verify the contracts at compile time for instance. On the other hand libhoare only adds the contracts as a runtime addition with no mention of formally verifying these. The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet." This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816 https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.

pacemaker 7y ago

If you build Pacemakers see me - Pacemakers.com - lol