Un cercle vicieux

Depuis longtemps, il est question en informatique de preuve algorithmique, c'est à dire de la possibilité de démontrer de façon catégorique la fiabilité d'une partie d'un programme. Cela ne concerne pas des tests plus ou moins exhaustifs sur le logiciel mais des formulations mathématiques permettant de dire en une seule opération s'il fera ce qui est attendu de lui. Que cela nécessite une certaine intervention humaine (d'où tout de même possibilité d'erreurs) ou soit automatique, que la démarche consiste à montrer la validité d'un algorithme déjà formulé ou à faire intervenir des règles dans sa conception même pour ne plus avoir à le prouver une fois terminé, des problèmes apparaissent. En effet, quand la complexité de l'algorithme augmente celle de la vérification aussi, et pas forcément de façon simplement proportionnelle, ce qui amène des difficultés quand il s'agit de prouver un logiciel complet.

De toute façon, même si on arrive à démontrer la validité des algorithmes d'une application entière et de leurs interconnexions, cela ne suffit pas. En effet, comme c'est presque à coup sûr un langage évolué qui sera utilisé pour l'écrire (ne soyons pas maso), il faudrait démontrer de la même manière la fiabilité du compilateur et de la bibliothèque de fonctions nécessaires pour obtenir l'exécutable (ce qui ne serait pas un mince affaire), ou même de plusieurs compilateurs s'il doit être porté.

Sans s'attarder sur le système d'exploitation auquel certaines des fonctions feront appel, même le processeur de la machine peut poser problème (ça s'est vu) et comme des logiciels spécialisés sont évidemment nécessaires pour concevoir des circuits réunissant plusieurs millions de transistors, il faudrait non seulement prouver leur fiabilité mais aussi être sûr que les modélisations mises en pratique soient suffisamment fines.

En conclusion, il n'est pas possible de démontrer avec certitude la fiabilité d'un logiciel mais on sait minimiser (efficacement) les risques qu'il comporte des erreurs.