Logical frameworks and generic proof development systems

pencil and paper argument can provide, and are forced to formulate it
instead in formal logical notation, where every step can be
mechanically checked. Only computers have made it possible actually
to do this for real, but even with computers there are still problems,
since formal proofs are enormous and awkward objects. In theory, and
given a decent programming language, we could program up first-order
logic in a couple of pages, but the result is not usable - a usable
implementation is a large and complex system. This in turn raises a
second problem: endless different logical notations, each with its own
syntax and deduction machinery, have been proposed, and we are forced
to choose those that look as if they might provide a decent return on
the effort of implementation.

Ideally we would like a single system which could be instantiated with
different proof calculi as necessary, allowing implementation effort
to be amortized as much as possible across different logics. The core
of such a system would be a suitable abstraction of syntax and
deduction machinery. Such abstractions have been developed and
implemented, and are known as `logical frameworks'. They turn out be
be not only practically effective (reducing the problem of a *usable*
implemention again to the level of a couple of pages of code), but
also theoretically elegant. In this talk I'll try to give some
intuitions for the underlying concepts of logical frameworks, and the
problems and compromises, as well as the advantages, of systems based
on them.