==========

                ACL2     Matt Kaufmann and J Moore

Matt:

 Right now, J and I are the sole implementors of ACL2.  This presents a
 bottleneck for supporting users (which will be even bigger some years
 down the road, when we're no longer able to contribute!).

 The "to-do" list has 561 entries, of which over 300 [337] may be
 things particularly worth doing in the short term.

 ACL2 users typically do well by focusing on proving useful rewrite
 rules, sometimes with hypotheses.  There are many other types of rules
 that can help, including so-called meta rules and clause-processor
 rules that allow the installation of provably correct code into the
 proof engine.

 But this isn't always enough.  For example, very recently a user
 wanted to massage the induction scheme that is stored into a simpler
 but logically equivalent form, and we had to modify the code to
 support that need.  For another example, it would be nice to
 disentagle I/O from the reasoning engine so that users can parallelize
 parts of the proof process.

 This fall we intend to begin a seed project on opening up the
 architecture of ACL2.  A first step will be to add design-level
 documentation, some of it as formal invariants on the ACL2 database
 (which we call the "logical world").  We have extensive source
 documentation and over 1500 pages of hypertext user-level
 documentation as a basis.  Another early step will be to put more of
 ACL2's reasoning routines in so-called logic mode, so that users can
 build formally verified tools on top of those trusted components.

 Eventually it would be nice if the only trusted components are
 extremely low-level.  J has a student, Jared Davis, who is defending
 his dissertation next month, which can be viewed as a proof of concept
 for that goal.  J has written a small prover, Paco, that also provides
 motivation and hope.

 But for now, our goal is less ambitious.  Anyhow, I'd be delighted to
 get advice from any of you during breaks, or if you like simply to
 explain more about what we have in mind, since there wasn't time to
 say much here.  I look forward to talking with anyone who is
 interested.

J: ACL2 has always focused on execution.  It has all sorts of hooks.
But mainly he'd like to see automation improved over the next 20
years.

- Make it easier for users to guide the system to a proof: How do you
 steer a largely automatic beast?

- Have ways to figure out what's out there in the community, like a
 "google for lemmas": Describe what is wanted and then search all
 ACL2 libraries mechanically.  Would be nice to be able to browse the
 dependency structure of the lemmas contributing to a proof.

- How do you come up with the right concepts and lemmas so that
 proving is more automatic?  Now, user has to decompose the proof
 manually.  Maybe tool could take advantage of lots of examples and
 invent suitable abstractions; not clear at all how to do this.

- Increase the capacity of ACL2.  For example, SMT can handle much
 bigger sets of inequalities.  We can read in an entire x86
 description into ACL2.  Jared Davis's largest proof has 241
 giga-conses in it.  We need to increase the capacity yet more.

==========