Rust has demonstrated that you using a type system as a vehicle for separation logic works, even in imperative languages, and it's nothing as arcane as those immutable functional predecessors would suggest. It did this by making sure the language defines a type system that helps you, by making sure core properties of soundness can be expressed in it.
- soundness requirement for memory access: lifetimes
- soundness requirements for references with value semantics: >
&/&mut _- soundness requirements for resources:
CopyandDrop- making sure your logic is monotic: traits instead of inheritance, lack of specialization (yes, that's a feature).
- (notably missing: no dependent types; apparently not 'necessary' but I'm sure it could be useful; however, research is heavily ongoing; caution is good)
This allows the standard library to encode all of its relevant requirements as types. And doing this everywhere is its soundness property: safe functions have no requirements beyond the sum of its parameter type,
unsafe functionscan. Nothing new or special there, nothing that makes Rust's notion of soundness special.Basing your mathematical reasoning on separation logic makes soundness reviews local instead of requiring whole program analysis. This is what makes it practical. It did this pretty successfully and principled, but did no single truly revolutionary thing. It's a sum of good bits from the last decade of type system research. That's probably why people refer to it as 'the soundness definition', it's just a very poignant way to say: "we learned that a practical type systems works as a proof checker".
-- HeroicKatora @ Reddit - Dive into anything