En fait, je ne vois pas pourquoi l'informatique serait plus une branche des mathématiques que la physique.
Pour la simple est bonne raison que, contrairement à la physique, elle n'emprunte aucun de ses principes à l'expérience : c'est une science pure et formelle. Du moins je me place du point de vue où l'on cherche à la considérer comme une science et non comme une simple technique. ;-)
Et l'article que tu cites va justement dans mon sens : tu ne t'es pas demandé pourquoi il était diffusé sur un site qui s'appelle Images des Maths et que l'exposé qui s'y rapporte avait eu lieu au séminaire d'histoire des mathématiques (qui plus est à l'IHP) ?
Pour reprendre le dessin de XKCD, très drôle au passage, les sciences pures et formelles sont aux nombres de trois : mathématiques, logique et métaphysique (philosophie pure); l'informatique est à la jonction des deux premières.
La classification encyclopédique de Wikipédia m'importe peu, je peux accepter comme argent comptant ce qui y est dit lorsque cela se trouve en dehors de mon domaine de compétence; ce qui ici n'est pas le cas.
Plus prosaïquement, et en dehors du débat épistémiologique, le sens de mon message était aussi de défendre les informaticiens (ie ceux qui sortent de la fac d'info) vis à vis des mathématiciens (ie ceux qui sortent de la fac de maths).
Je suis bien d'accord avec toi, mais parce que en général on n'y étudie pas les mêmes mathématiques. Et je maintiens que l'algorithmie et la calculabilité sont des disciplines mathématiques. Gödel, Turing ou Church, par exemple, étaient mathématiciens et logiciens.
Si les laboratoires de logique de jussieu et PPS ont créé le master LMFI, ce n'est pas sans raison.
This is officially a rant and should be read as such.
Here is my pet peeve: theoretical computer scientists misuse the word "provably". Stop it. Stop it!
Theoretical computer science is closer to mathematics than it is to computer science. There are definitions, theorems and proofs. Theoretical computer scientists must understand mathematical terminology. The words "proof" and "provable" are in the domain of mathematical logic. A statement is provable if it has a proof in a given formal system. It makes no sense to say "provable" without specifying or implying a specific proof system.
Un algorithme au fond, lorsque l'on considère les choses formellement, ce n'est rien d'autre qu'une preuve, ou un schéma de preuves, d'un théorème mathématique. C'est une manière différente, mais néanmoins très passionnante, de faire des mathématiques. C'est ce qu'aborde le deuxième article que j'avais cité, et qui relève de la théorie des types, théorie qui relève on ne peut plus du domaine mathématique. C'est elle qui est à la base des systèmes de typage des langages de programmation.
Pour le dire simplement, lorsqu'un compilateur vérifie qu'il n'y a pas d'erreurs de typage dans le programme, c'est comme un correcteur qui vérifie qu'il n'y a pas de vice de forme dans la démonstration d'un théorème. Et selon la richesse du système de type, on peut exprimer plus ou moins la sémantique du code à travers lui.
Un informaticien sera bien plus compétent qu'un mathématicien pour mettre au point un algorithme distribué ou parallèle. Inversement, pour étudier un point particulier de la topologie différentielle, vaudra bien mieux embaucher un mathématicien.
De même que pour étudier une question de théorie des ensembles, il vaut peut être mieux éviter d'embaucher un statisticien ou un arithméticien. Mais on a vu de tout : la conjecture de Poincaré a été résolue par des méthodes d'analyses, et celle de Fermat par des techniques de théorie des nombres qui relèvent grandement de la topologie et de la géométrie algébrique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Enfin un journal qui dénonce grave...
Posté par kantien . En réponse au journal De la nausée. Évalué à 6.
Pour la simple est bonne raison que, contrairement à la physique, elle n'emprunte aucun de ses principes à l'expérience : c'est une science pure et formelle. Du moins je me place du point de vue où l'on cherche à la considérer comme une science et non comme une simple technique. ;-)
Et l'article que tu cites va justement dans mon sens : tu ne t'es pas demandé pourquoi il était diffusé sur un site qui s'appelle Images des Maths et que l'exposé qui s'y rapporte avait eu lieu au séminaire d'histoire des mathématiques (qui plus est à l'IHP) ?
Pour reprendre le dessin de XKCD, très drôle au passage, les sciences pures et formelles sont aux nombres de trois : mathématiques, logique et métaphysique (philosophie pure); l'informatique est à la jonction des deux premières.
La classification encyclopédique de Wikipédia m'importe peu, je peux accepter comme argent comptant ce qui y est dit lorsque cela se trouve en dehors de mon domaine de compétence; ce qui ici n'est pas le cas.
Je suis bien d'accord avec toi, mais parce que en général on n'y étudie pas les mêmes mathématiques. Et je maintiens que l'algorithmie et la calculabilité sont des disciplines mathématiques. Gödel, Turing ou Church, par exemple, étaient mathématiciens et logiciens.
Si les laboratoires de logique de jussieu et PPS ont créé le master LMFI, ce n'est pas sans raison.
On pourra aussi lire l'article provably considered harmful :
Un algorithme au fond, lorsque l'on considère les choses formellement, ce n'est rien d'autre qu'une preuve, ou un schéma de preuves, d'un théorème mathématique. C'est une manière différente, mais néanmoins très passionnante, de faire des mathématiques. C'est ce qu'aborde le deuxième article que j'avais cité, et qui relève de la théorie des types, théorie qui relève on ne peut plus du domaine mathématique. C'est elle qui est à la base des systèmes de typage des langages de programmation.
Pour le dire simplement, lorsqu'un compilateur vérifie qu'il n'y a pas d'erreurs de typage dans le programme, c'est comme un correcteur qui vérifie qu'il n'y a pas de vice de forme dans la démonstration d'un théorème. Et selon la richesse du système de type, on peut exprimer plus ou moins la sémantique du code à travers lui.
De même que pour étudier une question de théorie des ensembles, il vaut peut être mieux éviter d'embaucher un statisticien ou un arithméticien. Mais on a vu de tout : la conjecture de Poincaré a été résolue par des méthodes d'analyses, et celle de Fermat par des techniques de théorie des nombres qui relèvent grandement de la topologie et de la géométrie algébrique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.