L’informatique est-elle logique ?

19.05.2014 | par Thierry Vieville | Uncategorized

L'informatique est une science, soit. Mais alors quel est son lien avec la logique cette étude des règles formelles de tout raisonnement ?

« C’est peut-être pas très logique, mais il n’y a pas qu’une seule logique ! Selon ce qu’on accepte comme mécanisme de raisonnement, on peut définir différentes logiques. Parmi elles, il y a la logique dite classique des mathématiciens ou la logique dite intuitionniste des informaticiens. Enfin pas tout à fait non plus : les deux sciences informatiques et mathématiques ne se privent pas d’utiliser les deux, et de... » et un jeune doctorant en science informatique de nous faire découvrir ces différences sous forme d'une petite histoire,  une petite histoire pas très logique de la logique. Donnons la parole à l'auteur de ce joli texte didactique, Guillaume Cano.

Ce qui est très intéressant dans ce texte, c'est qu'il nous emmène avec humour découvrir qu'il y a plusieurs logiques possibles, la classique des mathématiques que nous avons fait au lycée ou la logique dite intuitionniste plus utilisée par les informaticiens. Et pour nous permettre de bien comprendre cela il nous refait faire le chemin qui nous a permis de découvrir qu'une proposition comme une phrase affirmative à laquelle on peut donner une valeur de vérité, que l'on ne s'occuper pas du sens des propositions, mais de construire de nouvelles propositions à partir de propositions qui existent déjà,  avec des opérateurs logiques.

Le levier de cette logique intuitionniste c'est qu'une proposition peut-être considérée comme vraie seulement si on construit une preuve, donc si on peut la construire  à partir des règles définies pour les opérateurs  logiques. La logique devient un mécanisme de pensée algorithmique.

Où est le point dur alors ? Celui de décider si une proposition est-elle obligatoirement soit "vraie" soit "fausse" ? On parle de tiers exclu car cela revient à dire qu’une proposition ne peut avoir que deux valeurs de vérité : vrai ou faux, et qu’il n’existe pas de tierce possibilité. Utiliser cet axiome est bien pratique pour démontrer qu'une proposition est fausse car elle n'est pas vraie ou l'inverse. Mais on obtient alors des résultats de type «il existe un élément qui a telle propriété». Et quand on demande, «certes, mais comment le construire, cet élément ?», alors le logicien classique répond «ah ben, aucune idée, je dis juste qu'il ne peut pas ne pas exister».

Pas très logique ? Allons lire ce que nous propose Guillaume Cano : http://images.math.cnrs.fr/Une-petite-histoire-pas-tres.html

Est-ce que ça marche ?  regardons un exemple.

Un exemple de logiciel d'assistance à la preuve: COQ.

Loin d'être une posture théorique, c'est cette révision de la logique classique qui permet de développer des méthodes de preuve par ordinateur. Et à inventer des mécanismes de vérification des algorithmes. Bref : à éviter les bugs [1]. Gilles Kahn qui as contribué à élucider le bug probablement le plus célèbre de l'histoire industrielle [2], serais content de voir nos systèmes de carte à puce ou des systèmes robotiques au service de la chirurgie, protégés directement ou indirectement par ces méthodes formelles, qui permettent de garantir le bon fonctionnement logiciel. Les collègues qui travaillent sur un tel système viennent de recevoir, le , une des plus prestigieuses distinctions scientifiques pour ce travail [3]. Ce logiciel permet interactivement de construire de telles preuves en manipulant des assertions logiques en utilisant des outils d'aide à la recherche de preuves formelles et de synthétiser des programmes certifiés à partir de preuve [4]. D'autres logiciels comme Isabelle, HOL Light sont aussi des assistants de preuve.

Comment expliquer simplement en quoi tes travaux sont si novateurs ? On pourrait dire très simplement dire cela contribue à «donner du sens» aux langages de programmation. On peut avec tes formalismes manipuler un programme comme une formule mathématique, donc calculer des propriétés liées à ce qu'il va faire (ou pas). On ne se contente donc pas de vérifier que le programme est syntaxiquement correct (c'est à dire que la machine va être en mesure de le traduire pour l'exécuter). On vérifie aussi qu'il correspond aux spécifications que le concepteur s'était donné. Ces idées permettent donc de prouver mécaniquement (automatiquement ou interactivement), de certifier, les éléments de sens (sémantiques donc) liés au code que le programmeur se propose de réaliser.

[1] http://www-sop.inria.fr/marelle
[2] https://fr.wikipedia.org/wiki/Vol_501_d%27Ariane_5
[3] http://coq.inria.fr/coq-received-acm-sigplan-programming-languages-software-2013-award
[4] https://fr.wikipedia.org/wiki/Coq_%28logiciel%29


2 commentaires pour “L’informatique est-elle logique ?”

  1. patricedusud Répondre | Permalink

    Merci pour le lien sur l'article de Guillaume Cano. Au passage l'ordinateur ternaire outre d'avoir une base plus "économe" que la base binaire pouvait plus facilement implémenter la logique intuitionniste à trois états ...

Publier un commentaire