Re: [OT] software ed errori [Era: OpenSSL: Altro bug]
Ciao,
Il Mer, 11 Giugno 2014 10:01 pm, franchi@modula.net ha scritto:
> Il 10/06/2014 20:14, bodrato@mail.dm.unipi.it ha scritto:
>>>> ahi, ahi, ahi... top quoting... questo è male ;-)
> Così' va meglio?
Decisamente :-)
> Voglio aggiungere un pò di teoria dell'errore: una misura empirica non è
> mai corretta.
Sarebbe interessante sapere quale definizione daresti di "misura
corretta", ma finiremmo più fuori-luogo (OT) di quanto siamo già...
>> 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!
> E' il "quasi completamente" che (mi) dà fastidio. Peraltro occorrerebbe
Dagli tempo. Fino qualche mese fa una delle parti non certificate era il
parser, dalla versione del mese scorso lo è.
> A meno che il sistema di certificazione (umano o artificiale poco
> importa) non riesca a certificare anche sé stesso: però la vedo dura
> [Kurt Godel].
Povero Gödel, dopo aver dimostrato teoremi di così grande interesse,
finisce per esser troppo spesso citato da chi vuol sminuire il ruolo della
dimostrazione formale...
Ricordiamo almeno che ciò che in modelli infiniti è indecidibile, non
può esserlo in modelli finiti. O vogliamo applicare i teoremi di Gödel,
Turing e compagnia anche dove le loro ipotesi di partenza non valgono?
Se qualcuno mi presentasse la dimostrazione formale di correttezza di un
programma, valida solo se questo viene fatto girare su una macchina con
meno di un petabyte di memoria e finché il totale dei dati trasmessi non
supera lo yottabyte... personalmente mi accontenterei :-)
> Quindi cari colleghi programmatori, mettettetevi il cuore in pace e
> rassegnatevi al vostro destino di cacciatori di insetti (io l'ho già
Forse, ma non senza raffinare gli strumenti ausiliari, come ad esempio i
banali coretori ortografici :-D
Buona giornata,
m
--
http://bodrato.it/papers/
Reply to: