[FOM] Mechanizing Proof: Computing, Risk, and Trust

[Dennis E. Hamilton]

An aside,

I noticed an odd drift in the way Donald MacKenzie's book is mentioned here.  It has now been identified as "Automating Proofs."  The correct, full title is "Mechanizing Proof: Computing, Risk, and Trust."  <http://nfocentrale.net/orcmid/readings/trust.htm#[MacKenzie2001]>.

It is useful to consider that "Mechanizing Proof" is meant in quite a different sense than "Automating Proofs" and that the title was carefully chosen.  I was not aware of the "Strong Programme" (mentioned in an earlier posting) .  After some investigation, I don't think one's position about that need interfere with appreciation of "Mechanizing Proof."  The book looks at the question of what it is being taken to mean when someone claims to have a mathematical proof about the correctness of the behavior of an artifact.  (Including that artifact performing an ATP procedure, I suppose.) 

In the context of computing systems, the focus of the book, I find that the review by Peter Neumann says much about the appeal of Mackenzie's treatment, including his wonderful recounting of events that I have personal recollection of.  <http://www.acm.org/ubiquity/book_reviews/p_neumann_4.html>

-- Dennis

-------------------------------
Dennis E. Hamilton
mailto:Dennis.Hamilton at acm.org | http://orcmid.com 
OpenPGP public key fingerprint BFE5 EFB8 CB51 8781 5274  C056 D80D 0C3F A393 27EC

-----Original Message-----
From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu]On Behalf Of
Doron Zeilberger
Sent: Tuesday, November 11, 2003 17:49
To: fom at cs.nyu.edu
Subject: [FOM] Brief Reply to Comments on my Opinion 57

[ ... ]

3) Reply to Ms. Kathy Garber

[ ... ]

>Specifically, for Mr. Zeilberger - have you investigated the tools of the
>automated theorem proving (ATP) community yourself and found them lacking?


Interesting questions, Ms. Gerber. I have a great admiration to
ATP, and read with great interest Donald MacKenzie's book
`Automating Proofs', but I think that ATP have limited scope in
creating new non-trivial math, since it is logic-based.
I prefer what I call ansatz-based math, which would emulate
(much faster and better) the way math is actually created,
as opposed to written up, in the stultifying Euclidean-Fregean
style. [ ... ]