Le problème en informatique, c'est que tout le monde écrit des programmes. Il m'apparaît maintenant clair que nous devrions écrire des spécifications. Juste donner la sémantique, les lois qui régissent l'interaction des paramètres. On peut alors rêver d'un compilateur futur qui pourra trouver une implémentation performante, pourquoi pas à l'aide de programmation génétique.
Finalement, spécifier c'est un peu ce que nous croyons faire : on croit grâce à un langage particulier décrire un problème à l'ordinateur et lui demander de le résoudre. En réalité on se plie à une sémantique arbitraire qui agit plus qu'elle ne comprend le problème. On ne fait que coller de bout en bout des instructions machines. Le code ne décrit pas la sémantique du problème mais juste une de ses nombreuses solutions, idéalement la meilleure. Mais la meilleure solution pour un certain ensemble de données n'est pas forcément la meilleure pour un autre. Cette méthode manque d'agilité par son manque de compréhension sémantique du problème.
L'énorme boulot de l'architecture et du développement logiciel réside dans les interfaces et leurs protocoles. C'est ce fait le succès des middleware et autres IDL : ils décrivent et normalisent les interfaces de communication entre les différents modules et programmes et permettent presque d'oublier qu'ils sont séparés. Le problème en informatique c'est qu'on décrit des interfaces mais il est clair qu'on devrait écrire des spécifications de ces interfaces. On devrait décrire la sémantique de l'interaction de ces interfaces. On ne fait que coller les unes aux autres des définitions d'interfaces. La spécification ne décrit pas la sémantique du problème mais juste un découpage des fonctionnalités, idéalement le meilleur. Mais le meilleur découpage pour un certain domaine d'application n'est pas forcément le meilleur pour un autre. Cette méthode manque d'agilité par son manque de compréhension de la sémantique du problème.
Le développement actuel de l'informatique suit cette voie : l'étude des systèmes de typage correspond effectivement à la spécification sémantique d'un problème abstrait. La production d'un programme qui répond à ce typage correspond alors formellement à une preuve du problème théorique (c'est la fameuse correspondance de Curry-Howard). Il existe déjà une foule de programmes de preuve de théorèmes : HOL, Coq, ACL2 pour ne citer qu'eux. Je comprends maintenant que ce sont les racines des compilateurs du futur. Ils seront capable de produire le code optimal pour un ensemble de contraintes données par un utilisateur pas forcément très au courant des basses réalités électroniques. Finalement les histoires d'opérations de bits ça n'a jamais passionné personne hein ? Oui en fait il y en a, mais avouons que nous sommes d'un genre bizarre... ;)