I added a section on programmer-centric theorem-proving in my intro-to-ATS
book:
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/
Over the past few years, I gradually formed a somewhat philosophical
argument for
doing PwTP (programming with theorem-proving). Practical theorem-proving in
ATS is
meant to be semi-formal; its primary purpose is for debugging (instead of
guaranteeing
correctness).
“”""""
Programmer-Centric Theorem-Proving
I have so far presented several formal proofs in ATS. However, constructing
such formal proofs is at most a secondary issue in ATS. If I compare ATS
with theorem-proving systems such as Isabelle and Coq, I would like to
state emphatically that the design for theorem-proving in ATS takes a
fundamentally different view of theorem-proving. In particular,
theorem-proving in ATS does not take a foundational approach that
establishes the validity of a theorem by reducing it to the validity of a
minimal set of axioms and rules. Instead, theorem-proving in ATS is mostly
done in a semi-formal manner and its primary purpose is to greatly diminish
the chance of a programmer making use of incorrect assumptions or claims.
In this regard, theorem-proving in ATS is rather similar to contructing
informal paper-and-pencil proofs (in mathematics and elsewhere). I refer to
this style of theorem-proving in ATS as being programmer-centric. In order
to allow the reader to obtain a more concrete feel as to what this style of
theorem-proving is like, I present in the rest of this section a simple but
telling example of programmer-centric theorem-proving.
“”""""