Exactement, pour avoir encore plus confiance dans le programme codé, il faut regarder du coté de la preuve formelle, par exemple le programme coq pour OCaml : http://coq.inria.fr/(...)
Mais meme si un tel systeme te permet de prouver que ton programme suit exactement le specs, rien ne prouve que les specs ne comportent pas de 'bugs' (erreurs, comportement pas prévu), meme si en théorie les specs doivent etre plus simple à comprendre que le programme lui meme.
[^] # Re: pas une preuve
Posté par Olivier Grisel (site web personnel) . En réponse au journal couverture de code. Évalué à 3.
Mais meme si un tel systeme te permet de prouver que ton programme suit exactement le specs, rien ne prouve que les specs ne comportent pas de 'bugs' (erreurs, comportement pas prévu), meme si en théorie les specs doivent etre plus simple à comprendre que le programme lui meme.