[anfelor]

Intuition from category theory has certainly been useful for some programming language features (eg. algebraic effects, modal types or lenses), but I don't think it has helped with the things you cite. Rusts ownership model was created with little formal, academic understanding - or do you mean more foundational stuff like linear logic? And I don't think that Haskell does supercompilation today? It does optimize a whole lot but that is more due to laziness and other optimizations. But neither these optimizations nor supercompilation have much to do with category theory as far as I am aware.

[Yoric]

Yeah, my phrasing is probably unclear. I meant to give examples of applications of formal semantics (huddling everything together). I should probably sleep instead of commenting on HN :)

But it is my understanding that Rust's ownership traces its roots back to both linear logic (well, affine logic) and region-based resource management, both of which have formal semantics.

I haven't followed what got merged into GHC, but I remember seeing demos (and a paper) of a Haskell supercompiler during a conference many years ago, so it is something.

In my sleep-deprived brain, supercompilation is directly related to algebraic effects (although probably not in Haskell itself), which are themselves related to category theory. I could be wrong.