Arc Forumnew | comments | leaders | submitlogin
ACL2
3 points by evanrmurphy 4204 days ago | 2 comments
Is anyone here familiar with ACL2? http://en.wikipedia.org/wiki/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 4204 days ago | link

I took a very basic -- and very awesome -- class in grad school from J Moore, one of its creators: http://www.cs.utexas.edu/~moore/classes/cs389r

-----

2 points by evanrmurphy 4204 days ago | link

They have a web-based repl/tutorial at http://tryacl2.org/

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.

-----