if anyone has any experience or thoughts on this, I’m working through a prep for an application thats integrating a datalog engine in a pretty interesting way, and I’d welcome any thoughts on the utility of things like this, or prolog/datalog in general
What is the interesting way? Having a database that can be queried with a full fledged programming language is always a good idea in my book. The only downside is potential scalability issues but that’s a bridge that can be burned when you get to it.
the interesting way (to me at least!) is an implementation of datalog in ocaml for an upcoming release of BAP, the binary analysis platform. A short summary is that BAP lifts binary code into its own formalized instruction language BIL, which is then analyzed via its own IR. At the moment BAP is at 1.6 and with its 2.0 release it will have shifted the semantics of BIL to incorporate a datalog implementation, allowing all kinds of interesting analysis and, importantly, increasing the size of binaries the you will be able to analyze. I see that you’re one of the organizers of the SF formal methods meetup, you might find BAP pretty interesting, I’ll add some links.
the research being used to guide the implementation of the BAP+datalog
click the download link to grab a pdf of the thesis
First prototype of the implementation
Here’s a Coq formalization of BIL
The main developer is pretty active on Gitter, and very cool. We’ve had some interesting back and forth on classical vs intuitionistic logic.
This is indeed good stuff. Thanks for the references.
gladly! the timing on your blogposts was a nice serendipity, I just grabbed a couple of prolog books from the library to sort me out and make picking up datalog easier. One of the things I’d like to do is just cram a prolog implementation into one of my systems such that I can query system state via prolog, very much like in your posts. Not sure where I’ll go from there, but I’m not looking to make much of it, I just want to internalize the semantics of a logic language as much as I can in a short amount of time.
Latest I saw about embedded logic/constraint solvers were about mini/micro-kanren. You might be able to re-use one of those implementations for your specific use case.