J-Bob – The proof assistant from “The Little Prover”

github.com

59 pointsayberkt4 comments

I have the book but haven't opened it yet. Can someone who has comment on whether the proof assistant is tightly integrated with Scheme or whether it might be possible to implement it in another language such as Clojure ?

It's very small so you can do it easily in clojure, https://github.com/the-little-prover/j-bob/blob/master/schem... defines the language used and https://github.com/the-little-prover/j-bob/blob/master/schem... is the proof assistant. There's absolutely nothing fancy there.

"We include the necessary code to run J-Bob in ACL2 and Scheme, as well as a transcript of the proofs in the book. J-Bob is also included in the Dracula package for Racket."

Isn't ACL2 Common Lisp based? If it runs on Scheme/Racket and CL (or at least ACL2), it should be pretty easy to translate.

(ACL2? It's theorem provers all the way down!)

A quick skim over the code, shows it to be fairly small. ~1000 lines for the prover (little more in ACL2, little bit less in Scheme).

And about another 1000 lines for all the examples from the book (they too would need to be redone)

Reply on news.ycombinator.com