[tc] [OT]Re: lettera alla commissione europea

[167_]

Il giorno mar, 31/10/2006 alle 23.42 +0100, Luca Brivio ha scritto:
> Il giorno Tue, 31 Oct 2006 19:06:35 +0100
> Davide Prina <DavidePrina a email.it> ha scritto:
> 
> > > a) nessuno leggendo un programma può essere sicuro che non contiene
> > > errori o codici malevoli. Ci sono molti risultati formali della
> > > logica-matematica che hanno dimostrato questo.
> > 
> > veramente è stato dimostrato che non è possibile dimostrare la 
> > correttezza formale di un algoritmo, se non ricordo male si dice che
> > è un problema NP-completo.
> 
> Se è un problema NP-completo per definizione ha una soluzione. Il che
> non esclude che essa possa essere impraticabile sopra una certa
> complessità dell'algoritmo.
> 
> Tutto questo non so che cosa abbia a che fare con i bug...
in realta ci sono due grossi risultati che mettono in luce
l'inadeguatezzza della logica e dunque  la impossibilità di verifcare
formalmente in maniera automatica che un programma abbia una certa
semantica  (operazionale o denotazionale che sia ):
1) il teorema di incompletezza di godel
2) (derivabile dal punto 1 )il fatto che non esiste un algoritmo che ti
dice se un programma termine (tale problema e' in realta semidecidibile:
l'algortimo migliore ti puo rispondere SI o puo' bloccarsi senza fornire
risposta .)