Software perfetto
Posted on April 8, 2005
Filed Under Articles |
Non so perché, ma lavorando con i computer e parlando sempre in portoghese mi vengono in mente ricordi lontani, come quello di quando mio zio mi spiegò la numerazione in base due. Ieri mi è venuta in mente una vacanza a Palermo con un mio collega di università, Marco, nel 1989. Eravamo entrambi studenti di ingegneria (io sarei scappato verso fisica pochi mesi dopo) e intrippati con la matematica. A Palermo fummo ospitati da Franco e Vera (sì, anche loro zii…). Franco è un ingegnere che si rivelò un appassionato matematico: passammo una serata mangiando pesce e parlando di Russel, Hilbert, Bourbaki e Godel, dei fondamenti della matematica, del programma di Hilbert. Il programma di Hilbert era di riuscire a formulare la matematica in maniera solida e completamente logica. Poi arrivò Godel che mostrò che era impossibile.
Anche se il programma di Hilbert sa un po’ di positivismo (la mente umana, la *ragione umana* può tutto se ben utilizzata) è affascinante. Chiunque abbia provato un minimo piacere dopo aver dimostrato il teorema di Pitagora, alle medie, può capire la bellezza della dimostrazione matematica: sminuzzare in tanti pezzetti logici un grande passaggio che intuitivamente sentiamo vero e arrivare a dimostrarlo. Come scalare una montagna con le nostre forze, centimetro per centimetro, visto che non ce la facciamo ad arrivarci d’un balzo.
Sarebbe lo stesso arrivarci con la funivia?
Direi di no, ma comunque salire con l’aiuto della funivia dà un certo piacere.
Che direste di qualcuno che invece di spezzettare la dimostrazione in un numero accettabile di passaggi logici percorribili da mente umana la spezzettasse in 10.000 passaggi, e facesse percorrere questi passaggi da un computer? Beh, un po’ come la funivia, ma bisogna accettarlo. Nel 1976 due matematici americani, Appel e Harken, dimostrarono il teorema dei 4 colori (qualsiasi mappa può essere disegnata con non più di 4 colori e non ci saranno due paesi confinanti con lo stesso colore) con l’aiuto del computer. Una volta capito come fu utilizzato il computer per questa dimostrazione non si può obbiettare che la dimostrazione non è valida perche’ utilizza il computer: in realtà la mente umana gioca ancora un ruolo fondamentale, e il computer fa solo passaggi noiosi ma chiaramente banali.
Ora il teorema dei 4 colori è stato ri-dimostrato da un francese, un matematico di nome Gonthier che vive negli USA, utilizzando esclusivamente un “pacchetto software” al cui sviluppo aveva anche lui collaborato. La differenza con i due colleghi americani e` che Gonthier ha usato solo il software per mostrare che un’altra dimostrazione era corretta.
Chiunque abbia programmato sa che lo stesso programma, compilato anche sulla stessa macchina due volte, può dare risultati leggermente diversi. Anche a chi non programma è capitato che lo stesso programma abbia dato due risultati diversi. Ma alla fine tutti crediamo che una dimostrazione fatta col computer sia giusta. Insomma per tutto il 1800 i filosofi pensavano che comportandoci razionalmente avremmo avuto una società perfetta, all’inizio del 1900 che la mente umana potesse arrivare a creare un sistema logico (quindi astratto) perfetto, e nel 2000 siamo arrivati finalmente alla conclusione che l’uomo è imperfetto ma il computer no, lui non sbaglia.
[Per inciso ho perso gli ultimi due giorni cercando di installare stampanti. Chiaramente sono io che sbaglio… tipo di lavoro.]
Riusciamo insomma, noi imperfetti, a costruire programmi perfetti, senza errori! Il dott. Gonthier e il laboratorio di ricerca per cui lavora vogliono arrivare a convincerci di questo. Dicono “Se il mio computer dimostra, solo soletto, un teorema che io so essere vero e che l’uomo ci ha messo piu` di un secolo a dimostrare, evidentemente il programma che utilizzo è privo di errori.”
Ricordatevi questo nome, insomma, la prossima volta che il vostro computer (se con Windows) si blocca e mostra uno schermo blu con strane scritte (Il programma ha letto la memoria 0×2134762 che e` di sola lettura…). E sappiate due cose:
1) i tecnici della Microsoft stanno cercando *da anni* di creare qualcosa di più accattivante di uno schermo blu in caso di panico del computer
2) i laboratori di ricerca per cui lavora il dott. Gonthier sono i “Microsoft Research Labs.”
P.S. Non che io pensi che il software libero sia privo di bachi (errori), anzi. Ecco cosa scriveva l’autore del programma (libero) FVWM nel sorgente (parafraso):
“Scopro in media 5 bachi al mese nel mio programma. Poiche’ in media solo il 10% dei bachi viene scoperto vuol dire che ogni mese produco 50 bachi. Dubito che questo programma sarà mai perfetto”
Comments
Leave a Reply
Subscribe via RSS