Encore une fois, derrière recherche il y a "tentative de démonstration d'une théorie" et l'informatique ne se démontre pas.
L'informatique est une branche des maths, l'informatique est à base de maths et toute l'informatique c'est des maths.
Or qui dit maths dit démonstration.
Allez, on va sortir les gros morceaux de la calculabilité (discipline fondamentale de l'informatique), avec le modèle de Turing (machine de Turing), comment on démontre que les machines de type RAM (le PC en est une) est également une machine de Turing.
On sort également la preuve qu'il n'existe pas d'antivirus (application du théorème diagonal de Gödel) ou qu'il est impossible de prouver en un temps raisonnable et de façon automatique qu'un programme de la machine de Turing est correct (vérification de code?).
Inutile? ultra utile au contraire! car tu va chercher une sémantique de langage de programmation qui sera (presque) aussi expressive que la machine de Turing, tout en se restraignant à la partie qui est prouvable de façon automatique.
Si tu n'a pas envie de changer de langage, alors on va appliquer des outils de vérification de code qui vont vérifier que 1. tu restes dans cette restriction qui est prouvable et 2. que la preuve est correcte.
Allons un peu plus loin: la démonstration est nécessaire: tu accepterais de monter dans un avion si son logiciel n'était pas prouvé correct?
Toute l'informatique est une histoire de démonstration. Les mauvais informaticiens sont le plus souvent de mauvais mathématiciens.
[^] # Re: Dommage...
Posté par Jean-Baptiste Mayer . En réponse à la dépêche OCaml 3.10.0 est sorti. Évalué à 5.
L'informatique est une branche des maths, l'informatique est à base de maths et toute l'informatique c'est des maths.
Or qui dit maths dit démonstration.
Allez, on va sortir les gros morceaux de la calculabilité (discipline fondamentale de l'informatique), avec le modèle de Turing (machine de Turing), comment on démontre que les machines de type RAM (le PC en est une) est également une machine de Turing.
On sort également la preuve qu'il n'existe pas d'antivirus (application du théorème diagonal de Gödel) ou qu'il est impossible de prouver en un temps raisonnable et de façon automatique qu'un programme de la machine de Turing est correct (vérification de code?).
Inutile? ultra utile au contraire! car tu va chercher une sémantique de langage de programmation qui sera (presque) aussi expressive que la machine de Turing, tout en se restraignant à la partie qui est prouvable de façon automatique.
Si tu n'a pas envie de changer de langage, alors on va appliquer des outils de vérification de code qui vont vérifier que 1. tu restes dans cette restriction qui est prouvable et 2. que la preuve est correcte.
Allons un peu plus loin: la démonstration est nécessaire: tu accepterais de monter dans un avion si son logiciel n'était pas prouvé correct?
Toute l'informatique est une histoire de démonstration. Les mauvais informaticiens sont le plus souvent de mauvais mathématiciens.