Yusei a écrit 4649 commentaires

  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    1) on n'observe pas les contre-exemple

    Un contre-exemple est un exemple qui contredit une hypothèse. Par conséquent, si j'émet l'hypothèse "tous les cygnes sont blancs", et que je croise un cygne noir, j'observe un contre-exemple.

    2) on ne prouve pas les cygnes.

    Et c'est pour ça que j'ai parlé de prouver la théorie "tous les cygnes sont blancs". On prouve (enfin, on conforte) des théories.

    Ensuite, naturellement, Dijkstra est toujours pertinent, et ici si on veut se ramené à nos histoires de sciences expérimentales, avec les tests de programmes on teste l'hypothèse "ce programme n'a pas de bugs". Les tests peuvent la réfuter, mais jamais la prouver.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.

    Pour la nouvelle illustrée par Manara, ça doit être au minimum inspiré de la nouvelle de Borges, "la bibliothèque de Babel", qui parle d'une bibliothèque contant tous les livres d'une certaine taille.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.

    J'aurais dû préciser que ce programme exécutant tous les programmes ne les exécutera pas jusqu'au bout pour la plupart. L'important est que si on lui offre suffisamment de ressources, il les exécute tous. C'est plus les implications philosophies qui sont intéressantes, et pas l'idée de le réaliser un jour :)

    Pour faire cet énumérateur de programme, on ordonne les programmes par longueur, puis:
    - x = 1
    - t = 1
    - on exécute t secondes de chaque programme de taille <= x
    - on incrémente t et x
    - on répète infiniment

    À l'infini, on a exécuté tous les programmes. Évidemment c'est inatteignable par manque d'énergie pour faire tourner un ordinateur infiniment, mais par contre au bout de "longtemps" on aura probablement simulé toutes les consciences humaines vivantes aujourd'hui. Plus quelques autres.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    C'est cohérent avec ce qu'il dit: la théorie "tous les cygnes sont blancs" peut seulement être réfutée par l'observation d'un contre exemple, mais ne pourra jamais être prouvée, quel que soit le nombre d'observations de cygnes blancs.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    Bon, je suis pas non plus sûr que ça implique qu'il n'existe pas une [théorie déterministe] dans l'absolu

    En fait, si on prend l'interprétation "multivers" de la physique quantique, ça explique de manière élégante le non déterminisme que l'on observe. Mais je ne sais pas si j'arriverai à résumer ça clairement et succintement.

    Dans cette interprétation, il existe une infinité d'univers parallèles. Par exemple, si je met un chat dans une boîte avec un dispositif qui peut le tuer ou pas aléatoirement, il existe plein d'univers parallèles dans lesquels j'ai fait ça. Tant que je n'ai pas ouvert la boîte, je ne sais pas si le chat est encore en vie. Au moment où j'ouvre, ces univers se répartissent en deux groupes: ceux dans lesquels le chat est mort, et ceux dans lesquels le chat est vivant. La proportion d'univers dans chaque groupe est ce que nous percevons comme la probabilité que l'évènement se produise.

    Pourquoi ? Parce que le "moi" qui observe est dans un univers et un seul. Donc parmis tous ces univers, je suis dans un seul. La probabilité que le chat soit mort est égale à ma probabilité d'être dans un univers du groupe chat-mort, donc est égale à la proportion d'univers qui sont chat-mort.

    Ça résoud le problème du non-déterminisme en ce sens que le multivers est déterministe, ce qui est assez satisfaisant du point de vue philosophique. Là où on voit du hasard, il ne s'agit en réalité que de proportion. Et on ne voit du hasard que parce que notre conscience n'observe qu'un univers à la fois.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.

    Cela fait qu'en gros, moyennant une machine suffisament puissante, on peut émuler un cerveau humain

    Ce qui a plein d'implications philosophiques rigolotes. Par exemple on peut facilement écrire un programme qui exécute tous les programmes possibles. Et donc, si on le laisse tourner suffisamment longtemps et avec suffisamment de mémoire, ce programme simulera toutes les consciences imaginables, y compris la mienne pendant que j'écris ça, mais aussi une version de moi où je n'écris pas ça.

    On pourrait pousser encore plus loin et d'autres l'ont fait, voir entre autres les travaux de Bruno Marchal, ou bien le roman de Greg Egan, "permutation city".

    Ca ne garantie pas qu'à données d'entrées égales, la sortie soit égale.

    Si, parce qu'une machine de Turing est déterministe.

    Nous connaissons des sortes de macro-lois, donc nous perdons de la précision, d'oû le non déterminisme.

    Ça c'est la version du monde datant d'avant la découverte de la mécanique quantique: si on savait simuler avec assez de précision, alors le monde serait déterministe. La mécanique quantique affirme que le monde que nous observons est par nature non déterministe, et qu'il ne s'agit pas d'un problème de précision.

    Ce qui ne veut pas dire que notre conscience est soumise à ça, car la mécanique quantique ne s'applique pas à notre niveau. Les histoires de Roger Penrose me semblent être une tentative de "sauver" le libre arbitre en ajoutant de l'aléa en ajoutant des "phénomènes quantiques" agissant sur nous. Ça me parait violer le principe d'Okham, mais pourquoi pas. Et Penrose est quelqu'un de fort respectable par ailleurs, donc ça mérite d'être considéré au moins un instant.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    je suis curieux de savoir ce qui peu le pousser à penser autrement mis à part de l'anthropocentrisme

    Probablement qu'il rejette certaines implications philosophiques du matérialisme. L'esprit humain a l'air non déterministe, et ça nous arrange bien de penser qu'on a du libre arbitre. Mais si on est simulables par un ordinateur déterministe, que devient notre libre arbitre ? Si on me simule plusieurs fois de suite dans les mêmes conditions, vais-je prendre à chaque fois les mêmes décisions ? Etc.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.

    À partir du moment où je reproduit le shéma neuronale d'un cerveau humain dans un logiciel, je ne vois pas ce qui ferait que l'un soit incapable de faire virtuellement ce que l'autre fait physiquement.

    On ne sait pas ce qu'est la conscience humaine. Si c'est seulement une propriété émergente de l'agencement des atomes du cerveau, alors je suis d'accord, mais il y a des gens sérieux qui contestent ça, par exemple Penrose.

    Qu'est-ce qu'on en à faire que notre programme ne réponds pas au contrat dans des cas ultra rares auquel on aurait pas pensé soit même ?

    Tu supposes que dans tous les cas utiles/pratiques on peut prouver des choses (manuellement ou automatiquement). Ça reste à voir.

    Après, réfléchir à ce qu'on peut prouver et ce qu'on ne peut pas prouver, ce n'est pas de la branlette intellectuelle, et ça ne sert pas seulement à dire "je ne peux pas, donc je n'essaye pas". Ça sert aussi à savoir quelles sont les choses auxquelles je dois renoncer si je veux avoir une preuve solide.
  • [^] # Re: prouveur automatique/assistant de preuve

    Posté par  (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 6.

    Moi je dirais qu'il n'en existe pas encore, mais théoriquement, je vois pas ce qui l'empêche.
    Théoriquement, il est prouvé depuis longtemps qu'il n'existe pas d'algorithme permettant entre autres, et pour n'importe quel programme en entrée:
    - de déterminer si ce programme s'arrête
    - de déterminer si ce programme fait la même chose qu'un autre programme
    - et par extension de déterminer si ce programme est conforme à sa spécification

    Donc tous les prouveurs qu'on pourra écrire seront limités, non autonomes ou non déterministes.

    En poussant ton approche plus loin on peut même observer que si la conscience humaine est simulable sur ordinateur, alors un humain ne peut pas non plus prouver toutes ces choses.
  • [^] # Re: Kile

    Posté par  (Mastodon) . En réponse à la dépêche Atelier LaTeX - le 28 février 2009 à Paris. Évalué à 4.

    Personnellement, je préfèrerais que les éditeurs latex s'interfacent avec les gestionnaires de packages des distributions, même si ça représente un peu plus de travail. C'est un peu pénible d'avoir 36 gestionnaires de packages installés. Un de mes arguments de vente principaux quand je parle de GNU/Linux, c'est le système de packages centralisé qui permet de voir en un clin d'oeil ce qui est disponible pour installation/mise à jour.

    Accessoirement, s'il existe une base de packages à jour dans laquelle MikTeX va se servir, il ne doit pas être trop difficile d'effectuer une transformation automatique de ces packages vers le format deb/rpm, qui permettrait une intégration au système qui soit à jour.
  • [^] # Re: Kile

    Posté par  (Mastodon) . En réponse à la dépêche Atelier LaTeX - le 28 février 2009 à Paris. Évalué à 1.

    Sous Linux, cette gestion des packages est un grand manque qui est en passe d'être résolu

    M'enfin... sous Linux, ça fait des siècles que j'utilise la gestion des packages intégrée au système pour installer mes packages LaTeX, et ça marche très bien.
  • [^] # Re: rigolo

    Posté par  (Mastodon) . En réponse au journal [HS] Stallman à propos du logiciel "privateur" vs privatif. Évalué à 10.

    RMS est rigolo, mais comme tout extrémiste, ses propos sont à mettre sous le compte de la folie. [...] Quand il aura rasé sa barbe, on reverras la question.

    Il va être triste d'apprendre que tu refuses de revoir la question tant qu'il a de la barbe... ça va lui faire un choc. Je suis sûr qu'il va se la raser bien vite pour avoir l'honneur de remonter dans ton estime.
  • [^] # Re: Oui mais

    Posté par  (Mastodon) . En réponse à la dépêche L'Université souhaite continuer à jouer un rôle actif dans l'écosystème du logiciel libre. Évalué à 2.

    C'est l'occasion de faire de la pub pour le master "modèles et algorithmes" de Bordeaux 1 qui, s'il n'a pas changé depuis 2004, propose des modules de formation à la recherche et d'analyse de texte scientifique.
  • [^] # Re: Oui mais

    Posté par  (Mastodon) . En réponse à la dépêche L'Université souhaite continuer à jouer un rôle actif dans l'écosystème du logiciel libre. Évalué à 3.

    Si on veut apprendre un métier, on ne fait pas son bac+5 à l'université !

    Et les étudiants qui vont à l'université aujourd'hui, tu crois qu'ils font ça pour l'honneur de l'esprit humain ? Si l'université ne préparait pas les étudiants à travailler, il n'y aurait à l'université que les quelques personnes qui n'ont pas besoin de gagner leur vie. Presque personne d'autre n'irait investir 5 ou 8 ans de sa vie simplement pour apprendre des choses intéressantes.

    Les diplômes à bac+5 aujourd'hui sont divisés en Master Recherche et Master Pro. Les premiers forment au métier de chercheur, et les seconds forment à d'autres métiers. Avec stages en entreprise, et tout le bataclan. Tu peux penser que ce n'est pas le rôle de l'Université, mais c'est ce qu'elle fait aujourd'hui. Si elle ne faisait pas ça, je me demande qui irait sur les bancs des amphithéâtres.
  • [^] # Re: Oui mais

    Posté par  (Mastodon) . En réponse à la dépêche L'Université souhaite continuer à jouer un rôle actif dans l'écosystème du logiciel libre. Évalué à 5.

    Je ne suis pas d'accord: l'université permet d'étudier, pas de se former à un métier. [...] Il y a d'autres filières que l'université [...] qui permettent de se former à un métier

    Et donc, une fois qu'on a fait son bac+5 à l'université, on fait un BTS pour se former à un métier ? Ça ne semble pas très réaliste.
  • [^] # Re: Oui mais

    Posté par  (Mastodon) . En réponse à la dépêche L'Université souhaite continuer à jouer un rôle actif dans l'écosystème du logiciel libre. Évalué à 5.

    Par ailleurs, il me semble difficilement réalisable d'ajouter une formation intensive à l'épistémologie dans les premières années. Les élèves qui nous arrivent ont déjà bien trop souvent du mal avec l'algèbre de base pour qu'on puisse leur supprimer quelques cours de propédeutique en sciences « durs » au profit de leur culture.

    Je pense que l'épistémologie et l'histoire des sciences sont indispensables pour bien aborder les études scientifiques, et pas simplement une histoire de culture générale. Je n'ai jamais réussi à rien apprendre sans en connaître la raison, et je n'ai jamais réussi à comprendre la raison d'une chose sans m'intéresser à la manière dont elle a été découverte/construite. Peut-être que tout le monde ne fonctionne pas comme ça, mais en tout cas ça m'aurait bien aidé de ne pas devoir étudier l'épistémologie tout seul.

    Aujourd'hui on peut trouver des gens en bac+5 de matières scientifiques qui ne sont pas capables de décrire clairement ce qu'est la fameuse "méthode scientifique". Pas besoin de pouvoir citer Popper, mais au moins savoir expliquer qu'une théorie scientifique n'est pas une théorie prouvable mais une théorie réfutable, etc.
  • [^] # Re: Oui mais

    Posté par  (Mastodon) . En réponse à la dépêche L'Université souhaite continuer à jouer un rôle actif dans l'écosystème du logiciel libre. Évalué à 3.

    Je suis d'accord sur le fond, mais je pense qu'il faut quand même que l'Université forme aussi à un métier: il serait inadmissible qu'on sorte à bac+5 dans l'impossibilité de trouver un emploi. Tout le monde ne veut pas finir enseignant ou chercheur.

    Ce que j'ai aimé à la fac, et qui risquerait de disparaître si on axait trop la formation sur le métier, c'est la possibilité de découvrir plein de nouveaux horizons. J'ai eu des cours d'économie, de gestion et de sociologie, ça ne me sert à rien dans mon métier, mais ça m'est utile dans la vie de tous les jours pour comprendre ce qui se passe dans la société. Je n'aurais pas eu ça dans une école d'ingénieurs, malgré l'éventuelle présence de cours de "culture générale". Dans un autre style, en ce moment j'anime un TD de "musique et informatique" . Une bonne partie du cours est consacré à la théorie musicale ; ça ne sert à rien dans la vie professionnelle, mais c'est vraiment le cours que j'aurais aimé avoir quand j'étais étudiant.

    Néanmoins, il faut bien se spécialiser tôt ou tard. On se spécialise trop tôt à mon goût depuis la réforme LMD, mais ça ne me choque pas que vers la fin des études on attende de la majorité des cours qu'ils soient utiles.

    Multiplions les cours inutiles, imposons un important cours d'histoire générale et un cours de philosophie dans la 1ere année toutes les filières! c'est peut être les deux seuls cours véritablement importants!

    J'ajouterais des cours d'épistémologie/méthode scientifique, parce qu'on n'en a pas, même dans les filières scientifiques. J'ai eu la chance d'avoir quelques cours d'histoire des sciences, qu'on ne trouve pas partout ; il faudrait le généraliser. Et puis je suggère aussi à tout le monde de suivre des cours d'introduction à l'économie et à la sociologie.
  • [^] # Re: Rien sur le processus de Bologne ?

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 2.

    Des garanties sur le fait que tous les bons chercheurs pourront avoir moins d'heures à enseigner?

    Une garantie que le quota d'enseignement des chercheurs évalués positivement ne pourra pas augmenter. Donc, même si la plupart d'entre eux risque de rester à 192h/an, leurs collègues verront eux leur quota augmenter nettement.
  • [^] # Re: Pour la souris...

    Posté par  (Mastodon) . En réponse au journal Santé et usage de l'ordinateur. Évalué à 3.

    Celui que j'ai est gros, ce qu'on ne voit pas bien sur l'image, ce qui fait que la main est également penchée, dans une position plus naturelle que sur une souris. Ceci dit, je pense que les deux se valent, si tu n'as pas l'intention d'utiliser la symmétrie pour alterner la main qui utilise le trackball.
  • [^] # Re: Pour la souris...

    Posté par  (Mastodon) . En réponse au journal Santé et usage de l'ordinateur. Évalué à 3.

    Une observation au passage: la position du bras quand on utilise cette souris verticale est la même que celle de mon bras quand j'utilise mon trackball ( http://www.logitech.com/index.cfm/mice_pointers/trackballs/d(...) ). L'avantage de ce trackball est aussi sa symétrie, qui le rend utilisable par les gauchers. J'en suis assez content, depuis quelques années que je l'utilise en remplacement de la souris.

    Par contre, ça n'a pas résolu mes problèmes de poignet. Est-ce que ça les empêche de s'aggraver ? Je n'en suis même pas sûr.
  • [^] # Re: Hérissons

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 3.

    Un petit coup de selection a l'entree pour degager disons 20% des etudiants et hop, ton budget par etudiant et tes resultats prennent un coup de boost.

    Dégager les étudiants à l'entrée, ça peut réduire les sur-effectifs en première année, mais ce n'est pas ça qui va sensiblement réduire le nombre d'heures à faire. Parce que même si on retire un groupe de TD par matière en première année, pour tout le reste ça ne change pas. D'autant que ces TD là sont plutôt faits par des thésards qui ne sont pas concernés par la réforme. Même si ça peut être bénéfique pour les étudiants, ça ne résoud pas le problème de financement des enseignants.

    Il ne faut pas se leurer: même si quelques entreprises sponsorisent des chaires, ça ne remplacera pas les suppressions de postes. Si on diminue le quota d'enseignement des meilleurs chercheurs et qu'on supprime des postes (200 cette année) sans changer le nombre d'heures à faire, il faudra soit surcharger les enseignants restants, soit en engager plus. Et pour en engager plus, il faut des moyens, donc si l'État ne paye pas, ça se fera par les frais d'inscription.

    Tu compares les moyens des universités françaises avec les universités étrangères ; il faut aussi comparer le montant des frais d'inscription. Il me semble que les frais d'inscription dans ma fac sont de l'ordre de 300 euros. C'est combien dans les grandes universités américaines ?
  • [^] # Re: Hérissons

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 3.

    Le pire serait de rester comme cela.

    C'est là dessus qu'on n'est pas d'accord.

    Excuse moi d'être direct, mais il est idiot de dire que n'importe quel changement vaut mieux que pas de changement du tout. Aujourd'hui il faut décider si l'enseignement supérieur doit être à deux vitesses. On a une Université qui, avec tous ses défauts, propose quand même un enseignement accessible à tout le monde et globalement de qualité. La conséquence du décret actuel c'est une remise en question de ça. Je ne suis pas d'accord pour dire que c'est mieux que de ne pas changer.
  • [^] # Re: Hérissons

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 3.

    En gros, ils pondaient des théories et des affirmations non vérifiées, dans tous les sens mais refusaient de les mettres en pratique. Cela en resultait à des théories "juste" dans la tête du chercheur mais complètement erronées dans le concret.

    Il y en a sans aucun doute des comme ça. Si leurs théories sont sans fondement et "complètement erronées", alors il est probable qu'ils ne publient pas, car la publication est soumise à une évaluation sévère par les autres chercheurs.

    Et donc, la réforme actuelle propose d'augmenter la charge d'enseignement de ces chercheurs déconnectés de la réalité. Il va être beau, l'enseignement universitaire en France.
  • [^] # Re: Hérissons

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 2.

    T'auras aussi des facs élitistes qui font payer de forts frais d'inscriptions, ce qui leur permettra d'engager plus d'enseignants-chercheurs, et donc de proposer un enseignement de meilleure qualité. D'autant plus que les financements publics seront maintenant attribués en partie sur des critères d'efficacité, donc les facs qui attirent de meilleurs chercheurs voient automatiquement leurs moyens augmenter.

    Pendant ce temps, les facs avec peu de moyens devront augmenter le quota d'enseignement de ses employés. Donc, moins de recherche, donc moins bons résultats, donc moins de moyens, etc.
  • [^] # Re: Hérissons

    Posté par  (Mastodon) . En réponse au journal [HS] Pour info et désintoxication - recherche scientifique et université. Évalué à 2.

    Je suis d'accord sur l'immobilisme général dans l'enseignement. Ma mémoire politique ne remonte pas très loin, mais je ne me souviens pas d'un seul ministre de l'éducation qui ait été apprécié, et les moins détestés sont ceux qui ont fait le moins de choses.

    Il n'en reste pas moins que cette réforme là est mauvaise. Je connais des Sarkozystes convaincus qui s'y opposent, c'est pas juste une histoire de gauchistes. Quand au fait de savoir comment ça va se passer en pratique, il suffit de voir que la ministre propose une charte pour garantir que la loi sera "bien" appliquée.

    Une loi qui a besoin d'une charte pour éviter les débordements est une mauvaise loi. Si la charte résout tous les problèmes, ils n'ont qu'à en faire un amendement pour lui donner le même statut que le décret.