[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.