[FOM] Mechanising Proof

[Roger Bishop Jones]

In connection with Harvey Friedman's recent postings
on proof checking and program verification,
the following reference may be of interest.
(previously mentioned on FOM but not much discussed)

"Mechanising Proof: Computing, Risk, and Trust"
by Donald MacKenzie
ISBN 0-262-13393-8

The book gives a good historical account of the
connections between mechanised inference and proof
checking and their applications, including software
and hardware verification.

(it also, incidentally, confirms my speculation
about the half century by dating Martin Davis'
implementation of the Pressburger decision
procedure to 1954)

Roger Jones