Rust does have some theoretical innovations, however. Probably the most significant one that comes to mind is the solution to the problem posed in Dan Grossman'

Rust does have some theoretical innovations, however. Probably the most significant one that comes to mind is the solution to the problem posed in Dan Grossman's "Existential Types for Imperative Languages". A simple example of the problem: taking a reference to the value inside an Option is unsafe if the Option gets mutated and invalidates that reference. Previous solutions like Cyclone just disallowed taking those kinds of references entirely, or had only immutable data, both of which are way too restrictive. Rust's innovation was to track immutability vs. aliasing at a fine-grained level per use site via uniqueness paths to solve this specific problem (which ends up solving a whole bunch of other problems too). I'm not claiming the techniques are novel (borrowing rules are similar to fractional permissions for example), but I'm not aware of their application to this specific problem prior to Rust. (I could be wrong though! There's a lot of work on substructural type systems out there.) For a good overview of the prior art and how Rust relates, section 1.1 of the RustBelt paper goes into detail: https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf