[Yoric]

Category Theory (just as all mathematical models for programming or subsets thereof) are building blocks for reasoning on what we build. Past applications of such mathematical models include:

- programming languages with semantics that are better adapted to specific problems (e.g. Rust's ownership);

- better compilers (see e.g. Haskell's supercompiler, which puts to shame `constexpr`-style features);

- better static analyzers (e.g. better type systems, abstract interpretation, model checkers).

In the case of Machine Learning, it might some day help us create Machine Learning that we can understand and trust better. Or it might fail. Or it might help us invent something different entirely, in 30 years.

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

[riku_iki]

why those approaches never picked up outside of some academia projects?..

[Yoric]

These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD.

I suspect that Apple is also using model-checking at various layers, but I have no proof :)

[riku_iki]

and how does it work? Do they write drivers in some verifiable subset of C?

[Yoric]

That's how I understand it. I haven't checked the details.