The Engines of Logic
Sunday, June 8th, 2008It is interesting to contrast von Neumann’s views of computer programming as an activity with Turing’s. Von Neumann called it “coding” and made it clear that he thought of it as a clerical task requiring little intellect. A revealing anecdote tells of a practice at the Institute for Advanced Study computer facility of using students to translate by hand computer instructions written using human-readable mnemonics into machine language. A young hot-shot programmer proposed to write an assembler that would do this conversion automatically. Von Neumann is said to have responded angrily that it would be wasteful to use a valuable scientific tool to do a mere clerical job. In his ACE report, Turing said that the process of computer programming “should be very fascinating. There need be no real danger of it ever becoming a drudge, for any processes that are quite mechanical can be be turned over to the machine itself.”
— The Engines of Logic, p. 192
Ho appena finito di leggere The Engines of Logic di Martin Davis, un saggio sulle vite e il lavoro dei logici che possono essere considerati i papà dell’elaboratore elettronico. E sono, secondo Davis:
- Leibniz, perché è stato il primo a concepire l’idea di meccanizzare il ragionamento
- Boole, perché ha inventato quella che oggi chiamiamo logica proposizionale o Booleana
- Frege, perché ha esteso la logica proposizionale con la quantificazione (per ogni… esiste…)
- Cantor, perché ha inventato il metodo di dimostrazione “diagonale”, che è stato poi messo a frutto da Goedel e da Turing
- Hilbert, perché ha dato nuova linfa al progetto di Leibniz di ottenere un metodo per ottenere la risposta a qualsiasi domanda tramite il calcolo
- Goedel, perché ha dimostrato che il progetto di Hilbert è irrealizzabile
- Turing, perché ha definito con precisione il concetto di “problema computabile” (favolosi quegli anni… più o meno nello stesso periodo Hamming definiva con precisione il concetto di “informazione”. Bello che si possa dare una definizione precisa a concetti apparentemente sfuggenti.) Non solo: Turing ha anche concepito l’idea dell’algoritmo universale, ovvero di una singola macchina che è in grado di risolvere qualsiasi problema computabile. Da quest’idea nasce l’elaboratore di uso generale che conosciamo oggi: con il mio computer posso risolvere problemi di analisi matematica, archiviare indirizzi, editare immagini… non c’è limite.
- Von Neumann, perché ha progettato l’architettura generale degli elaboratori che usiamo ancora oggi, e continueremo ad usare per un bel pezzo, visto che non ci sono all’orizzonte alternative plausibili.
L’argomento fondamentale del libro è che sì, gli ingegneri che hanno progettato l’hardware hanno la loro parte di merito, ma è l’idea logica a monte che è più importante e ha portato più lontano. Per fare un paio di esempi dal libro: Eckert e Mauchly, gli ingegneri che hanno costruito ENIAC, sono stati geniali per come sono riusciti a rendere affidabile una macchina costruita con 15000 tubi elettronici, componenti notoriamente inaffidabili. Però era basata sulla notazione decimale: pensate che spreco! La notazione binaria è molto più economica. Non solo, ENIAC comprendeva meccanismi specializzati per calcolare funzioni trascendenti, analogamente a quanto avveniva nei differenziatori analogici che erano le macchine di calcolo più avanzate dell’epoca. Ma in un calcolatore digitale non c’è bisogno di questi aggeggi, perché le funzioni trascendenti si approssimano con serie che possono essere calcolate con le ordinarie operazioni aritmetiche. I logici, invece, la sapevano più lunga. Già Leibniz era un sostenitore della notazione binaria. E Turing, nel suo ACE report, sosteneva l’idea che il calcolatore doveva implementare direttamente solo le operazioni più elementari, perché quelle più complesse (come quelle aritmetiche) potevano essere ottenute mediante quella che oggi si chiamerebbe “microprogrammazione”.
Ben scritto, avvincente e conciso.
Ci sono altri libri più approfonditi su questi argomenti; i seguenti sono sempre di divulgazione, tutti e tre veramente belli.
- Turing: the Enigma, di Andrew Hodges. Grandissima biografia.
- Goedel, Escher, Bach: an Eternal Golden Braid, di Douglas Hofstaedter. Labirintico e illuminante viaggio nella logica e nell’intelligenza artificiale.
- Mechanizing Proof, di Donald MacKenzie. Grande compendio sugli sforzi di dimostrare automaticamente la correttezza dei programmi.