La programmation des ordinateurs trouve son cadre formel dans des résultats qui les ont largement précédé et qui viennent de la formalisation de la notion de fonction effectivement calculable. Ce cadre formel fixe les limites de ce qui peut être programmé, des propriétés des programmes qui peuvent être prouvées et de la complexité des problèmes à faire résoudre par des programmes. L'étude de la complexité a bien sûr connu des développements importants après l'avènement des ordinateurs, mais la préoccupation existait bien avant eux.
Sauf rare exception
(par exemple, modèle de programmation fondé sur la mécanique quantique),
la recherche en programmation n'a pas pour objet de repousser ces limites,
mais plutôt de mieux les occuper.
Cela signifie essentiellement mieux utiliser les ressources,
machines, temps, hommes, argent,
à la fois lors de la production des programmes et lors de leur
exploitation.
Nous prenons
«mieux utiliser les ressources» dans un sens très large qui
comprend aussi «ne pas causer de catastrophes».
En particulier,
mieux utiliser les ressources lors de l'exploitation
est crucial lorsque la programmation est au c
ur d'un système vital.
Il s'agit alors de diminuer les risques pour les individus ou la société.
Que ce soit à propos de la production des programmes ou de leur exploitation, le discours des chercheurs mélange des considérations purement formelles et des considérations qui prennent en compte le facteur humain. Le typage en programmation illustre bien cette dualité. Que le typage permette une vérification formelle d'une propriété des programmes est incontestable, mais que cette propriété soit utile relève plus d'un acte de foi. On peut se convaincre qu'il s'agit d'une propriété utile en se plaçant sur le versant technologique de la programmation, et en constatant que beaucoup d'autres disciplines technologiques classifient et normalisent des concepts intermédiaires afin d'assurer qu'on peut les composer correctement. C'est ce que la programmation fait avec les types. On peut aussi se placer sur le versant expérimental et répertorier les erreurs couramment commises par les programmeurs, et constater que la propriété de bon typage en élimine quelques unes. Finalement, sur le versant fondamental, la formalisation des types montre que certaines tâches de programmation sont automatisables.
La recherche en programmation est donc une discipline à deux visages :
formalisation et prise en compte du facteur humain.
Son second visage est souvent traité cavalièrement.
Par exemple,
on voit beaucoup plus souvent qualifier un programme de lisible,
ou même de plus lisible qu'un autre,
que définir la notion de lisibilité,
ou l'expressivité, ou la maintenabilité, etc.
Cette discipline est donc aussi riche en débats sans réelle conclusion :
on peut lire par exemple
«Goto Statement Considered Harmful»
[Dijkstra 68]
et les débats qui ont suivi
dans la revue de l´
(Association for Computing Machinery).
Une grande partie de la recherche en programmation s'exerce sur les langages de programmation eux-mêmes. En effet, un langage de programmation n'est pas un outil neutre et interchangeable. Nous allons le montrer à propos de trois aspects de leur rôle : la discipline de programmation, le schéma d'évaluation, la méthode de programmation. Sous le nom de «discipline de programmation» nous entendons ce qui a trait à l'écriture des programmes, alors que sous le nom de «méthode de programmation» nous entendons ce qui a trait à l'environnement de programmation.