Je crois que tous les chercheurs en maths français font de l'info
J’imagine que tu te réfères à « utilisable par des mathématiciens non informaticiens » ? Au risque de te surprendre, une bonne partie des mathématiciens n’en ont strictement rien à foutre de l’informatique, et ont même une certaine répulsion à utiliser des ordinateurs. De façon plus explicite, Cosnard parle ici de Coq, un outil de vérification automatique de preuves basé sur les types dépendants. C’est l’un des logiciels libres développés par l’INRIA (sous LGPL) et la référence absolue en la matière (il y aussi Agda basé sur une syntaxe Haskell, lui même un excellent langage libre développé chez Microsoft !). Mais ça reste encore peu attractif pour la majorité des mathématiciens (qui aiment beaucoup faire des preuves à la craie).
Utiliser le logiciel, le plus en retard et le plus fermé(windows media player) comme base de développement
Tu es encore à côté de tes pompes. Les chercheurs de ces centres de recherche ne vont pas utiliser les algorithmes dont tu parles (sauf si ça sert de base, et là encore ils sont libres), ils les développent.
Bref, la recherche, autant chez Microsoft qu’à l’INRIA, nous apporte d’excellents langages (eg Coq, Haskell, Caml), logiciels et bibliothèques (eg CImg, CGAL) libres, et d’excellents algorithmes à intégrer dans nos outils favoris (eg G'MIC). Ce qui n’empêche pas leurs dirigeants d’émettre des avis dénoncés par leurs employés, ou de développer aussi des logiciels proprios pourris.
[^] # Re: INRIA, contre les logiciels libre?
Posté par neil . En réponse à la dépêche Le parlement français adopte une disposition législative donnant la priorité au logiciel libre. Évalué à 7. Dernière modification le 10 juillet 2013 à 19:24.
J’imagine que tu te réfères à « utilisable par des mathématiciens non informaticiens » ? Au risque de te surprendre, une bonne partie des mathématiciens n’en ont strictement rien à foutre de l’informatique, et ont même une certaine répulsion à utiliser des ordinateurs. De façon plus explicite, Cosnard parle ici de Coq, un outil de vérification automatique de preuves basé sur les types dépendants. C’est l’un des logiciels libres développés par l’INRIA (sous LGPL) et la référence absolue en la matière (il y aussi Agda basé sur une syntaxe Haskell, lui même un excellent langage libre développé chez Microsoft !). Mais ça reste encore peu attractif pour la majorité des mathématiciens (qui aiment beaucoup faire des preuves à la craie).
Tu es encore à côté de tes pompes. Les chercheurs de ces centres de recherche ne vont pas utiliser les algorithmes dont tu parles (sauf si ça sert de base, et là encore ils sont libres), ils les développent.
Bref, la recherche, autant chez Microsoft qu’à l’INRIA, nous apporte d’excellents langages (eg Coq, Haskell, Caml), logiciels et bibliothèques (eg CImg, CGAL) libres, et d’excellents algorithmes à intégrer dans nos outils favoris (eg G'MIC). Ce qui n’empêche pas leurs dirigeants d’émettre des avis dénoncés par leurs employés, ou de développer aussi des logiciels proprios pourris.