"Why didn't substructural type systems catch on before Rust" is an interesting question I don't know the answer to, and the answer might just be "dumb luck".
15
1
102
Conversation
In the early 2000s, there was a lot of effort (including at MSFT / MSR) around trying to integrate substructural type systems and OO. My memory is that it all ended up at odds with even basic OO patterns...
1
7
So, then you had to layer a constraint language to express temporary conditions to the prover, and now your framework developers are also doing theorem proving, but this was also before the Twelf/Coq revolutions, so it was adhoc and the provers were not exactly gentle interfaces.
1
2
My own touchpoints were the Spec# work which in addition to the usual OO stuff of the time (exception analysis, pre/post conditions) also went really deep down the object ownership rabbit hole:
1
1
Oh interesting! Is this a good paper to look at in relation to that work?
That is unfortunately long before I'd gone to grad school and developed paper-reading skills. So, most of what I remember about it is from the folks on my team who were contributing to the work from the product team side and internal talks / demos.
1