证明的机械化
Mechanizing Proof
Donald MacKenzie · 初版 2001 年
1人推荐
2位读者提及
3次提及
我们个人与社会生活的方方面面——我们的安全、金融体系的完整性、公共设施及其他服务的运转乃至国家安全——如今都依赖于计算。但我们如何确信这种计算是值得信赖的？在 Mechanizing Proof 中，Donald MacKenzie 从历史学与社会学的视角探讨了这一核心问题，调查了过去半个世纪中计算、风险与数学证明之间的相互关系。他的论述借鉴了计算机科学与人工智能的技术文献，并基于对参与……的广泛访谈。
Hacker News 上怎么说
正在加载完整评论……
…以“事实是，令人遗憾的是，无论是浅显还是深刻的计算机科学史，受过专业训练的历史学家写过的都极少”开头的那一段。让我特别重申一个推荐：Donald MacKenzie 的《Mechanizing Proof》。这既是一本关于 formal methods 这一技术主题的绝佳入门书，又是一部极佳的历史著作！我唯一的遗憾是它出版于 2001 年，而在过去的……里发生了太多事情。
…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…
我很清楚 specification 的问题。对其他人说一句：我从读《Mechanizing Proof》这本书中获益匪浅。不需要任何 formal methods 的基础知识（但你在阅读过程中会学到一些 formal methods 的知识）。我对这本书推崇备至。http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...
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...
…论文《The Evolution of Lisp》https://www.dreamsongs.com/Files/HOPL2-Uncut.pdf [扩展版]。（他们两位也都在 Donald MacKenzie 的《Mechanising Proof》中出现过 https://mitpress.mit.edu/9780262632959/mechanizing-proof/ https://archive.org/details/mechanizingproof0000mack/，尽管书中并没有真正把他们联系在一起。）
…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.)