text: The design of modern proof assistants is faced with several sometimes conflicting goals, including scalability, extensibility, and soundness of proof checking. In this paper, we propose a new design for proof assistants, in an attempt to address some of these difficulties. The new design is characterized by a pervasive use of macros in representing and checking proofs, and a foundational format for theory files based on JSON. We realize these ideas in a prototype proof assistant called holpy, implemented in Python. We also demonstrate how proof automation can be extended using Python under this framework. Finally, we present a case study about a simple imperative language.
  @cite_11: HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon's original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light's case this is Objective CAML (OCaml). Thanks to its adherence to the so-called LCF approach', the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.
  @cite_1: 
  @cite_2: Elementary Techniques.- 1. The Basics.- 2. Functional Programming in HOL.- 3. More Functional Programming.- 4. Presenting Theories.- Logic and Sets.- 5. The Rules of the Game.- 6. Sets, Functions, and Relations.- 7. Inductively Defined Sets.- Advanced Material.- 8. More about Types.- 9. Advanced Simplification, Recursion, and Induction.- 10. Case Study: Verifying a Security Protocol.
summary: Apart from the new concepts proposed in this paper, the design of holpy is largely based on that of Isabelle @cite_2 . Many choices in the design, including the use of higher-order logic, structure of terms, syntax for inductive definitions, conversion combinators, or even the typesetting of HOL terms used in this paper, are taken from there. In addition, the author examined the design of HOL Light @cite_11 and HOL4 @cite_1 during this research.