4 ms·

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

• nickmain 11y ago
  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 ?
  • kryptiskt 11y ago
    It's very small so you can do it easily in clojure, https://github.com/the-little-prover/j-bob/blob/master/scheme/j-bob-lang.scm 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/scheme/j-bob.scm https://github.com/the-little-prover/j-bob/blob/master/schem... is the proof assistant. There's absolutely nothing fancy there.
    • mcguire 11y ago
      "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!)
  • rdc12 11y ago
    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)