《Mechanizing Proof》 Chapter 1

《Mechanizing Proof: Computing, Risk, and Trust》 Donald MacKenzie

Chapter 1 〈Knowing Computers〉

第一章可以分成兩個部份，後半部份(P.13-P.21)是這本書每一章的摘要，因為Donald MacKenzie自己也建議讀者如果對於一些技術細節不感興趣，可以跳過某些章節，因此花了不少篇幅描述每一章的主要內容，以幫助讀者選擇，也因為MacKenzie將這本書定位為歷史社會學的著作，書中包含很多歷史細節。因此，閱讀這些摘要其實已經可以大略理解這本書每一章的內容。

第一章的前半部份，則是這本書的背景和學術定位。一開始MacKenzie提到”數位電腦”(digital computer)的興起，以及”computing”的無所不在。[對他來說，digital computer和computing似乎是同一件事。]接著，他問，How can we know that the computing upon which we depend is dependable?...how do we know the properties of artifact? 這是這本書的根本問題。(P.1)

接著，他把「電腦的特質(property)」這個問題提升到另一個層次。MacKenzie將關於人造物和自然世界的知識分成三種：歸納性(induction)、權威性(authority)、演繹性(deduction)。他認為在STS的領域中，關於演繹性知識(包含數學和形式邏輯)的研究很少。(P.2)然而，MacKenzie接下來指出，一方面，電腦科學界自身對於歸納性知識拒斥(program testing can be used to show the presence of bugs, but never to show their absence!)；另一方面，軟體工程一直都不被承認是一個專業，也因此不構成一個權威，沒有權威性知識。所以，當問到我們怎麼知道電腦系統(軟體及/或硬體)的特質時，就等於直接提出關於演繹性知識及其證明的問題。[這個推論是不是有些問題？](P.3)

但是MacKenzie接著提到，軟體或硬體設計並不是純粹演繹性推論的問題，原因在於，…perhaps one could prove deductively that program or design was a correct implementation of its specification. It would not be a proof that the program or design was in an absolute sense “correct” or “dependable,” because the specification might not capture what was required for safety, security, or some other desired property, and because an actual physical computer system might not behave in accordance with even the most detailed mathematical model of it。不過Mackenzie沒有延伸這個論點，反而只是提到，不管如何，形式驗證(formal verification)對於電腦科學而言是非常必要的。

MacKenzie進一步指出，形式驗證是關於電腦的證明(proof about computers)，但另外一個相關連的，是電腦作為證明的用途(the use of computer in proof)。而這引起了一個問題，究竟電腦能不能成為人工數學家？(P.5)

提到證明和電腦的關係，是因為MacKenzie接下來就指出，這本書是一本歷史社會學的著作，目標是to describe salient features of the interrelations between computing and proof as they have evolved from 1950s onward。也就是說主要考察的是電腦運算(computing)和證明之間的關係。(P.5)

接著他提到他的資料來源，主要是期刊和書面文獻，另外輔以口述史。他也提到他對於科學戰(science war)的態度，他認為社會等所謂的「外在」因素和其他「內在」因素並非零合競賽，並非一個多另一個就減少。(P.6)[不過關於科學戰，是另一個大議題，需要其他的閱讀。]

第一章的主要內容，就是接下來對「風險社會」的回顧。MacKenzie首先引用Beck的說法，引出「風險分配的社會(risk-distributing society)」這個概念。接著，他提到，雖然科技風險被高度重視，但是關於電腦的風險，一直到Y2K這個問題出現才開始被重視。雖然最後證明Y2K並沒有造成大問題，但是已經對歐美世界造成影響：不知道電腦會如何動作(behave)是不可忍受的。相較於這種「不可見的潛在危險(invisible potential danger)」，也就是從軟體設計錯誤到bugs，各種環節都可能出現問題，Y2K其實是一個比較簡單的案例，因為已經知道問題是什麼。(P.8)

關於這種潛在危險對一般大眾的影響，MacKenzie引用Brian Wynne等人的看法，指出，Outside the necessarily narrow domains in which one has expertise, one can at best choose wisely in whom or in what to trust and find an appropriate balance between blind faith and self-defeating scepticism。也就是說，一般大眾會在絕對不信任和盲目相信之間找到一個平衡。(P.9)

從這裡MacKenzie已經從「風險」導入「信任」的問題。他開始回顧STS領域中和「信任」相關的著作。首先是Theodore Porter關於量化方法優勢的歷史著作。MacKenzie認為Porter的著作值得思考，因為他提出了a trade-off between mathematicization and trust這個觀點。Porter主要認為隨著社會從Gemeinschaft轉變到Gesellschaft，原先面對面的、對個人的信任會轉變成「對量的信任(trust in numbers)」，主要原因在於數學的高度結構性和規則限制(highly structured and rule-bound)，以及認為數學是一種規則的語言，一種即使笨如電腦也可以使用的語言。這個觀點也契合社會學對於現代性的看法，例如與Giddens對「信任」的觀點是相一致的。(P.9,10)

但是Steven Shapin的《Social History of Truth》這本書則提出不同的觀點。MacKenzie指出，Shapin認為在科學場域中，面對面的信任其實沒有消失。The scientists of high modernity “know so much about the natural world by knowing so much about whom they can trust”。事實上，MacKenzie認為這樣的看法是STS領域普遍接受的意見。(P.10)

然而，接下來Mackenzie從Shapin自己的作品《Leviathan and The Air-Pump》反駁Shapin的看法。MacKenzie指出，在Shapin的這本著作中，不管是本來就反對經驗和實驗知識的Thomas Hobbes，或者偏向實證立場的Robert Boyle，都將數學這種演繹性知識視為最高位階的知識。[也就是說，這是一種不需要「社會」(the social)的知識。](P.11)

關於這種演繹性知識與社會的關係，MacKenzie在David Hume的著作中找到了答案。Hume指出，沒有人會完全相信自己的演繹性證明，除非得到其他人的評估。(P.12)

從這裡，MacKenzie引入他的主題，在當代社會，我們不僅可以從其他人獲得評估與信任，也可以從電腦獲得。因此，Modernity’s “trust in numbers” can, it appears, lead back to a grounding not in people, but trust in machine。(P.12)

最後，MacKenzie做了一個總結，回到這本書的主題。This book examines the historical sociology of machine proof。(P.13)

Some comments and note

1. MacKenzie在書的一開始問的問題，也是我的論文方向。Digital或Computing對於人造物的內涵產生什麼影響？當Digital和Computing已經不僅僅出現在電腦上，也在許多日常生活的事物中，那麼這些人造物和過去的人造物有什麼不同？

2. MacKenzie的寫作，展現了如何將技術與社會結合在一起的可能性，或者說，如何討論一種非常根本的科技(computing)的社會影響(social effect)？他從風險社會這個背景切入，談到專業的不確定性，以及大眾「信任」的問題，然後從Proter的研究，引出一種「信任」方式的轉變，轉向trust in numbers，其實也就是trust in mathematics。接著，透過和Shapin的對話，說明這種演繹性知識其實也需要一種外在的”支持”，過去這要藉由其他人的確證獲得，但現在我們有另一種方式，也就是computing。在這裡，computing和proof的關係變得複雜，如MacKenzie所說，computing的內涵是一種演繹性知識，也就是說，必須藉由演繹性知識的proof來確保computing的運作，但另一方面，computing也可以用來作為演繹性知識proof的工具。也就是”deduction about computers” 和 “use of computer for proof”。因此，Mackenzie想要描述computing和deductive proof這兩者在歷史中的關係，藉此來思考”trust in numbers”這件事。

以上是我的理解。但是整個論證還是有些不清楚的地方？

3. My concern for the whole book:

對我的閱讀而言，有兩個重點，一個是MacKenzie認為的computing的內涵為何？另一個則是用「歷史的」這種方式去思考問題的特色為何？