Alternate Talk Titles We Can't Complain But Sometimes We Still Do ACL2 provides so much .. and yet we want more Conditional Forms : The Shame of ACL2 We want to be pure .. but we are unwilling to sacrifice 3 Ways Common Lisp is Better Than ACL2 Looking at ACL2 as a real programming language