Arc Forumnew | comments | leaders | submitlogin
3 points by evanrmurphy 2407 days ago | 2 comments
Is anyone here familiar with ACL2?

I was talking with a guy tonight who works with it. From my understanding, it's a functional subset/variant of Common Lisp.

3 points by akkartik 2407 days ago | link

I took a very basic -- and very awesome -- class in grad school from J Moore, one of its creators:


2 points by evanrmurphy 2407 days ago | link

They have a web-based repl/tutorial at

The neatest thing I've found on there so far is the theorem proving abilities. Lesson 3 shows you can input things like (thm (= (+ a b) (+ b a))) and it will return a proof that the sum of a and b is equal to the sum of b and a.