auve a écrit 310 commentaires

Manque de bol, sur tes cinq examples, les trois traitants de temps de réponse sont tout à fait dans le colimateur des méthodes formelles via par exemple automates temporisés*, et du fameux problème de calcul du temps d'exécution pire cas**. En particulier, ton premier exemple est un grand classique de la vérification de système temps-réel, domaine qui me semble particulièrement bien étudié !

Pour les problèmes d'interface graphique, effectivement c'est plus difficile, et je ne pense pas que les méthodes formelles aient un quelconque intérêt.

* : http://mpri.master.univ-paris7.fr/attached-documents/C-2-8/m(...)

** : http://en.wikipedia.org/wiki/Worst-case_execution_time

Les rédacteurs de chez Éconoclaste, Alexandre Delaigue et Stéphane Ménia, ont également décidé de ne pas suivre cette proposition : http://econoclaste.org.free.fr/dotclear/index.php/?2009/03/0(...)

Les raisons semblent assez similaires.

Oui, enfin rappelons avec monsieur Gödel que la preuve se base forcément sur quelque-chose de « plus fort » que la théorie de Coq elle-même. Il n'y a pas de preuve de cohérence de Coq en Coq, sans ajouter d'axiome supplémentaire, et (autre façon de voir les choses) il est impossible pour la même raison de coder l'algorithme de réduction du calcul des constructions inductives, la base formelle de Coq, en Coq.

Pour reprendre une image de Jean-Yves Girard, les preuves de cohérences sont des assurances contre l'explosion de la Terre (même si elle peuvent avoir des retombées pratiques et nous apprendre des choses).

Toi tch'as envie de dichtribuer des batches...

Mes confuses, je me suis lourdement trompé. C'est quand même étrange que l'option (il semble que ce soit « -fprofile-use ») soit si peu connue et discutée sur le net.

Mea maxima culpa.

Enfin, c'est surtout un individu immature.

Ah ? Il me semblait qu'un geek était quelqu'un d'obsédé par un sujet particulier, que ce soit l'informatique, une science quelconque comme les geeks physiciens de la série The Big Bang Theory, ou encore le milieu des opérateurs radio amateurs, très en vogue aux USA dans les années 80 et fortement lié aux balbutiements du hacking/phreacking. Évidemment, c'est souvent corrélé à une certaine asocialité qui peut éventuellement le faire passer pour immature...

Parce qu'à ma connaissance ça n'est pas géré sous GCC, et qu'on en parlait vaguement y a des années pour LLVM ? Et qu'on ne va pas s'amuser à compiler un logiciel libre sur une plateforme libre avec un compilateur propriétaire (Intel C++ pour ne pas le citer).

Fluctuat.net a réalisé un petit dossier intitulé « Les geeks au cinéma », où ils tirent à boulets rouges sur le film d'Élie Semoun et encensent ceux de Judd Apatow. Ils reprochent principalement à Cyprien d'être outrancier, bas de plafond et repompé sur d'autres long métrages bien plus réussis.

Le dossier : http://www.fluctuat.net/6721-Les-geeks-au-cinema
La critique : http://cinema.fluctuat.net/films/cyprien/5368-chronique-40-a(...)

Les linuxfriens ayant vu des films de Judd Apatow pourraient-ils m'éclaire sur la qualité d'iceux ?

J'ai toujours eu des problèmes à qualifier les articles de Cousot de "sympathique". Ils sont généralement très ardu et il y a un paquet de symbole dont la police de caractère a été inventée pour l'occasion (on ne sait pas comment le prononcer).

Je parlais uniquement de la page en question. Effectivement, l'interprétation abstraite n'est pas réputée être abordable, malgré des fondation mathématiques d'un niveau plutôt raisonnable. Il est aussi connu pour avoir une approche des exposés à base de transparents plutôt... singulière, tout comme le personnage d'ailleurs.

Pour le procès en paternité, je ne suis pas assez au fait de l'histoire mais j'ai quand même quelques doutes. Le fait est que de nos jours beaucoup de gen faisant de l'analyse statique industrielle (MSR, MathWorks/PolySpace, etc.) se placent quand même dans le cadre et la terminologie de Cousot, cf. l'exposé de Tom Ball à l'occasion des trente ans de l'Int. Abs.

J'ajoute au model-checking l'approche (plus ou moins concurrente... plus ou moins !) dite de « l'interprétation abstraite » inventée par Patrick Cousot : un cadre rigoureux pour la conception d'analyses statiques correctes basé sur la théorie de l'ordre et les treillis. Une introduction sympathique ici : http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html

Je crois que tu ne réalises pas que des gens qui se battent pour la liberté du logiciel peuvent avoir des positions très diverses sur beaucoup de sujets, et que tous n'adhèrent pas forcément à une certaine idéologie (Stallmanienne ?) qui peut sembler dominante.

Si tu ne veux ou ne peux passer par le gestionnaire de paquets de ta distribution pour compiler Whitelister, tu peux utiliser GODI[0]. C'est une distribution tout-en-un d'OCaml, qui récupère, bootstrappe et installe le compilateur OCaml. Ensuite tu lances « godi_console » et installes le module godi-syslog. Il ne te reste plus qu'à compiler Whitelister simplement.

Une fois compilé nativement, un exécutable écrit en OCaml est parfaitement indépendant du compilateur ou d'une forme quelconque d'environnement d'exécution.

[0] : http://godi.camlcity.org/godi/index.html

Camarades !

Des briseurs de grêves veulent rompre notre lutte solidaire contre les puissances de l'argent et les forces contre-révolutionnaires ! Ces sociaux-traîtres ont poussé la fourberie jusqu'à développer une barbe identique à celle de certains de nos camarades, Camarades !

Heureusement, ces agents à la solde du patronat arborent sans s'en rendre compte leur statut de « jaunes » : http://www.copinedegeek.com/img/tshirt_derriere2.jpg

À bientôt sur les baricades, Camarades !

« Linus chooses Third Reich »

Il n'y a pas vraiment de concurrence : Ext4 est une évolution d'Ext3 destiné à être employé jusqu'à ce que Btrfs soit pleinement finalisé et opérationnel.

Ted Tso, développeur principal d'Ext4, et d'autres spécialistes des systèmes de fichiers se sont mis d'accord lors du dernier workshop dédié à ce sujet pour adouber Btrfs « NGFS » : Next-Generation File System, c'est à dire le principal futur système de fichier moderne pour Linux.

Ted Tso signale également qu'il est pleinement pour l'intégration de Btrfs dans le noyau, donc a priori il ne me semble pas du tout y avoir de rivalité entre lui et son auteur, Chris Mason.

Source : http://thread.gmane.org/gmane.linux.file-systems/26246/focus(...)

1 - Un driver propriétaire dans Linux est de la pure provocation. Beaucoup de dévelopeurs et de personnes impliquées dans le libre (côté GPL en particulier) considère le driver de nvidia comme un excellent générateur de haine par son aggression.

Oui, d'ailleurs l'armée israëlienne a découvert des caches du Hamas contenant plusieurs dizaines de drivers nVidia, qui selon elle ont été utilisés contre les civils d'Israël.

...

/o\

Petit rappel : ta 6800 est une carte du haut de la gamme des 6***, alors que la 8400 est le bas de celle des 8***. En bref, ta carte est a priori meilleure qu'une 8400...

http://en.wikipedia.org/wiki/GeForce_8_Series#GeForce_8300_a(...)

Une monade (T, eta, mu) sur une catégorie C est formée d'un foncteur T de C dans C et de deux transformations naturelles : eta de l'identité sur C vers T et mu de TT vers T, satisfaisant certaines équations.

(Haskell en dix secondes : expr :: type indique que l'expression expr est de type type; \id -> expr déclare une nouvelle fonction anonyme prenant en paramètre une variable id et ayant pour corps expr. Par exemple,

ajoute2 x = x + 2

est équivalent à \x.x + 2.)

Haskell, est un langage purement fonctionnel, ce qui signifie que ses fonctions ne font pas d'effets de bords : appliquées au même argument, elles rendent toujours le même résultat, comme en mathématiques. Évidemment, on ne peut parfois pas échapper aux effets de bords : par exemple, pour faire des entrées sorties !

Imaginons, par exemple, une fonction readLine qui lit une chaîne de caractères sur la console. En Haskell, chaque programme se voit attribuer un type unique par le compilateur*; imaginons celui de notre fonction readLine. Premier jet :

readLine :: QQchose -> String

Qu'est-ce que ce QQchose ? A priori, rien de bien particulier. En C, on déclarerait une fonction sans paramètres (pour les dinos, void); en Haskell ça n'a pas de sens. On dispose justement d'un type approprié : () (à prononcer « younite »), habité par une unique valeur, elle aussi notée (), ce qui peut d'ailleurs entretenir une certaine confusion.

On a donc :

readLine :: () -> String

Problème plus grave : ça ne correspond pas à ce que j'ai décrit plus haut. Il est évident qu'un appel readLine () renverra différentes valeurs selon ce que rentre l'utilisateur... Intuitivement, le coeur du problème est que readLine, en faisant un effet de bord, agit sur le environnement qui l'entoure. On pourrait modéliser cela par le fait qu'on dispose d'un type Envir symbolisant ce fameux monde/environnement; son type deviendrait alors :

readLine :: Envir -> String

Se pose un nouveau problème : de toute évidence, readLine a... changé le monde ! Plus précisément, elle a entre autres consommé l'entrée de l'utilisateur sur le terminal où est lancé notre application. Elle doit donc nous renvoyer le nouveau monde obtenu après qu'elle ait effectué ses opérations.

readLine :: Envir -> (String, Envir)

Bien, il semblerait que nous ayons progressé dans notre modélisation. Maintenant, imaginons par exemple une fonction putLine qui affiche une chaîne sur la console puis passe à la ligne (un équivalent du puts de C). Nous savons que le type :

putLine :: String -> ()

Ne fonctionnera pas; notre fonction faisant des effets de bords, on va imiter la méthode utilisée ci-dessus et prendre un argument supplémentaire, sous forme du monde, et renvoyer le nouveau monde obtenu :

putLine :: String -> Envir -> ((), Envir)

Maintenant, nous pouvons écrire du code de ce style :


repete w =
let (ligne, w') = readLine w in
putLine ("Vous avez entre " ++ ligne) w'


Petit exercice : quel sera le type de notre fonction demandeAge ?

demandeAge :: Envir -> ((), Envir)

Ça fonctionne. Toutefois, a priori il reste un problème : je peux me tromper en passant mes « mondes » d'appel en appel, ici par exemple en confondant w et w' dans l'appel à putLine. En fait, idéalement, la « plomberie » de passage du « monde » ne devrait pas être réalisée explicitement par le programmeur.

Pour résoudre ce problème, on peut commencer par remarquer l'apparition progressive d'un motif récurrent dans nos types :

Envir -> (truc, Envir)

Étant programmeurs, nous sommes feignants : et si on s'abstrayait de ce type en l'encapsulant dans une nouvelle abbréviation ? On va déclarer un nouveau type, synonyme du précédent** :

type IO truc = Envir -> (truc, Envir)

Et là, on vient mine de rien de réaliser une petite percée conceptuelle : on est désormais capable de distinguer, en regardant son type, un programme faisant potentiellement des effets de bords d'un programme n'en faisant pas. Nos types deviennent :

readLine :: IO String
putLine :: String -> IO ()
demandeAge :: IO ()

Maintenant, il est intéressant de se demander quelles fonctions génériques sont communes à tous nos « programmes à effets de bords potentiels ». Déjà, on peut voir tout programme comme faisant potentiellement des effets de bords, en remarquant qu'il suffit qu'il ne modifie pas le monde qu'il reçoit :

return :: a -> IO a
return a = \w.(a, w)

Ensuite, on aimerait, comme dit précédemment, éliminer la plomberie, c'est-à-dire le passage explicite du monde d'une fonction à l'autre. Essayons de nos laissons guider par, par exemple, la composition des fonctions readLine et putLine. Imaginons une hypothétique fonction compose portant bien son nom; quel serait son type ?

compose :: (IO String) -> (String -> IO ()) -> IO ()

Soit, en s'abstrayant des types « concrets » String et () :

compose :: IO truc -> (truc -> IO bidule) -> IO bidule

Cette fonction est traditionnellement notée « >>= », à prononcer « bind ». Notre code devient donc :

demandeAge :: IO ()
demandeAge = readLine >>= (\ligne.putLine ("Vous avez entré " ++ ligne))

Qu'avons nous gagné ? Et bien, si on cache a l'utilisateur la nature de notre type IO, par exemple dans une bibliothèque séparée, il n'est plus possible de se tromper dans le passage des mondes. Il deviendra également impossible de mélanger arbirairement code « pur » et code à effets de bords. Cerise sur le gatal, Haskell propose du sucre syntaxique automatique se traduisant simplement dans le style utilisé ci-dessus, mais qui permet d'écrire :

demandeAge :: IO ()
demangeAge = do {
ligne <- readLine;
putLine ("Vous avez entré " ++ ligne);
}

Comme vous devez déjà vous en douter depuis un petit moment, ce triplet (IO, return, >>=) est... une monade. Et il s'avère que ce genre de construction apparaît TRÈS souvent en programmation, grosso-modo dès qu'on a besoin de parler d'un calcul se faisant dans un certain contexte; citons par exemple la monade des listes qui nous permet de programmer de façon non-déterministe. Elles viennent de la théorie des catégories, une jolie branche des mathématiques abstraites qui sert de plus en plus en théorie (et pratique :-) ?) des langages de programmation.

Donc, pour la définition programmatique : une monade est un triplet (T, return :: a -> T a, (>>=) : T a -> (a -> T b) -> T b), satisfaisant six équations que je vous épargnerais, mais qui, intuitivement, impliquent que return et >>= « coopèrent » bien.

Une monade est donc une façon simple de représenter et encapsuler des programmes s'exécutant dans un certain contexte, de les distinguer par leurs types, et de les composer. Pour plus de détails, je suggère la lecture de l'excellent papier de Philip Wadler : http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba(...)

...

Bon, ok, le Haskell n'est pas simple; mais au moins, il est différent, et je pense qu'il vaut la peine d'être appris, à défaut d'être utilisé.

* : Je simplifie un peu.

** : Je prends mes aise avec les déclarations de type Haskell pour la clareté de l'exposé, que les puristes m'épargnent.

Le principe est donc de proposer un logo plus moderne devant représenter la simplicité du langage.

Moi j'aime bien l'actuel*, au moins il a le mérite de rappeller les caractéristiques du langage : le « :: » pour le typage, la flêche « -> » pour la programmation fonctionnelle, le « ∀ » pour le polymorphisme, l'implication « => » pour la logique et enfin le « >> » pour les monades (et plus globalement la théorie des catégories).

Cela dit il faut reconnaître que c'est assez lourd symboliquement, et que ça peut (?) repousser les débutants.

* : http://www.willamette.edu/~fruehr/logos/PNGs/HaskellLogo.png

Oui, espérons qu'il soit bien routé vers le paradis...

Sinon, pour moi, une vraie réforme serait d'apprendre la bureautique et l'informatique et pas "Word/Excel" parce que c'est ce qui est utilisé en entreprise.

<aigri>Haha, comme l'enseignement d'informatique proposé par l'EPI et l'ASTI qui a été tant décrié ici ?</aigri>

cf. https://linuxfr.org/~akauffmann/27491.html

... je le fais (fuckin' serious).

Rendez-vous dans quelques mois/années !

Je suis assez sidéré par les commentaires présents à l'heure actuels.

Certes, la partie « société » n'est pas du tout prépondérante, bien que
clairement abordée, cf. annexe 1. Certes, le programme est ambitieux et bien sûr
imparfait (par exemple, le logiciel libre ne mériterait-il pas d'être au moins
mentionné ?).

Mais je ne peux m'empêcher de penser que la plupart des objections que j'ai lues
plus haut sont en contradiction presque totale avec ce qui me semblerait être la
vocation d'un tel programme : l'acquisition d'un vrai savoir généraliste faisant
potentiellement d'un citoyen un acteur responsable et lucide face au numérique,
c'est à dire capable de prendre des décisions basées sur ses connaissances
scientifiques et techniques objectives plutôt que sur le mélange de propagande,
rumeur et ouï-dire qui forme la base du savoir informatique de la vaste majorité
de nos compatriotes.

Avant tout, il ne faut pas négliger que les formulations employées exposent le
programme à des décideurs sensés être compétents en la matière (hum), et ne
reflètent pas du tout la présentation qui en sera faite aux élèves.

De plus, je trouve assez savoureuses certaines objections à ce programme, qui
transposées dans le cadre d'autres disciplines, feraient probablement hurler
leurs auteurs. Par exemple, on semble lui reprocher d'être trop théorique;
pourquoi ne pas faire de même, disons, pour le programme de chimie ? Après
tout, accabler des élèves très différents avec un savoir qui ne leur servira pas
dans leur vie professionnelle, à quoi bon ? On se contentera facilement d'un
module « Chimie et société » exposant de façon vulgarisée les grands principes
de la chimie, son histoire et l'apport à la société moderne. Mieux, on
généralisera aisément à toutes ces disciplines superflues comme l'histoire ou
les mathématiques; après tout, quel DRH a déjà demandé la date de la bataille de
Marignan lors d'un entretien d'embauche ? Ou bien, pour l'écrasante majorité
d'entre eux, la résolution d'une équation du second degré ? Ne parlons pas de la
philosophie. En route pour l'ECJSisation du lycée !

Toutes les ébauches de programmes gloubi-boulga que j'ai vu ci-dessus me
semblent oublier un détail : tous les points « web social » / « sous-culture
internet » seront probablement autant maîtrisés par les élèves que par le
professeur. Le rôle du lycée devrait plutôt être de dispenser un savoir plus
difficile à acquérir par soi même pour la majorité, réduisant ainsi les
inégalités présentes et futures.

Quand aux reproches concernant le caractère supposé trop « professionnalisant »,
ils me semblent vraiment absurdes; pour reprendre l'analogie avec la chimie,
va-t-on reprocher l'étude de la combustion du carbone en quatrième comme un
honteux cadeau au patronat friand de jeunes ingénieurs chimistes ?

En filigrane se pose la question de la nature de l'informatique. Si on admet, ce
qui me semble raisonnable bien qu'inconscient chez 99% de la population, qu'il
s'agit d'une discipline technique mais aussi d'une science*, alors on
doit en déduire que ce genre de programme a sa place, et que l'algorithmique et
la programmation doivent légitimement en former le coeur, tout comme elles
fondent la science qui le sous-tend.

Pour conclure : cet enseignement a pour vocation avouée d'être « de qualité »,
ambition rafraîchissante à la lueur de la médiocrité éducative ambiante; il aura
besoin d'enseignants compétents et motivés ainsi que de courage politique
et pédagogique pour arriver à ne serait-ce qu'une fraction de son objectif. Mais
je pense sincèrement qu'à long terme, il peut améliorer significativement les
rapports des français au numérique.

Si on lui en donne l'occasion.

auve

PS : Les lecteurs intéressés par plus d'information, et en particulier un
programme plus général concernant le lycée, pourront se référer à la page de
Gilles Dowek : http://www.lix.polytechnique.fr/~dowek/enseignement.html

* : Tout à fait distincte mais souvent voisine des mathématiques.

C'est toi, les gens à l'origine de ce programme n'ont clairement rien à voir avec cet truc infâme.

Hmm ? Les VPNs ne limitent pas l'usage de la cryptographie asymétrique à l'échange d'une clé de session qui sera ensuite utilisée avec un algorithme de chiffrement symétrique ? Ou bien même cela coûte vraiment trop ?