Chris Uppal wrote: > Pascal Costanza wrote: > >> Sorry, obviously I was far from being clear. ACL2 is not >> Turing-complete. All iterations must be expressed in terms of >> well-founded recursion. > > How expressive does that end up being for real problems ? I mean obviously > in > some sense it's crippling, but how much of a restiction would that be for > non-accademic programming.
I don't know your definition of "real problem" ;), but ACL2 is definitely used in industrial settings. See http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/intro-to-acl2.pdf Pascal -- 3rd European Lisp Workshop July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/ -- http://mail.python.org/mailman/listinfo/python-list
