Ciao, Innanzitutto cito Davide...
> Il 09/06/2014 21:49, Davide Prina ha scritto: >> ahi, ahi, ahi... top quoting... questo è male ;-) >> >> fare il top quoting impedisce una corretta lettura del discorso e >> causa una difficile risposta. Ora veniamo al dunque. Il Mar, 10 Giugno 2014 9:38 am, [email protected] ha scritto: > Non importa se poi l'errore è del tuo comando o della shell o di chissà > cosa: il fatto è che il sistema, nel suo complesso, può produrre > risultati diversi da quelli che ci aspettiamo. Invece importa, se l'errore non è nel mio comando, non puoi imputare il bug al mio software. Inoltre non bisogna confondere i bug dagli errori estemporanei. Se un surriscaldamento, un raggio cosmico o un altro evento del genere possono generare errori imprevedibili nell'esecuzione di un software, questo non significa che il software abbia bug (anche se certamente è possibile scrivere software più resiliente di altri nei confronti di eventi del genere). Il bug di OpenSSL da cui è partita questa discussione era tale che, al verificarsi di un evento riproducibile a volontà, OpenSSL _sistematicamente_ e _prevedibilmente_ permetteva di aprire una falla di sicurezza, indipendentemente da errori di compilazione, hardware malfunzionante o simili "incidenti"... Di questo stiamo parlando. > se meriterebbe rifletterci): voglio solo dire che la complessità del > software non è completamente dominabile e che anche in questo campo si > procede per errori e correzioni come in qualsiasi altro ambito > scientifico. Io penso si debba distinguere tra scienza e tecnologia. Forse la tecnologia procede per errori e correzioni, non mi pronuncio. La scienza dovrebbe procedere per teorie, verifiche e dimostrazioni; chi commette errori grossolani di solito non usa il metodo scientifico e magari ha finge di poter estendere la validità di una teoria al di fuori del suo ambito di applicazione. Tanto per fare un esempio in breve, dire una cosa come "la meccanica relativistica Einsteiniana è la versione corretta della meccanica classica di Galileo e Newton che era un errore" sarebbe una sciocchezza. La meccanica classica continua a fornire previsioni attendibili se le masse, i tempi, gli spazi e le velocità in gioco, assieme alla precisione richiesta dalla previsione non eccedono certi limiti. Scommetto che chi progetta mezzi di trasporto terrestri continua (correttamente) ad usarla senza tener conto delle "correzioni" relativistiche. Scommetto anche che chi progetta la traiettoria di "astronavi" usa la meccanica Einsteiniana e non la quantistica... e chi... etc etc. Un esempio più informatico potrebbe essere l'articolo di chi ha proposto i B-heap [ http://queue.acm.org/detail.cfm?id=1814327 ]. L'autore fa notare che per i computer moderni non è valida l'ipotesi di costo costante per un accesso in memoria indipendentemente dalla locazione, ne conclude quindi che usare la teoria classica per implementare un heap, oggi, è sbagliato. Anche in questo caso sarebbe sciocco dire che quella teoria contiene un errore, quando questo è nel suo uso (tecnologico?) fuori dalle ipotesi. Detto questo, le teorie scientifiche restano certamente tutte falsificabili, lungi da me sostenere che affermino "la verità". Descrivre però il metodo scientifico come "errori e correzioni" è un po' riduttivo. >> meglio dire che non esiste un metodo automatico che possa essere usato >> per dimostrare la correttezza di un software qualsiasi. Questa frase è di Davide (infatti concordo ;-); giustamente non esclude la possibilità di dimostrare la correttezza di software specifici! Anche qui, vale la pena fare un esempio, magari un po' più significativo del "return 0"... va bene un intero compilatore? Non è software libero (ha una clausola che ne esclude l'uso commerciale; anche se ampie porzioni del codice sono rilasciate con doppia licenza, talvolta affiancando la BSD, talaltra GPL o LGPL) ma bisogna ammettere che CompCert [ http://compcert.inria.fr/ ] è un progetto estremamente interessante: si tratta di un compilatore la cui correttezza è (quasi completamente) certificata da sistemi di dimostrazione automatica! Certo, scrivere oltre al software (e alla documentazione :-) anche il sistema di teoremi che ne dimostrano la correttezza richiede _MOLTO_ più tempo che andare per tentativi affidandosi alla propria esperienza e alle revisione di colleghi e (nel caso del software libero) volenterosi per commettere meno errori possibile. Si può certamente sostenere (ci sono validi argomenti a supporto) che per software "troppo" complessi, che devono anche velocemente adattarsi alle innovazioni tecnologiche (come OpenSSL), l'approccio della dimostrazione automatica sia impraticabile... Bisogna però ammettere che c'è gente tutt'altro che ignorante che usa un approccio (davvero) scientifico per scrivere software con certificazione della correttezza. Per installare il compilatore citato, bisogna scaricare dal sito il sorgente (verificare l'impronta hash); aver installato gcc, coq, menhir, ocaml; eseguire "./configure <opzioni> && make" e ... aspettare un tempo piuttosto lungo che tutti i teoremi necessari vengano dimostrati ;-) Buon divertimento ;-) m -- http://bodrato.it/papers/ -- Per REVOCARE l'iscrizione alla lista, inviare un email a [email protected] con oggetto "unsubscribe". Per problemi inviare un email in INGLESE a [email protected] To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: https://lists.debian.org/[email protected]
