Je n'ai pas trop d'avis au sujet de ta modélisation du risque de panne dans un raid, si ce n'est que le recours à la loi binomiale est peut être effectivement discutable (non indépendance du risque de panne conjointe). Mais quoi qu'il en soit, le modèle en question était volontairement simplifié (c'était clairement affiché de ta part) et dans tous les cas, pour toute modélisation physique c'est la confrontation avec l'expérience et l'observation qui a le dernier mot. ;)
Pour ce qui est de Nicolas Boulay, il ne semble pas savoir ce que c'est que de la théorie : modéliser c'est faire de la théorie (la réciproque n'est pas nécessairement vraie, bien entendu). À moins qu'il est pour projet d'inventer le triangle à quatre côtés.
En revanche, tu n'as peut être pas bien saisi la signification du passage du texte de Kant que tu cites. Il est vraie que si l'on n'est pas familier avec la partie théorique de sa philosophie (théorie de la connaissance), ce passage peut prêter à confusion. Il veut dire par là que si un concept contient bien un règle, il est souvent impossible de fournir une règle pour dire comment l'appliquer, car alors cette dernière règle exigerai à son tour un autre règle pour savoir quand et comment l'appliquer, et cela à l'infini. Telle est l'utilité de la jurisprudence dans le domaine juridique : donner des cas d'affaires singulières qui tombent sous le coup de telle ou telle loi. La loi fournit l'universel (la règle) et la jurisprudence contient des cas particuliers qui tombent sous elle (appliquer une règle à un cas, c'est cela que Kant nomme « subsomption »). Lorsque notre faculté de juger remplit cette fonction, elle est qualifié de déterminante : elle détermine un cas particulier selon un règle générale.
Or dans le cas de la recherche et de la construction d'un modèle, le particulier est connu mais non la règle. Au contraire c'est cette règle que l'on cherche à trouver. Dans ce cas, notre même faculté de juger (qui précédemment était déterminante) devient réfléchissante : c'est ce que l'on appelle tout bonnement réfléchir. Et ce processus consiste justement à modéliser, et son produit est un modèle. Ce qui correspond plutôt à ce passage du texte
c'est de là que le médecin qui sort de son école, ou l’agriculteur, ou le financier, peut et doit abstraire de nouvelles règles pour compléter sa théorie. Ce n’est pas alors la faute de la théorie, si elle n’a encore que peu de valeur pour la pratique; cela vient de ce qu’on n’a pas assez de théorie, de celle que l’homme aurait dû apprendre de l’expérience, et qui est la véritable théorie
Mais bien sûr, pour faire cela il faut savoir théoriser et donc connaître des théories (c'est en forgeant que l'on devient forgeron).
Pour finir, il y a un passage qui m'a fort étonné dans ton journal sur le raid :
Je sais, les maths, blah blah blah blah... l'informatique, l'IT, ce ne sont pas des maths, blah blah blah blah...
Alors je ne sais si c'est ton ressenti d'une pensée ambiante en ces lieux, ou si elle est réelle, mais je peux te rassurer : l'informatique et l'IT c'est des mathématiques !
Comme mon message est déjà bien long je ne vais pas trop m'appesantir, mais l'informatique est une science dont l'algorithmique et la logique mathématique sont des composantes essentielles (ce n'est pas pour rien qu'existe le master Logique Mathématique et Fondements de l'Informatique ). On y apprend, par exemple, qu'un algorithme ou un programme n'est rien d'autre qu'un preuve d'un théorème mathématique, ce résultat est connu sous le nom de « correspondance ou isomoprhisme de Curry-Howard ». Cela relève du lambda calcul fortement typé : c'est de là que vient, entre autre, le système de type algébrique de langages comme Haskell ou OCaml (Haskell était le prénom de Curry). Un exemple classique sur le sujet est le théorème d'Euclide qui affirme l'existence d'une infinité de nombre premier, c'est à dire que pour tout entier n il existe un entier p tel que n < p et p est premier. Et bien toute preuve de ce théorème est un programme qui prend un entier en entrée et renvoie en sortie un nombre premier plus grand que son entrée. ;)
Le langage de type des GADT ne permet pas d'exprimer cela, on peut juste dire qu'on à une fonction qui prend un entier et renvoie un entier, mais le langage Coq le permet.
Les lecteurs désireux dans connaître plus sur le sujet pourront par exemple lire ces deux textes: À propos de la théorie des démonstrations il relate bien l'histoire de la découverte des paradoxes de Russell, en passant par les résultats de Gödel, jusqu'aux travaux contemporains. De plus, il comporte une touche d'humour en comparant les mathématiciens à des drogués à un jeu en réseau. Fonctions, programmes et démonstrations
[^] # Re: Bon en théorie, mais inutile en pratique
Posté par kantien . En réponse au journal François Hollande visite 42, non mais allô quoi.... Évalué à 1.
Je n'ai pas trop d'avis au sujet de ta modélisation du risque de panne dans un raid, si ce n'est que le recours à la loi binomiale est peut être effectivement discutable (non indépendance du risque de panne conjointe). Mais quoi qu'il en soit, le modèle en question était volontairement simplifié (c'était clairement affiché de ta part) et dans tous les cas, pour toute modélisation physique c'est la confrontation avec l'expérience et l'observation qui a le dernier mot. ;)
Pour ce qui est de Nicolas Boulay, il ne semble pas savoir ce que c'est que de la théorie : modéliser c'est faire de la théorie (la réciproque n'est pas nécessairement vraie, bien entendu). À moins qu'il est pour projet d'inventer le triangle à quatre côtés.
En revanche, tu n'as peut être pas bien saisi la signification du passage du texte de Kant que tu cites. Il est vraie que si l'on n'est pas familier avec la partie théorique de sa philosophie (théorie de la connaissance), ce passage peut prêter à confusion. Il veut dire par là que si un concept contient bien un règle, il est souvent impossible de fournir une règle pour dire comment l'appliquer, car alors cette dernière règle exigerai à son tour un autre règle pour savoir quand et comment l'appliquer, et cela à l'infini. Telle est l'utilité de la jurisprudence dans le domaine juridique : donner des cas d'affaires singulières qui tombent sous le coup de telle ou telle loi. La loi fournit l'universel (la règle) et la jurisprudence contient des cas particuliers qui tombent sous elle (appliquer une règle à un cas, c'est cela que Kant nomme « subsomption »). Lorsque notre faculté de juger remplit cette fonction, elle est qualifié de déterminante : elle détermine un cas particulier selon un règle générale.
Or dans le cas de la recherche et de la construction d'un modèle, le particulier est connu mais non la règle. Au contraire c'est cette règle que l'on cherche à trouver. Dans ce cas, notre même faculté de juger (qui précédemment était déterminante) devient réfléchissante : c'est ce que l'on appelle tout bonnement réfléchir. Et ce processus consiste justement à modéliser, et son produit est un modèle. Ce qui correspond plutôt à ce passage du texte
Mais bien sûr, pour faire cela il faut savoir théoriser et donc connaître des théories (c'est en forgeant que l'on devient forgeron).
Pour finir, il y a un passage qui m'a fort étonné dans ton journal sur le raid :
Alors je ne sais si c'est ton ressenti d'une pensée ambiante en ces lieux, ou si elle est réelle, mais je peux te rassurer : l'informatique et l'IT c'est des mathématiques !
Comme mon message est déjà bien long je ne vais pas trop m'appesantir, mais l'informatique est une science dont l'algorithmique et la logique mathématique sont des composantes essentielles (ce n'est pas pour rien qu'existe le master Logique Mathématique et Fondements de l'Informatique ). On y apprend, par exemple, qu'un algorithme ou un programme n'est rien d'autre qu'un preuve d'un théorème mathématique, ce résultat est connu sous le nom de « correspondance ou isomoprhisme de Curry-Howard ». Cela relève du lambda calcul fortement typé : c'est de là que vient, entre autre, le système de type algébrique de langages comme Haskell ou OCaml (Haskell était le prénom de Curry). Un exemple classique sur le sujet est le théorème d'Euclide qui affirme l'existence d'une infinité de nombre premier, c'est à dire que pour tout entier n il existe un entier p tel que n < p et p est premier. Et bien toute preuve de ce théorème est un programme qui prend un entier en entrée et renvoie en sortie un nombre premier plus grand que son entrée. ;)
Le langage de type des GADT ne permet pas d'exprimer cela, on peut juste dire qu'on à une fonction qui prend un entier et renvoie un entier, mais le langage Coq le permet.
Les lecteurs désireux dans connaître plus sur le sujet pourront par exemple lire ces deux textes:
À propos de la théorie des démonstrations il relate bien l'histoire de la découverte des paradoxes de Russell, en passant par les résultats de Gödel, jusqu'aux travaux contemporains. De plus, il comporte une touche d'humour en comparant les mathématiciens à des drogués à un jeu en réseau.
Fonctions, programmes et démonstrations
P.S : on peut aussi étendre ce système de typage aux protocoles réseaux
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.