Mechanizing Proof
by Donald MacKenzie · first published 2001
3mentions
1recommended by
2HN commenters
2012–2026first – last mentioned
50% recommend50% neutral
Most aspects of our private and social lives—our safety, the integrity of the financial system, the functioning of utilities and other services, and national security—now depend on computing. But how can we know that this computing is trustworthy? In Mechanizing Proof, Donald MacKenzie addresses this key issue by investigating the interrelations of computing, risk, and mathematical proof over the last half century from the perspectives of history and sociology. His discussion draws on the technical literature of computer science and artificial intelligence and on extensive interviews with part
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
…paragraph starting with "The truth is that regrettably little history of computer science, whether dumb or deep, has been written by trained historians". Let me reiterate one recommendation in particular, Mechanizing Proof, by Donald MacKenzie. This is a superb introduction to the technical subject of formal methods as well as a superb history! My only regret is that it was published in 2001 and a lot happened in the last…
on “The Tears of Donald Knuth” ↗I am quite aware of the problem of specification. For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough. http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...
on “A Tale of Two Pwnies (Part 1)” ↗…paper "The Evolution of Lisp" https://www.dreamsongs.com/Files/HOPL2-Uncut.pdf [extended version]. (They also both show up in Donald MacKenzie's Mechanising Proof https://mitpress.mit.edu/9780262632959/mechanizing-proof/ https://archive.org/details/mechanizingproof0000mack/ though it doesn't really connect them.)
on “The Birth of Prolog (1996)” ↗