Je vois bien que l’on est d’accord sur le fond, mais sur la forme, non ce n’est pas cela la preuve formelle.
Vous donnez l’impression de confondre validation du fonctionnement d’un logiciel et preuve formelle d’un théorème ou algorithme.
La preuve formelle consiste à prouver que si les hypothèses sont respectées, le résultat est obtenu au bout d’un temps fini et est correct.
Tout ce qui est en dehors des spécifications est également en dehors de la preuve formelle.
On ne sais pas toujours le faire et/ou il est souvent inutile de le faire (car coûteux), mais on peut prouver qu’un algorithme respecte toute les propriétés que l’on a formulées.
Là où vous voulez en venir je pense, c’est que pour prouver formellement qu’un programme réponde à notre besoin, il faudrait être capable de formuler exactement notre besoin, et c’est cela qu’on ne sait pas faire.
On peut prouver que certains programmes font ce qu’on leur demande de faire, mais on ne peut prouver qu’il « fonctionne » sans avoir défini ce que « fonctionner » voulait dire.
Dans le cas du bitcoin :
- Le wallet repose sur un clef public/privée à ma connaissance on ne peut prouver par exemple qu’il est impossible de trouver la clef privée à partir de la clef public (+ un certains nombre de transactions). Au mieux on pourrait peut être prouver qu’il faut beaucoup trop de temps pour le faire pour que cela soit réaliste.
- Mais même si on prouvait que le vol de bitcoin est impossible (sans vol de la clef privé), ça ne voudrait pas pour autant dire que c’est une bonne monnaie puisque l’on ne sait pas définir toutes les propriétés que doit avoir une bonne monnaie.