Re: [Fsfe-france] Re: Quelques elements supplementaires sur le vote electronique verifie

[Romain d'Alverny]

Le jeu 11/11/2004 à 11:44, Xavier Roche a écrit :
> David MENTRE wrote:
> > Il y a moyen de *prouver mathématiquement* qu'un code est sans bogue,
> > oui, avec du logiciel libre.
> > Question classique : est-ce que je peux avoir confiance dans un
> > compilateur, un assistant de preuve, un OS ?
> 
> Oui, je suis persuadé que l'on peut.

Dans une certaine mesure, seulement.
Un code prouvé sans bogue pourra tout à fait tourner sur du matériel
défectueux. Du matériel prouvé non défectueux pourra tout à fait subir
une avarie.

Et surtout, les règles de probation pourront toujours oublier quelque
chose : un code n'est jamais prouvé que par rapport à des exigences.

Si les exigences sont mal définies, incomplètes par rapport à la tâche
visée par le code, la preuve ne servira pas à grand chose dans les
situations non prévues (voir l'accident d'Ariane V, par exemple ; le
code tournait sur Ariane IV, on a manifestement supposé qu'il tournerait
sans autre problème sur Ariane V).

En la matière, la preuve par le raisonnement demande à être confirmée
par la preuve de l'usage. Le mode de scrutin "urne, bulletin" a été
sensiblement plus expérimenté que le vote électronique.

romain.