Desiderata for Interactive Verification Systems
What facilities should an interactive verification system provide? We
take the pragmatic view that the particular logic underlying a proof
system is not as important as the support that is provided. Although a
plethora of logics have been implemented, we think that there is a
common kernel of support that a proof system ought to provide. Towards
this end, we give detailed suggestions for verification support in three
major areas: formalization, proof, and
interface. Although our perspective comes from experience with
highly expressive logics such as set theory, higher order logic, and
type theory, we think our analyses apply more generally.
paper