[FOM] Adventures in Formalization (Scott)

[Dana Scott]

Harvey Friedman has posted on this list three messages asking for
better developments in computer-assisted theorem proving.  This
call is very timely.  But before re-inventing the wheel, I would
like to suggest making an assessment of some existing systems.
In particular, the Isabelle system has some recent developments
which, I think, go a long way in meeting some of the demands
Harvey has made.  I went to the WWW sites and have edited up
some background descriptions and included pointers:

> Isabelle is a generic proof assistant. It allows mathematical 
> formulas to be expressed in a formal language and provides tools 
> for proving those formulas in a logical calculus. 
> 
> Isabelle was originally developed at the University of Cambridge 
> and Technische Universität München, but now includes numerous 
> contributions from institutions and individuals worldwide. 
> 
> Isabelle comes with a large theory library of formally verified 
> mathematics, including elementary number theory (for example, Gauss's 
> law of quadratic reciprocity), analysis (basic properties of limits, 
> derivatives and integrals), algebra (up to Sylow's theorem) and set 
> theory (the relative consistency of the Axiom of Choice). Also provided 
> are numerous examples arising from research into formal verification. 
> A vast collection of applications is accessible via the Archive of Formal 
> Proofs, stemming both from mathematics and software engineering.
> 
> See the Isabelle overview for a brief introduction, which along with
> many other resources can be found at:
> 
> https://isabelle.in.tum.de/
> 
> Also Tobias Nipkow and Gerwin Klein have written a book
> titled: "Concrete Semantics".  There is a free ebook version 
> of the book online:
> 
> http://www.concrete-semantics.org/
> 
> The recent development of Isabelle/Isar provides an interpreted language 
> environment of its own, which has been specifically tailored for the 
> needs of theory and proof development. Its top-level provides a robust 
> and comfortable development platform, with proper support for theory
> development graphs, managed transactions with unlimited undo etc.
> And the Isabelle/jEdit Prover IDE emphasizes the document-oriented approach
> explicitly. The main purpose of the Isar language is to provide a conceptually 
> different view on machine-checked proofs.
> 
> "Isar" stands for "Intelligible semiautomated reasoning". Drawing from both 
> the traditions of informal mathematical proof texts and high-level programming 
> languages, Isar offers a versatile environment for structured formal proof 
> documents. Thus, properly written Isar proofs become accessible to a broader 
> audience than unstructured tactic scripts (which typically only provide 
> operational information for the machine). 
> 
> Writing human-readable proof texts certainly requires some additional efforts 
> by the writer to achieve a good presentation, both of formal and informal 
> parts of the text. On the other hand, human-readable formal texts gain some 
> value in their own right, independently of the mechanic proof-checking process.
>