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

[kryptiskt]

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.

[mcguire → kryptiskt]

"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!)