Proving as Programming with DrHOL: A Preliminary Design

We discuss the design of a new implementation of the HOL system aimed at improved graphical user interface support for formal proof. We call our approach Proving as Programming, since we believe that metalanguage programming is a central aspect of proof construction. Thus we look to contemporary programming environments for inspiration on how to provide graphical support for proof. In particular, our implementation builds upon DrScheme, a popular programming environment for Scheme.

PDF