Christopher Strachey
Christopher Strachey (1916-1975) a introduit l'idée de sémantique dénotationnelle en théorie de la programmation. Son objectif était d'arriver à des méthodes de preuves de programmes par les mêmes moyens qu'il existe des démonstrations mathématiques de l'exactitude d'une solution.
Des considérations d'informatique théorique aboutissent à l'impossibilité d'arriver à ce résultat pour un programme sur lequel ne s'exerce aucune contrainte (par exemple de taille mémoire). Toutefois, les programmes du monde réel ont une taille finie, bien que grande (dizaines de milliers de lignes).
Christopher Strachey, après avoir montré la possibilité de démontrer certains programmes (en particulier écrits en Smalltalk), est mort sans avoir achevé son œuvre. On travaille aujourd'hui sur deux pistes de démonstrations de programme :
- les unes, concernant les langages procéduraux (comme Pascal ou Eiffel), en imposant des contraintes de contrat à des blocs qui sont ceux de la programmation structurée.
- les autres, concernant les langages fonctionnels comme Haskell, ont une orientation beaucoup plus mathématique (dans un langage fonctionnel, l'ordre où sont écrites les instructions n'a (comme en algèbre) pas d'importance, ce qui rend moins ardu le travail de démonstration.