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, post

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).