Citazione:
|
Originalmente inviato da epicurus
Ci sono alcune cose, però, che stonano (sono pignolo, lo so), quindi provo a metterle qui in risalto.
|
avrei dovuto immaginarlo che non l’avrei passata liscia
In linea di massima le tue obiezioni sono corrette, ho esagerato e semplificato un po’ per dare maggiore impatto all’articolo
Citazione:
|
Originalmente inviato da epicurus
E' strano che tu abbia portato proprio questo esempio, infatti Wiles scrisse il suo teorema in linguaggio matematico, e il linguaggio matematico è uno dei linguaggi famosi per il loro rigore e non-ambiguità.
In effetti le dimostrazioni matematiche sono rigorose, il problema è che sono lunghe e complesse, è difficile per un essere umano seguire tutti i punti senza commettere errori.
|
Ho scelto questo esempio proprio perché il linguaggio matematico è notoriamente rigoroso e non ambiguo ... l’idea era di sostenere che persino in questo campo privilegiato la verifica è molto difficile e suscettibile di errori
Citazione:
|
Originalmente inviato da epicurus
la verifica (completa e) automatica del software è un problema non computabile. L'esempio classico è il problema della fermata: non è possibile determinare in modo automatico se un programma generico su input generico terminerà o meno.
Se il programma termina e fornisce i dati attesi, può essere che funzioni su quell'input, ma chi può dirlo in generale per un input qualsiasi? Questo problema è indecidibile.
E' vero che si può fare un'analisi "umana" su un programma e scoprire se terminerà (e funzionerà come deve) oppure no, ma se il programma ha qualche migliaio di righe di codice? Oppure qualche miliardo?
|
Ovviamente in linea di principio hai ragione: ho molto sottostimato la difficoltà della verifica del software. Vi è però un aspetto molto interessante: pare che la “solidità” del software sia notevole, molto maggiore di quanto si potrebbe pensare analizzando le sue procedure di testing. Hai mai sentito di una banca che ha ottenuto dai suoi computer informazioni sbagliate sul conto di un cliente? Le procedure di verifica, però (parlo dell’aspetto ingegneristico della cosa) testano soltanto un sottoinsieme molto piccolo delle possibili condizioni che si potrebbero verificare. Immagino che quando comprimi un file con winzip non ti poni il problema di ritrovarlo corrotto, eppure ovviamente non si sono potute testare tutte le possibili combinazioni di bit in ingresso all’algoritmo di compressione.
Con il software, ad un certo punto “le cose funzionano”. Passata la fase di debugging, e dopo dei test che sono comunque ridicolmente semplici rispetto alla quantità di combinazioni che teoricamente dovrebbero testare, ci si può ragionevolmente fidare.
Citazione:
|
Originalmente inviato da epicurus
Mi sembra che possa confondere mettere sullo stesso piano teorie e programmi.
|
Beh, sono entrambi frutti dell’ingegno umano. Un algoritmo secondo me non è concettualmente molto diverso da una teoria.
