- [MacKenzie1998]
- MacKenzie, Donald A. Computers and the Sociology of Mathematical Proof. Prepared for Northern Formal Methods Workshop, Ilkley, September 1998. Edinburgh University Department of Sociology..
- [MacKenzie2001]
- MacKenzie, Donald A. Mechanizing Proof: Computing, Risk, and Trust. MIT Press (Cambridge, MA: 2001). Inside Technology Series. ISBN 0-262-13393-8 hard cover, alkaline paper.
My associate, Bill Anderson, referred me to Mechanizing Proof and now we are both reading it. Considering that this is the week that Bill Gate's chose to emphasize Trustworthy Computing as fundamental to the .NET Strategy, it seems valuable to gain as much out of MacKenzie's treatment of the way trust is unavoidable as we can.
I am also interested in this topic because trust is a crucial consideration in my Miser Project formalization of a computational mechanism. I am already aware of some places where trust cannot be avoided, and I intend to use that to demonstrate the requirement of trust in several dimensions. Mechanizing Proof strikes me as the appropriate background and source for appropriate distinctions and nomenclature.
-- Dennis E. Hamilton
2002 January 18
Last updated 2002-10-13-13:07 -0700 (pdt)
see also: R020100A: Players in
Trustworthy Computing
R020100B: Unrefined Sources and Materials on Trustworthy
Computing
R020100C: The Road to Trustworthy Computing (a timeline)
Content
Syllabus
Bibliography
Bill and I decided that we need to be disciplined at working through this book. It also seems that we could make an useful contribution by identifying and locating many of the source materials as well as more-recent information (e.g., an error in the Shostok prover that was uncovered after all this time). In particular, we want to see what we can find on-line in terms of fundamental materials that we and others may wish to confirm themselves.
The following reading-plan/syllabus is broken into arbitrary week-long chunks. I hope we can best that. The extensive notes of the book need to be reviewed along with the corresponding chapters. My intention is to link further notes and resources here.
| Week Ending | Topic | Status |
2002-02-02 |
Acknowledgments
There seem to be a great many related materials to review and consider as essential background and primary sources. I don't propose to read all of those. It seems more valuable to know where we can get our hands on them. I began a list of people and places whose work is relevant for Trustworthy Computing, starting with the people that MacKenzie has relied up one way or another. I also began a list of sources and readings that are to be located and added to an appropriate bibliography as they are found to be pertinent. Finally, I noticed that Chronology is important, so I began a chronology based on the Appendix in [MacKenzie1998] |
Text
pages created that are a basis for further analysis: identification of
contributors, location of important reference materials, and creation of a
time-line.
Complete. |
2002-02-03 |
1. Knowing Computers | Notes
and text have been compiled below. The references have been updated
and consolidated where possible.
The synopsis of the chapters has been spread out to the appropriate sections from here, and I'll do more as I get into the chapters. |
| 2002-02-08 | 2. Boardwalks across the Tar Pit | |
| 2002-02-15 | ||
| 2002-02-22 |
4. Eden Defiled |
|
| 2002-03-01 | 5. Covert Channels | |
| 2002-03-08 |
6. Social Processes and Category Mistakes |
|
| 2002-03-15 | 7. Clocks and Chips | |
| 2002-03-22 | 8. Logics, Machines, and Trust | |
| 2002-03-29 |
9. Machines, Proofs, and Cultures |
Benefits of computerization clear and compelling.
Dependence comes with it. Reliance in safety-critical systems.
Tension that results: enthusiasm (.com) and fear (millennium bug).
How can we know the computing we depend upon is dependable?
Broader question: How do we know the properties of the natural world, of artifacts?
For computers, how do we know the properties of computers and the programs that run on them? Brings focus to deduction.
Offers a definition of three categories of sources of knowledge:
- induction - we learn the properties by observation, experiment, and (especially in the case of artifacts) testing and use
- authority - people whom we trust tell us what the properties are
- deduction - we infer the properties from other beliefs, for example by deducing them from theories or models
MacKenzie sites his 1996 paper for this.
Deductive proof at the core of mathematics and formal logic. That propositions can be proved, not simply justified empirically, is at the heart of the claim to provide more secure knowledge than the natural sciences.
It is often assumed that there is nothing sociological that can be said about proof, which is ordinarily taken to be an absolute matter.
Influential current of thought within computer science is that inductive knowledge of computer systems is inadequate, especially in areas where systems are critical to human safety or security.
Authority is weak, absent an established profession of software engineering or the like.
Alternative often seen as being deductive proof.
MacKenzie seizes on the key elements:
If one could,
- first, construct a faithful mathematical representation of what a program or hardware design was intended to do (in the terminology of computing, construct a "formal specification") and,
- second, construct a mathematical representation of the actual program or hardware design, then
- perhaps one could prove deductively that the 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.
All of those involved in the field would acknowledge that these are questions beyond the scope of purely deductive reasoning.
More useful concepts:
- Formal verification is proof about computers (this being how the term is applied in the formal verification community)
- Distinct is the use of computers in proof
- automated theorem proving and proof checking
- inference engines in artificial intelligence applications
The topic of the book.
Methodology is one of social science. Uses the technical literature of computer science and artificial intelligence for factual assertions wherever possible, and interviews with the main participants, used primarily as evidence of interviewees' opinions and beliefs.
Does not see the consideration of social factors as diminishing in any way the others that play in the conduct of science.
Welcomes errors on the technical subject being pointed out. Does not want cross-disciplinary point scoring.
The (sociological) question of one's knowledge of computer-system dependability.
Striking feature of the politics of high modernity is the salient place in it of issues of technological risk.
Measured by life expectancy, today's Euro-American world is uniquely safe.
Patently, however, members of these societies do not always feel safe.
Comments on invisible hazards and the inability to have direct knowledge, thus a reliance on authorities of various kinds and levels of trustworthiness. "an invisible potential danger, the seriousness of which the layperson's unaided senses cannot judge."
The millennium bug is seen as the one main case of widespread fear of the computer.
In the Y2K case, political and business leaders throughout the Euro-American world judged the effort essential: not knowing how computer systems would behavie was intolerable.
Trade-off between mathematicization and trust. As community becomes modernity's society, face-to-face solutions are no longer viable. Modernity's "trust in numbers" is a substitute for absent trust in people. [Porter] argues that "reliance on numbers and quantitative manipulations minimizes the need for intimate knowledge and personal trust." What we trust are "systems of technical accomplishment or professional expertise," not particular, personally known people.
2002-02-03: A Concern: I think the debates over the World Trade Organization suggests that the populace does not trust in arrangements that have technical merit, if the public perceptions is of a zero-sum game. Also, I am disturbed about the fear of computer viruses and its most-peculiar manifestation, the computer-virus hoax message. In fact, e-mail-carried hoaxes of all kinds are problematical for me. What I haven't got my grip on is the willingness of people to forward these to all of their friends, often with the appearance of testimony to the message's authenticity, when it is not difficult to impeach the authenticity and the authority of the message. -- dh.
It is pointed out that within scientific communities, there are systems of trust based on degrees of personal knowledge of others, however. There is need for honest testimony and skillful experimentation.
No matter how much confidence scientists have had in empirical methods and trustworthy testimony, they have conceded deductive proof as providing surety of the truth of a conclusion without consulting experience.
There is Hume's observation that "there is no ... mathematician so expert in his science, as to place entire confidence in any truth immediately upon his discovery of it."
But now we have machines for checking of proofs. Leading us from trust in people to trust in machines.
It is interesting that if a computer is able to operate without socialization, and be an expert in a human field, this can be a demonstration that socialization is not the only way to accomplish that. "If machines can prove, does it mean that proof is not social?"
Synopsis: Dependability. Potential for disaster in critical systems. Awareness of software crisis. October 1968 NATO Conference identified software engineering as the solution to the crisis. Emphasis on practical disciplines from traditional areas of engineering and emphasis on theoretical foundations of computer science, especially mathematics and logic. Subjecting the computer to the rigor of mathematics and logic: Edsger W. Dijkstra, John McCarthy, Peter Naur, Robert W. Floyd, Tony Hoare. Harlan Mills on subjective conviction for correctness of claimed proofs. James King's program-proof program.
Synopsis: Newell and Simon, Science of the Artificial, Logic Theory Machine, Human-like Heuristics. Hao Wang, Liebniz, Alan Robinson resolution method. Debates about computers: Roger Penrose and J. R. Lucas. Using Gödel's proof to argue for human intelligence. Douglas Lenat's Automated Mathematician, AM.
- [Gates2001]
- Gates, William H., III. Trustworthy Computing. E-mail message. 2002 January 15.
This message was widely distributed outside of Microsoft Corporation. Here are commentaries via AP, BBC, USA Today, and ZDNet.
- [MacKenzie1998]
- MacKenzie, Donald A. Computers and the Sociology of Mathematical Proof. Prepared for Northern Formal Methods Workshop, Ilkley, September 1998. Edinburgh University Department of Sociology. Published on-line.
- [MacKenzie2001]
- MacKenzie, Donald A. Mechanizing Proof: Computing, Risk, and Trust. MIT Press (Cambridge, MA: 2001). Inside Technology Series. ISBN 0-262-13393-8 hard cover, alkaline paper.
created 2002-01-18-14:34 -0800 (pst) by orcmid
$$Author: Orcmid $
$$Date: 03-05-25 10:50 $
$$Revision: 11 $