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

-----

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.