A few minor remarks by Bob Boyer, Computational Logic, Inc.

     1.  It is useful to view meta-level reasoning as merely an application
     of program verification.  Simply put, one is verifying the correctness
     of certain programs (the metafunctions), which happen then to be
     installed in the prover's code.

     2.  For efficient meta reasoning, it seems crucial to focus upon a
     very fast method (one machine instruction or so) for quoting and
     dequoting terms.  Boyer and Moore believed this to be so important
     that they recoded Nqthm to be able do it.  This issue is both subtle
     and tedious.

     3.  Although Nqthm's meta reasoning capability has received a good
     bit of use by very experienced users, it still suffers from the small
     number of places in the overall structure of the prover where it can
     be applied.  Figuring out how to attach a meta-theoretic capability
     in more places, soundly of course, would be a good idea.

     4.  Both Nqthm and Acl2 use an approach based on evaluators (roughly,
     functions that provide an operational semantics for the term
     language).  This approach is probably not as useful an approach as a
     full-fledged proof-theory style approach, which would, for example,
     permit one to prove and add meta theorems such as generalization.