I can see the added functionality but... wouldn't building a SQL system that implements formal Relational Algebra be more useful? In that case, a person could run a proof solver to optimize their queries. This may be an ignorant statement since I'm not a 'real' CS person.

I think a higher level of abstraction makes certain functions easier?

Sorry. I can’t take the page that uses category theory and artificial intelligence in that sense seriously

Isn't automated theorem proving a kind of AI?

Unfortunately, the name is already taken - by Cassandra, which is widely used enough that it's probably worth avoiding a naming clash.

I commented something similar about KQL yesterday. At this moment probably every [A-Z]QL is taken at least twice over…

I just created a query language that searches abbreviations of technical modeling and query languages for a collision and posts the result in a comment on hacker news without formatting. The previous sentence was a simple statement using the built in grammar. Memory limit is defined by the size of the comment boxes, and output is stored in other user's history enabling redundancy.