Le passage de Rice à "les mathématiques ne sont pas possibles"
Je n'ai jamais dis ça. J'ai dis l'usage des mathématiques est en pratique impossible pour prouver des programmes non triviaux.
En pratique, on ne peut pas pas prouver les programmes à la main, cela prendrait beaucoup trop de temps quand bien même ce serait possible. On ne va pas ressortir les exemple d'Ariane 5 et du Rover de Mars dont les code étaient tout petits par rapport à ce qu'il se fait dans l'industrie et qui pourtant n'ont jamais été prouvé mathématiquement car c'est simplement trop lourds.
Le seul espoir aurait été de tout vérifier automatiquement mais ce n'est pas possible (Rice). Donc en pratique en sûreté de fonctionnement on prouve certes deux trois truc, on fait de nombreux tests, du model checking de l'injection de fautes, de la supervision, etc sans jamais avoir de garanties.
Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par Diagonale de Cantor (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 3.
Je n'ai jamais dis ça. J'ai dis l'usage des mathématiques est en pratique impossible pour prouver des programmes non triviaux.
En pratique, on ne peut pas pas prouver les programmes à la main, cela prendrait beaucoup trop de temps quand bien même ce serait possible. On ne va pas ressortir les exemple d'Ariane 5 et du Rover de Mars dont les code étaient tout petits par rapport à ce qu'il se fait dans l'industrie et qui pourtant n'ont jamais été prouvé mathématiquement car c'est simplement trop lourds.
Le seul espoir aurait été de tout vérifier automatiquement mais ce n'est pas possible (Rice). Donc en pratique en sûreté de fonctionnement on prouve certes deux trois truc, on fait de nombreux tests, du model checking de l'injection de fautes, de la supervision, etc sans jamais avoir de garanties.
Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.