| In Rod Burstall's 1980 paper titled, "ELECTRONIC CATEGORY THEORY", he explores "using algebraic and categorical ideas to write programs", and explains how his interest in "using algebraic ideas in programming goes back to work with Peter Landin, who first interested me in universal algebra and category theory" in the '60s. Also, you have to love this introduction: > If we can have electronic music, why not electronic category theory? 'Music has charms to soothe the savage breast', said Congreve Has category theory less charm? Can we not make the electrons dance to a categorical tune? You have to love his whimsy. I've been playing with lately Maude (Based on OBJ and Clear) and it really seems like the motivation for algebraic data types has been about driving categorical algebras / universal algebras from the beginning. At some point it clicked how it felt like I was defining categories (modules), objects (sorts) and morphisms (ops) and then adding constraints writing equations. I don't know Maude or category theory well enough to say it qualifies as an "electronic category theory" for some defined set of categories (small?), but I can see that vision, and how it's a little disappointing this vision isn't better understood. FYI, Burstall sought out Jim Thatcher from the ADJ group and Thatcher, who referred Burstall to Goguen (Thatcher was focused on stopping the Vietnam war), who was the ADJ group's practicing logician / category theorist. From what I read, the reason Goguen was even at the ADJ group in the first place is MacLane recommended him for the position while Goguen was studying under him in Chicago. When you consider the timeline in 1977 when Burstall/Goguen first met. They figured out the semantics for this language very quickly, define institutional model theory, which formalized a minimal definition of "what is a logic?" and then used that as the basis for creating Clear, which inspired Burstall's Hope and Goguen's OBJ. The fact that they did all that in such short order is very telling (IMO) for how long they had been each been concocting schemes to get universal algebras and category theory into computer science. https://link.springer.com/chapter/10.1007/BFb0022493 |