Mechanizing Proof: Computing, Risk, and Trust (Donald MacKenzie; The MIT Press, 2001)

MacKenzie pyrkii kirjallaan vastaamaan kysymykseen 'Mistä tiedämme, että tietojenkäsittely on luotettavaa?' Joidenkin mielestä kysymys on tarpeeton, koska tietojenkäsittely ei ole luotettavaa, vaan täynnä ohjelmistovirheitä ja tietoturvariskejä. Joidenkin mielestä taas nykyisen epäluotettavan tietotekniikan syy on pikemminkin se, että ohjelmoinnissa ei käytetä oikeita menetelmiä eikä ohjelmia testata tarpeeksi.

MacKenzien kirja on laaja katsaus tietojenkäsittely perusteisiin. Erityisesti hän pohdiskelee tietotekniikkaan sisältyviä riskejä ja mahdollisuuksia niiden minimointiin. Samalla hän esittää tärkeät kysymykset: Mihin tietokoneen käyttäjä voi luottaa? Millaiseen tietotekniikaan yhteiskunta voi luottaa?

MacKenzie pohtii luotettavuutta tietotekniikan perusteista alkaen. Voidaanko tietokoneohjelma suunnitella niin, että se varmasti toimii oikein? Voidaanko ohjelma ehkä jopa todistaa matemaattisesti oikeaksi? Entä miten tietotekniikan kehittäjien ja käyttäjien vuorovaikutus yhteisönä liittyy riskeihin ja luottamukseen?

MacKenzien käsittelee teoksen alussa matematiikan perusteita ja ristiriidattomuutta. Hän tuo esille tietotekniikan käytön matemattisten teoreemojen todistamisessa. Hän pohtii tämän lähestymistavan rajoja: voisiko tietokone olla matemaatikko?

Teoksen skaala on laaja lähtien matematiikasta ja päätyen tietotekniikan sosiologiaan. MacKenzien pohtii tietoturvan perusteita ja mahdollisuuksia ylipäätään kehittää turvallista tietotekniikkaa. Samalla hän tuo ymmärrettäväksi tämän alan tutkijoiden haasteet ja mahdollisuudet. Todellisessa maailmassa ei eletä pelkästään abstraktioiden varassa, vaan tietotekniikan luotettavuuteen vaikuttavat myös sosiaaliset tekijät.

Näyttää mahdottomalta todistaa tietokoneohjelman toimivuutta. Saatavilla ei ole myöskään vuorenvarmoja ohjelmointimenetelmiä. Siten on yllättävää, että tietotekniikka kaikesta huolimatta yleisesti ottaen toimii varsin hyvin.

MacKenzie etsi kirjaansa varten todistettavia tapahtumia, joissa tietotekniikka on ollut ihmisten kuolinsyy. Varmistetussa aineistossa oli lopulta 1 100 tapahtumaa. Yli 90 %:ssa syynä oli epäonnistunut ihmisen ja tietokoneen vuorovaikutus. Fysikaaliset syyt olivat taustalla 4 %:ssa ja ohjelmistovirheet vain 3 %:ssa tapauksista.

Miten ohjelmistot ovat näin luotettavia ilman matemaattisia todistuksia? Tätä ristiriitaa nimitetään Hoaren paradoksiksi. Tietojenkäsittelyn kehittämiseen merkittävästi vaikuttanut Hoare on ihmetellyt esitelmissä ja artikkeleissa, miksi tietotekniikka toimii kohtalaisen hyvin, vaikka kehityksessä ei käytetä hänen ja muiden tutkijoiden suosittelemia ohjelmointi- ja suunnittelumenetelmiä.

MacKenzien mukaan tärkein syy tietoteknisten ongelmien suhteellisen pieneen määrään on se, että kriittisten järjestelmien tietotekniikkaan on kiinnitetty erityisen suurta huolellisuutta. Kun tietotekniikan tutkijat ovat korostaneet ohjelmistovirheiden vaaroja, on virheiden seurauksiin pystytty ennalta varautumaan. Siten suunnittelijat ovat välttäneet turvallisuutta vaativissa kohteissa täysin automatisoituja järjestelmiä, joissa ei ole ihmistä valvomassa toimintaa.

Tietotekniikan käyttäjien panosta järjestelmien luotettavuuteen ei aina täysin ymmärretä. Usein ihmiset korjaavat tietoteknisten järjestelmien virheitä huomaamatta tätä itse. On siis väärin syyttää tietotekniikan toimimattomuudesta käyttäjiä. Usein on päinvastoin niin, että käyttäjien ansiosta tietotekniikka ylipäätään toimii.