Informatique et Sciences du Numérique au lycée : un pas plus loin/LANGAGES/Théorie des Types et Assistants de Preuve

Page en cours de construction, à partir de fragments des pages citées dans le texte ci-dessous.

L'intuitionnisme est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une alternative à l'approche dite classique. Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting. Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique. Gerhard Gentzen en a formulé les règles de déduction dans le cadre de la déduction naturelle.

Les travaux récents, notamment la correspondance de Curry-Howard, lui ont donné un statut central dans la logique et dans l'informatique, en faisant d'elle historiquement la première des logiques constructives. Des travaux la concernant, effectués par Gödel et Andreï Kolmogorov au sujet de la « non-non interprétation » (interprétation de la double négation) ont ouvert la porte de l’interprétation de la logique classique dans les termes de la logique intuitionniste. L'étude de la logique intuitionniste est la clé pour bien comprendre la logique classique et ses subtilités.

Les assistants de preuve sont des logiciels qui permettent de démontrer des théorèmes énoncés dans la logique (en général d'ordre supérieur) qui constitue leur fondement. Ils sont utilisés en informatique pour démontrer la validité de propriétés de programmes ou de systèmes. Par exemple, certaines propriétés de résistance à des intrusions de systèmes embarqués ont été démontrées en utilisant de tels systèmes.