core.logic VS hatlog

It's also available in Clojure: https://github.com/clojure/core.logic

If you want to write one yourself, it's pretty easy: https://www.youtube.com/watch?v=y1bVJOAfhKY

Something like Clojure's core.logic would be pretty nice too. As I understand it, this is one of those features that has been re-invented time and again in the Lisp world over the years. Although the CL standard is already fairly large, it would probably be a bit controversial to make that a required part of a CL implementation. Still, it would be cool to have the option of using dependent types in the macro system to generate formerly verified Lisp code at compile time.

It also has core.logic which is minikanren. There are other logic programming options as well. Some libraries like core.typed use core.logic for the type checker.

You could study core.logic: https://github.com/clojure/core.logic/tree/master/src/main/c...

I swear I'd bookmarked a resource that was more analogous to #2, but you may want to have a look at The Little Prover: https://mitpress.mit.edu/books/little-prover

related:

https://github.com/clojure/core.logic/wiki/A-Core.logic-Prim...

A couple years ago I hacked on a Python type inferencer someone wrote in Prolog. I wasn't enlightened, despite expecting to be, from a bunch of HN posts like this.

https://github.com/andychu/hatlog

For example, can someone add good error messages to this? It didn't really seem practical. I'm sure I am missing something, but there also seemed to be a lot of deficiencies.

In fact I think I learned the opposite lesson. I have to dig up the HN post, but I think the point was "Prolog is NOT logic". It's not programming and it's not math.

(Someone said the same thing about Project Euler and so forth, and I really liked that criticism. https://lobste.rs/s/bqnhbo/book_review_elements_programming )