Joseph Goguen's book [Algebraic Semantics of Imperative Programs](https://mitpress.mit.edu/books/algebraic-semantics-imperative-programs) is "a self-contained and novel 'executable' introduction to formal reasoning about imperative programs." The author [writes](https://www.mta.ca/~cat-dist/catlist/1999/book-goguen) that it "does not explicitly use category theory, but almost everything in it was inspired in one way or another by category theory."

Goguen's homepage has more about the [OBJ language family](http://cseweb.ucsd.edu/~goguen/sys/obj.html) (and a lot of other very interesting topics).