Lionel Debroux (./65) :
mais absolument pas de prouver qu'un programme est correct

C'est impossible: halting problem

Les langages formels, associés à des compilos certifiés, ont plus de chances de donner du code correct

Ouep, c'est pour cela que pour des applis *vraiment* critiques, l'ADA est souvent utilisé.

Si tu parles des machines de vote...

Du tout; je parlais d'une méthode de vérification. Ce qui est généralement (dans le sens où ils font des vraies vérification, pke c'est rare que tout cela soit fait) utilisé est:
- preuve formelle d'algos
- analyse statique de code source et dynamique
- test de fonctionnalités avec une plus ou moins bonne couverture