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

[François TOURDE]

Le 12733ième jour après Epoch,
David MENTRE écrivait:

> Bonjour,
>
[...]
> Pour répondre aux questions de Benoît :
>
>> Pourquoi le code de l'urne n'est-il pas publique ?
>
> Il faut évidemment qu'un tel code soit public.

Totalement d'accord.

>
>> Et s'il était public, serait-il pour autant fiable/sans bogue ?
>
> Il y a moyen de *prouver mathématiquement* qu'un code est sans bogue,
> oui, avec du logiciel libre.

Du haut de mes maigres compétences en algo non numérique, je sais que
c'est possible (j'ai eu à le faire en TP il y a ... ans :( ) mais
c'est aussi un travail colossal ! Sauf si:

> Pour l'instant, trois axes me semblent possibles :
>
>  - vérifier un code C avec Caduceus et Why (http://why.lri.fr/), puis
>    Coq (http://coq.inria.fr/) ;
>
>  - vérifier un code common-lisp avec ACL2
>    (http://www.cs.utexas.edu/users/moore/acl2/) ;
>
>  - dériver un programme OCaml prouvé correct à partir de preuves
>    formelles, soit directement dans Coq, soit en utilisant Focal
>    (http://caml.inria.fr/archives/200410/msg00182.html).

Mais il faut auparavant démontrer le code des divers vérificateurs. Ça
va bien au dela du "souci" qu'il y a eu avec le théorème des 4
couleurs.

Et du point de vue du grand public, ça semble AMHA totalement
inutile. Ça s'apparente à faire confiance à une bande de techos du
même accabit que ceux qui disent que l'amiante n'est pas dangereuse,
que le nuage de Tchernobyl s'est arrêté aux frontières de la france,
etc.

Mes 2¢

PS: La citation ci-dessous est totalement aléatoire (au sens de la
fonction random d'un ordinateur), mais totalement bienvenue ici ;)

-- 
May you do Good Magic with Perl.
             -- Larry Wall's blessing

pgpCd6Q6a6R2p.pgp
Description: PGP signature