Aspects of ACL2 User Interaction

Matt Kaufmann (joint work with J Strother Moore), UITP'08, August, 2008

ABSTRACT

Users of the ACL2 theorem prover typically interact with the system in many ways beyond submitting definitions and proving theorems. This talk will show some examples to provide a sense of the diversity of ACL2 user interaction. A few more in-depth examples may be found in the TPHOLS 2008 ACL2 tutorial.

Certainly we will consider the narrow sense of "user interface" as control of input and output. Users traditionally interact efficiently with ACL2 through Emacs, and we will demonstrate some Emacs customizations provided with the system. More recently, two Eclipse-based interfaces have been developed by other groups for teaching purposes: the ACL2 Sedan (ACL2s) and DrACuLa. Beyond the choice of editor (or terminal) is the issue of how to control ACL2 output, traditionally through generated English commentary. A proof-tree display illustrates proof structure and provides help for navigating that commentary. But a recent gag-mode enhancement is probably much more effective for debugging failed proof attempts.

Other useful output includes error and warning messages, which often point to user documentation. But ACL2 supports effective user interaction in ways beyond the above notions of input/output control.

Proof commands include not only definitions and theorems, but also scoping mechanisms. Hints can affect the course of proof attempts, and (less often) are dynamically generated by user programs (roughly in analogy to tactics in LCF-style systems).
Users can direct how proved theorems are to be stored as rules, by default as (conditional, congruence-based) rewrite rules. Syntactic control mechanisms can affect the applicability of rules.
The system state can be affected by setting various modes. Two examples include a program mode, which allows the user to write programs that need not terminate but can be used in macros, and a backchain limit for rewriting.
Session management commands include undoing, redoing, and querying the state.
Proof assistance is provided by two break/trace utilities for the rewriter; an interactive goal manager; and a report mechanism that can show "expensive" rules.
The programming interface provides features to bridge the gap between the user and the computing engine, such as Lisp-independent trace and backtrace utilities and verifiable alternative function bodies. This interface also makes available powerful Lisp features including packages and macros. State and other single-threaded objects are supported efficiently with an applicative semantics. A guard mechanism provides a powerful, though less automatic, alternative to types that is separate from the logical content of definitions.
Users can interactively extend the system's capabilities by providing books of logical definitions and theorems, as well as system utilities and even (through trust tags) system modifications.
A clause-processor mechanism provides an interface through which the user connects ACL2 with another tool.

A separate question, not addressed in this talk, is how to communicate proof results effectively to non-users. Our focus is on interface support for effective usage.