I hear you. Logic based and relational languages, like Prolog and miniKanren, have captured my attention a lot lately. One reason: I wondered if they might comp

I hear you. Logic based and relational languages, like Prolog and miniKanren, have captured my attention a lot lately. One reason: I wondered if they might complement LLMs nicely, or if LLMs might be a good tool for helping people learn/understand logic languages. While exploring the logic language space, I recently reacquainted myself with a branch of logic based languages based on *Clear/OBJ* that were born in the ‘70s at the University of Edinburgh. It never took off like Prolog, mostly because it was a research language focused on specification and verification, but a lot of the ideas have lived on in many modern languages. (Haskell, OCaml, C++, etc…) First, imagine you wanted to create a Prolog inspired language that allowed a person to create their own domain specific languages like they were abstract data types. You can also create abstract data types. The goal of this language isn’t to create a lexer/parser tool, but rather a more integrated tool that is capable of specifying both abstract data types and DSLs with a formalized logic. Oh yeah, let’s make it modular, so you can mix and match specifications. Clear/OBJ did just that, but they did it in a way built on a foundation of formal semantics. What I mean that is, Rod Burstall and Joseph Goguen used Category Theory to create an abstract formal specification that answers the question, “What is a logic?” https://en.wikipedia.org/wiki/Institution_(computer_science) https://en.wikipedia.org/wiki/Institution_(computer_science) With this framework in place, Goguen formalized order sorted equational logic and used it as the basis for the OBJ language in the ‘70s and ‘80s. Jose Meseguer formalized rewriting logic (for rewrite based systems) and used it as the basis for his language Maude. Most recently, Grigore Rosu lead the creation of Matching Logic (Used by the K Framework) for specifying the semantics of full programming languages, as well as automatically generating the lexer, parsers. This system of logic lets them define the operation semantics and prove the properties using Hoare logic in a single language. This one reference language semantics can derive program behavior (compilers/tooling) and verify programs. This works because we have a framework for defining a system of logic like Matching logic, which isn’t based on True/False and predicate logic, but pattern matching and power sets. Instead of defining Top/Bottom as True/False, what if Top/Bottom corresponded to pattern matching primitives like MatchesEverything/MatchesNothing? My point is this: While I am loving this resurgent interest in Prolog, I feel like it’s easy to overlook the wider world of logic programming beyond Prolog & Datalog. We have 50 years of incredibly insightful research that we can use to build the next generation of tools and systems to serve us.