Mon programme est-il correct ?

Un programme (et plus généralement un système matériel ou logiciel) est dit correct (ou valide) lorsqu’il fait «ce qu’on veut qu’il fasse», et rien d’autre. Encore faut-il définir «ce qu’on veut qu’il fasse», autrement dit sa spécification, ce qui est moins facile qu’il n'y paraît à première vue.
La validité des programmes est un problème central de l’informatique. Maurice Wilkes, un pionnier de l’informatique, l’avait bien vu dès 1949 lorsqu’il disait, après avoir réalisé l’EDSAC, premier ordinateur à programme enregistré, et écrit ses premiers programmes : «Je pris conscience, et cette révélation me frappa avec toute sa force, que j’allais passer une bonne partie du restant de ma vie à trouver des erreurs dans mes propres programmes».
Vers le début des années 1960, on pensait que l’invention des langages de programmation de haut niveau allait résoudre le problème de l’écriture de programmes corrects ; on parlait alors de «programmation automatique» et certains annonçaient même la fin prochaine du métier de programmeur. Il fallut peu d’années pour dissiper ces illusions : de grands projets informatiques dépassaient leur budget, prenaient des mois de retard, et échouaient à rendre le service requis ; le système d’exploitation OS/360, le programme le plus complexe existant à cette époque, contenait un millier d’erreurs, et on considérait comme un exploit le fait de ne pas augmenter ce nombre à chaque sortie d’une nouvelle version. On parla alors de «crise du logiciel».
Cette prise de conscience conduisit en 1969-70 à l’idée que la programmation devait passer d’un stade artisanal à un stade industriel et s’appuyer sur des fondements scientifiques, à l’instar d'autres domaines de l’ingénierie : génie civil, génie chimique, génie électrique. Ce fut la naissance du génie logiciel. Mais il ne suffisait pas d’inventer un nouveau terme, encore fallait-il lui donner un contenu. Le génie logiciel recouvre l’ensemble des techniques nécessaires à la construction raisonnée de systèmes logiciels. La validité des programmes en est un aspect important, mais ce n’est pas le seul.
La suite de ce parcours est dédiée aux méthodes et outils développés pour assurer la validité des programmes.