URL: https://linuxfr.org/users/montaigne/journaux/le-labo-commun-inria-microsoft Title: Le labo commun Inria-Microsoft Authors: Ontologia Date: 2009年02月02日T15:31:03+01:00 Tags: leslie_lamport Score: 8 L'inria, au grand dam de nombre de ses salariés, a pactisé avec l'ennemi pour créer un laboratoire commun de recherche. Pour le moment, les Forces du Mal ne semblent pas avoir imposé leur maléfiques brevets logiciels, et permettent même de libérer les sources et informations sur leur projet par une licence agréée par le Camp du Bien. On y trouve divers axes de recherches très intéressants : **Secure Distributed Computations and their Proofs et Tools and Methodologies for Formal Specifications and for Proofs** En gros il s'agit de deux choses : de la cryptographie et de la vérification semi automatique de respect de séquence de protocoles en fonction de la spécification. A ce propos, le gourou iMil, de la secte GCU, signalait l'autre jour un merveilleux logiciel, propre qui plus est, permettant d'implémenter des automates à état fini dans divers langages. Un compilateur de machine à état fini, ça s'appelle [Ragel](http://www.complang.org/ragel/) et c'est génial ce truc ! **Mathematical Components** L'idée est pas bête du tout : plutôt que de travailler à faire des outils de preuve de programme à approche globale, on cherche ici à prouver des petits bouts de code, de théorème afin de faciliter la preuve d'ensemble. Ce travail de fourmi, utilisant le logiciel français COQ (développé à l'INRIA par des partisans résolus des Forces Du Bien), permettra d'étendre le domaine des logiciels prouvé formellement, qui sont encore peu nombreux (là où il y a risque pour la vie humaine). On pourra noter des travaux précédents, comme [why](http://why.lri.fr/index.fr.html) de Jean-Christophe Filliâtre. **Tools and Methodologies for Formal Specifications and for Proofs** On y utilise pour se faire les TLA, (Temporal logic of actions) de Leslie Lamport, qui lui aussi travaille pour les Forces du Mal, le but étant de construire un ensemble d'outil pour faire de la preuve logiciel avec. Malgré tout, je comprend pas très bien pourquoi on essaye de combiner de la preuve pas model checker et de la preuve formelle, l'un est potentiellement le sous ensemble de l'autre, non ? **Dynamic Dictionary of Mathematical Functions** Encore d'après ce que j'ai compris, il s'agit de proposer une bibliothèque de d'équation typiques avec leur résolution (un peu comme si on donnait ax2+bx +c avec la méthode pour résoudre l'équation), le but étant de pouvoir rendre tout cela dynamique. Ca aidera probablement nos amis du Cern à nous fabriquer un bau trou noir ;-) **Adaptive Combinatorial Search for e-Sciences** L'objectif est de fabriquer des solveur de problèmes complexes (recherche d'ensemble solution avec fonction solution à beaucoup beaucoup de variable je suppose) à partir de la programmation par contrainte. Les langages à programmation par contraintes sont lents, c'est connu. **ReActivity** En gros, c'est la digne suite des travaux de Douglas Engelbart (le type qui a inventé la souris avec son équipe) : comment rendre plus productif un scientifique avec des outils informatiques. On va plus loin que notre ami Douglas, car l'outil devient intelligent. Un énorme potentiel là dedans, à suivre... En passant... Qui sait qui va récupérer les brevets ? C'est... **Scientific Image and Video Data Mining** En gros, encore une fois d'après ce que j'ai compris, il 's'agit de détecter des pattern "complexes" dans de la vidéo et de l'image. Complexe signifie plus seulement reconnaitre des formes, mais des raisonnement analytiques applicables sur ces images. J'adore le [texte d'introduction](http://www.msr-inria.inria.fr/Projects/copy_of_tools-for-formal-specs/tools-for-formal-specs-index) qui nous raconte que les gennnntils krosoft vont gentilment utiliser tout cela pour des choses aussi utiles que de la sociologie, de l'archéologie, toussa. Bref de la bonne conscience en barre. Bon, on remarque quand même qu'ils ont pas pu s'empêcher de lâcher "studies of consumer trends in commercials", histoire d'évoquer les choses véritablement sérieuses. Ca a du leur échappé, c'était plus fort qu'eux... Bref intéressant tout ça... Moi ce que je vois, c'est que l'Inria est encore dirigé par des fonctionnaires avec une vision économique attardée de 20 ans (je dis ça, parce que j'en ai pratiqué quelque uns...), et la seul chose qu'ils sont capable de faire, c'est de vendre leur âmes à des grosse boites. Créer des startup en se disant que certaines pourront devenir de très gros business, mais vous n'y pensez pas, c'est beaucoup trop risqué !! Et ma carrière ? Oui parce qu'en fait, quand les chargés de transfert industriels arrivent en poste, ils sont fonctionnaire stagiaire, eu égard aux statuts fossilisés de la fonction publique... Et il doivent prouver leur compétence en passant un contrat avec une grosse boite, voyez ? (bon, je suis mauvaise langue, il ont fait [http://www.inria-transfert.fr/fr/index.php](http://www.inria-transfert.fr/fr/index.php) , mais c'est à la franchouillarde, c'est pas la californie...) Voilà, j'ai fait attention à pas trop pomper le monde informatique pour celui-ci, mais c'était dommage de ne pas pouvoir continuer le très intéressant débat qui pointait...

AltStyle によって変換されたページ (->オリジナル) /