Jonathan wrote:

> Everyone and their grandma apparently knows that the simply-typed lambda calculus is the internal language of cartesian closed categories [...]

Yes, but what people often forget is that cartesian closed categories don't formalize what's really _interesting_ about the simply-typed lambda calculus, namely that it can be seen as a simple programming language.

The problem is that we get a morphism in a cartesian closed category from an _equivalence class_ of terms-in-context, where two terms related by beta or eta reduction are considered equal. Thus, a program that huff and puffs and adds 2 and 3, and one that simply prints out 5 count as _the same morphism!_

So, even in this "well-understood" case, the relation between category theory and programming has not been worked out in detail.

I began trying to deal with this problem in [the winter of 2007](http://math.ucr.edu/home/baez/qg-winter2007/index.html#computation) when Mike Stay started working with me. Now he's helping run the company [Pyrofex](https://johncarlosbaez.wordpress.com/2018/02/04/pyrofex/), and I'm working with him and my new student Christian Williams to tackle this issue.

A good approach would also handle imperative languages. I will have to read Goguen's book.