are there any attempts to map category theory (or type theory or set theory -- I am not sure where the boundaries are) to applications (versus theory per se), roughly analagous to Z or VDM, that might be comprehensible to somewhat without the ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ formal framework? ^^^^^^^^^^^^^^^^ This last condition is the kicker. Applying category theory without a grasp of the formal framework is like operating a car without a grasp of how to drive. So I would say a definite "not". If not, is there a sequence of study you would recommend for proceeding? It would be interesting to have some comparison of the effectiveness of the various texts and articles that are aimed at computer scientists and set at a reasonably elementary level. There are quite a few of these, some easily identifiable from their titles. I have no idea which ones work best in practice for beginners. But there are first steps to category theory that one can take that do not require any category text. How comfortable are you with graphs and partially ordered sets (definable as transitive acyclic graphs)? If not very, then this is an excellent place to start. Graphs and posets are more fundamental than categories, in the respective senses that a graph is a basic underlying structure of a category while a poset is a primitive kind of category. Moreover they are versatile and useful concepts that will stand you in good stead in many areas of computer science and elsewhere. Once you are comfortable with graphs and posets the conceptual passage to categories becomes easier. What goes on in categories is for the most part a complicated generalization of what goes on in graphs and posets. The complications arise from the composition law for a category, which amounts to a means for tracking which path one is following in a graph. When there is more than one way to get from A to B, the mathematics of keeping track of those ways gets very interesting. This is what is going on down in the engine room of category theory. Up on the bridge the ship is steered with natural transformations. Both of these levels have their counterparts in poset theory and poset-based logic respectively, and make much more sense when understood in that light. Vaughan Pratt