Dans cet exposé (entre philosophie de la logique et philosophie de l'informatique), je défendrai l'idée que la notion de programme informatique doit être mise au centre des approches logico-philosophiques de la question sémantique.

Dans une première partie, consacrée à la sémantique des termes, je commencerai par observer que, posée au « texte » d'un programme informatique, la question sémantique se présente en des termes assez différents de ceux auxquels la théorie de la signification d'inspiration frégéenne et le référentiel ensembliste nous ont habitué. En effet, la signification d'un programme informatique ne dépend pas en première instance de la question sémantique usuelle posée aux termes d'individu par la logique, à savoir : « à quoi ce terme réfère-t-il ? », « que désigne-t-il ? », mais de la question préalable « que fait-il ? », « comment agit-il ? ».  Je défendrais l'idée que la prise en compte de la notion intensionnelle de programme dans la question sémantique est d'une part nécessaire, sous peine d'un collapse (partiel) de la notion frégéenne de « sens », d'autre part productrice d'un renversement de la relation de priorité sens / référence.

Dans une seconde partie, consacrée à la sémantique des énoncés, je montrerai comment la « correspondance preuves-programmes » (dont je présenterai schématiquement les linéaments et extensions récente) et l'idée de « propositions-comme-types » permettent d'éviter deux objections qui peuvent être faites à l'idée Dummettienne de sémantique de déplacer le centre de gravité de la théorie de la signification, des énoncés vers leurs preuves.

Dans une troisième partie, je rappellerai comment le point de vue extensionnel qui prévaut dans le référentiel ensembliste peut être reconstruit à partir des notions de terminaison de l'évaluation des programmes (résultats), de (types de) donnée, enfin de cohérence calculatoire.

Je concluerai par une ouverture vers la philosophie du langage.