While technically there's a relationship between category theory and substructural logics (of course there is, category theory is general enough that there's a relationship between it and everything), they don't really strike me as having that much to do with it directly - they're a fairly straightforward extension (restriction) of typical presentations of constructive logic. And I wasn't aware that e.g. Rust picked up its type system via exposure through category theory. Is there a source for that narrative?
Girard mentions the connection with categories all the time.
For example in "Proofs and Types"
he proves various theorems along the lines of: the sub-category of coherence spaces and stable maps (one of the main models that LL was developed for) induced by some LL fragment is
cartesian closed category (IIRC). I think he developed LL in parts by fine-tuning it, until all the categories induced as models of fragments of LL have nice categorical properties. (To the extent that is possible.)
When I was a PhD student, my supervisor suggested that I learn category theory to understand linear logic. (Not sure, in retrospect, that was the best course of action, but that was my trajectory)
Rust's types evolved over many years. Rust used to have "typestate" for example. I had discussions with Graydon Hoare around 2011-ish about session types (which are linear). It struck me that Hoare knew exactly what I meant with the term. More generally, linear typing was just "in the air" in the early 2000s: you could not been serious in programming language design without being aware of linearity. Linearity was all over the research literature. Hoare was clearly very knowledgable in programming language research.
