Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theori

Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads neatly generalise many similar ideas in programming. (Moggi/Plotkin should have won a Goedel award for this!) This led to a great deal of activity towards generalising this to other forms of computation, in particular parallel computing (key problem: generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding). In my opinion, this has comprehensively failed to date, in the sense that (A) while you can express some parallelism in a way that can be read as a generalisation of cut-elimination / category theory, that is not surprising since (simplifying a great deal for brevity) category theory is a foundation of mathematics; but (B) when you express non purely functional computation categorically, you get extremely complicated formal systems that obscure the fundamental simplicity of what they abstract from and generally have only what they abstract from as actual model of the abstraction. Let's take Example 47 from the Native Type Theory paper: what exactly is the formal property the typing system induces? (The paper makes vague allusions to a "foreign function interface" with rho-calculus, but there is no published understanding of even the equational theory of rho-calculus. Why should I trust this paper?) What is the logic that the paper promises ("Native Type Theory gives provides a shared framework of reasoning")? What are the proof rules, so I can type them into Lean or Coq? Show me that they are better than the simple logics I get from looking at lambda-calculus operationally. Each abstraction has costs and benefits. As of 2021, the costs of categorical methods outside of pure functional languages outweigh their benefits. I worked in categorical methods for programming and changed the field, when I realised this.