As a topologist/category theorist with an interest in type systems I can assure you that I find pages full of sequents hard to understand :)

Actually I think the approaches are complementary. Suppose I wanted to talk about the simply-typed lambda calculus (with base types B) and its semantics. Category theory gives you a very simple definition: we take the free closed cartesian category C on the set B; if I choose interpretations of the types as sets, I get the semantics as the functor from C to Set induced from the map B -> Set and the fact that Set is a CCC. In the traditional presentation of the STLC, I have to define

- the syntax of types
- well-formedness and typing rules for terms
- reduction rules to put terms in normal form
- how to interpret a terms as a function on a set

All told it probably takes a few pages. (As an aside, it's also not clear what kind of mathematical object is being described, which I think can be a little off-putting to non-logicians.)

Of course the traditional presentation has one big advantage: it tells us what the objects and morphisms of C actually are! But this is a *computation* which we could (and presumably would) do if we adopted the category-theoretic definition of C. The category approach explains why we wrote down those few pages of syntax/typing/reduction rules rather than slightly different ones.

Naturally in other parts of mathematics it's common to have objects determined by universal properties (as the free CCC was here) and to want to compute more explicit presentation of them. If those objects are sufficiently similar to CCCs, then techniques from lambda-calculus may be useful.

notasking for (a) a justification for category theory as tool in various branches of mathematics, but rather for (b) a justification for category theory in the study of programming languages. (Correct?) I think there are many people here ready to answer (a), but not so many with an opinion on (b). $\endgroup$ – Kevin Walker Oct 24 '09 at 14:29