| Technical approach | ACL2 is a constructive logic. Infix ACL2 (IACL2) simply provides an alternative infix syntax to the standard ACL2 Lisp-like prefix syntax. |
| Technical challenges | The only challenge was coming up with an infix syntax that came anywhere near the simplicity of the standard syntax. |
| Hard/New/Different | What is new about Infix
ACL2 (IACL2), as compared to ACL2,
is its syntax. We believe this syntax will be
accessible to the large class of new users lacking experience with
Lisp. At the moment, IACL2 supports a subset of the full range of operation of standard ACL2. As a result, some of the very advanced features of ACL2 are not available without reverting to the standard ACL2 Lisp syntax. On the other hand, these are capabilities that only very experienced users are likely to explore. Once you decide to use ACL2 on a large project you may want to take a day or two to learn the standard prefix syntax. |