neil a écrit 428 commentaires

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.

que cette connerie du compilo de Ken Thompson qui fait rire tout le monde dans le monde de la securite.

Oui, enfin Thompson ne fait que donner une discussion et une implémentation d’un sujet qui intéressait déjà le gouvernement américain il y a 40 ans, comme il l’indique sa référence au rapport technique (qui a aussi implémenté d’autres trap doors) de l´ Electronic Systems Division (une agence avec un petit budget de 3 milliards de dollars par an).

Plein de gens ont acces aux source de Windows depuis des annees

Quand bien même tout un chacun pourrait recompiler Windows pour son usage personnel après avoir lu le code source pour vérifier qu’il n’y a pas de backdoor, si Windows ne se compile qu’avec un compilateur de Microsoft, alors cet argument est le plus pourri que l’histoire de la sécurité n’ai jamais donné, comme l’a bien montré Ken Thompson.

Donc soit tu peux nous démontrer que Windows compile effectivement avec d’autres compilos, soit ton argument est fallacieux (pour ne pas dire : de la grosse merde).

Ingénieur de recherche

tldr; ils peuvent absolument faire de l’informatique

Les gens trop cons pour ne pas aimer qu'on doive mémoriser […] utiliser Unix ?

Je ne vois pas où tu prends ce que je dis comme une insulte. Je dis surtout que X a été fait pour des gens qui en ont besoin, qui l’utilisent, et pour qui le fonctionnement est tout à fait normal. Je ne parlais que de X, mais pour UNIX c’est pareil, la base d’UNIX reste quand même POSIX c’est à dire un ensemble d’API (pour programmeurs) et d’outils en lignes de commandes. C’est le fondement même de ces systèmes d’exploitations dans lesquels lire une page de manuel est la base.

Avoir à mémoriser des raccourcis (différents, oh mon putain de dieu !) est la base de ces outils, et le fondement même de celui qui veut utiliser un outil de façon efficace. Sur mes pédales de voiture il n’y a pas marqué « frein » ou « accélateur ». Quand j’appuie sur l’embrayage, je n’ai pas un sous-menu « vitesse » qui apparaît. Se plaindre parce qu’on utilise X et que ça ne marche pas comme Windows ou Mac OS ou Android, ou je ne sais quel environnement dédié à une utilisation bureautique/surfing est un comble. C’est comme acheter un objectif Zeiss et pleurer parce qu’il n’y a pas d’auto-focus, un stylo à plume et se plaindre parce qu’il faut le recharger, ou bien d’autres choses.

Et l’intelligence n’a rien à voir la dedans, utiliser ces outils fait simplement appel à la mémoire procédurale qui se développe sans qu’on ait rien à faire, que l’on soit con ou pas.

http://lmgtfy.com/?q=x+clipboard&l=1

Bah oui, il existe différents presse-papiers sous X, avec différents comportements, et pour beaucoup de gens c’est loin d’être suffisant puisqu’ils utilisent les différents registres des divers éditeurs (eg sous VIM ou Emacs).

Pour les gens qui utilisent des machines pour surfer sur Facebook et GMail, c’est sûr c’est trop. J’avoue être très étonné que GNOME n’ait pas encore gentiment masqué ces fonctionnalités.

j'ai un accès gratuit

Il y a pourtant une énorme différence entre une chose gratuite, et une autre dont tu ne te rends pas compte que tu paies.

Sauf que les autres animaux n'étaient pas encore domestiqués

Pas du tout. La persistance du lactase (la molécule qui détruit le lactose) chez l’adulte est un exemple typique de mutation récente. La page wikipédia est, une fois n’est pas coutume, remplie de références vers des études établissant la conservation de cette mutation comme conséquence de la domestication des animaux produisant du lait. Par exemple, l’apparition significative de la mutation remonte à 7500 ans seulement, époque à laquelle la plupart des animaux producteurs de lait étaient déjà domestiqués depuis des milliers d’années.

Pour simplifier, dans un GADT par rapport au type somme classique, tu peux y mettre des fonctions en plus des type de donnés.

Non. Il n’y a pas de fonction « à l’intérieur » du type. Comme pour une somme classique, les fonctions sont indépendantes et à l’extérieur (ici c’est eval). Une somme classique s’écrirait sous la forme :

-- J’ai viré le tuple de App pour alléger
data Term = Intg Int | Add | App Term Term

eval :: Term -> Int
eval (Intg n) = n

Mais déjà là, on est bloqué aux définitions de eval Add et eval (App f x) qui retourne des fonctions de type différents. On pourrait s’en sortir en faisant retourner à eval soit un Int, soit une fonction (de deux types possibles), mais il faudrait alors tester qu’on a bien une fonction pour f dans eval (App f x) par exemple, et ça serait un test à l’exécution (avec du pattern matching développé ailleurs dans ce journal) et non pas à la compilation. Or c’est non seulement lent (exécution), inutile (le développeur ne veut jamais passer autre chose que des fonctions à App), verbeux et mal extensible (il faut rajouter tout le code de pattern matching), et sources de bugs (le compilateur aurait vu tout de suite à la compilation qu’il y avait un problème).

On peut vouloir dire au compilateur que chaque terme sera évalué à un type particulier, en lui associant un phantom type, sous la forme data Term a = ... | App (Term a) (Term a). Ainsi à chaque terme est associé un type à la compilation (il est viré à l’exécution). Mais ça ne résout pas nos problèmes, en ayant eval :: Term a -> a, il n’y a pas assez de contraintes sur a pour que le compilateur empêche un utilisateur d’écrire eval (Intg 123) :: String par exemple (en gros de convertir n’importe comment). La solution c’est d’utiliser les GADTs, qui vont apporter la flexibilité d’écriture nécessaire (le compilateur déduit que eval (Intg n) retourne un Int, et que eval Add retourne un Int->Int->Int), et la sécurité du système de types, en résumant (mal) le manuel d’OCaml :

Les GADTs sont un type somme avec des contraintes de type vérifiées à la compilation.

PS : On peut simplifier le code que j’ai donné au dessus, genre avec eval Add = (+).

C’est plus puissant parce que c’est de la PAO. Un « équivalent » libre est Scribus.

En général ce mécanisme s’appelle les view patterns et existe dans un grand nombre de langage fonctionnels par exemple en Haskell ou en F# (active patterns), vu que le concept a été introduit il y a quand même longtemps (en 1987 !). Le problème de OCaml est qu’une partie de ce qui aurait pu atterrir dans le langage a été relégué dans les outils, dans ce cas dans camlp4.

J’imagine que tu parles des GADTs dans OCaml décrits en 7.18 du manuel ? Juste parce que c’est plus facile pour moi, voilà la version Haskell :

data Term t where
  Intg :: Int -> Term Int
  Add  :: Term (Int -> Int -> Int)
  App  :: (Term (b -> a), Term b) -> Term a

eval :: Term a -> a
eval (Intg n)    = n
eval Add         = \x y -> x+y
eval (App (f,x)) = (eval f) (eval x)

On peut la charger dans l’interpréteur, et exécuter l’exemple du manuel OCaml :

 ghci> eval (App (App (Add, Intg 1), Intg 1))
 2

L’exemple définit un AST fonctionnel dont les termes sont soit des entiers, soit des additions d’entiers, soit des applications d’une fonction à un argument. Les ASTs sont couramment utilisés comme représentation interne des compilateurs et autres interpréteurs.

Dans ce cas, on considère l’addition comme un objet de première classe, c’est à dire qu’on peut le passer en argument, le retourner, etc, et on considère aussi qu’une fonction est curryfiée, c’est à dire qu’une fonction de deux arguments est en fait une fonction de un argument qui retourne une fonction de un argument. Ces deux concepts sont à la base de la programmation fonctionnelle. Un terme d’application fonctionne lui aussi de manière fonctionnelle, en prenant en paramètre une fonction (qui n’a qu’un argument, comme toute fonction :p), un argument, et retourne le résultat de cette fonction.

Avec l’aide d’un interpréteur, on comprend facilement ce que fait chaque terme de l’expression :

ghci> :t Intg 1
Intg 1 :: Term Int
-- La construction d’un terme entier est triviale

ghci> :t App (Add, Intg 1)
App (Add, Intg 1) :: Term (Int -> Int)
-- On construit un terme qui représente l’addition avec 1, en Haskell ce serait (+1)
-- On voit que le résultat est un terme-fonction qui prend un argument entier, et retourne un entier

ghci> :t App (App (Add, Intg 1), Intg 1)
App (App (Add, Intg 1), Intg 1) :: Term Int
-- On utilise le résultat précédent (qui était un terme-fonction) en lui passant un entier

Utiliser les GADTs va permettre de vérifier à la compilaition qu’on ne construise pas de terme erronés :

ghci> :t Intg 1.0
-- Erreur : on ne peut pas convertir implicitement 1.0 en Int
ghci> :t App (Add, Add)
-- Erreur : les paramètres de App doivent être de type b->a et b, ici ils sont identiques

Il y a d’autres applications que cet usage trivial de vérification d’arbres bien formés, exemple qu’on ferait en POO avec des classes, et les design patterns adéquats pour l’évaluation.

De façon générale, mais ce n’est que mon avis, les fonctions avancées des langages fonctionnels sont surtout intéressantes parce qu’elles permettent d’écrire rapidement et de façon très concise (surtout en Haskell) du code sûr et performant. Le cas d’utilisation typique est quand on travaille dans des startups, dans la recherche (scientifique ou R&D), dans lesquels on doit avoir rapidement un code qui marche pour montrer des nouveaux concepts (en gros des cas où l’important ce n’est pas le code mais ce qu’il permet de montrer). C’est mon cas, l’informatique n’est absolument pas mon domaine, juste un outil dont je me sert pour une partie de mon boulot (simulations numériques, affichages prouvables, visualisations, traitement de données). Je n’ai pas le temps de débugger, d’avoir des erreurs à l’exécution (ou du code lent de par les vérifications à l’exécution), et mon code ne sera lu ou utilisé que par un nombre nul ou très très réduit de gens, ce qui compte c’est de vérifier les idées.

C’était principalement de l’humour pour dire qu’il y a toujours des systèmes de type plus puissant, c’est à dire permettant de détailler encore plus finement ce que fait un élément d’un programme (une fonction par exemple). L’exemple de l’OP avec un alias de type pour les heures par exemple, permet de définir des fonctions typées comme :

-- Date de Pâques pour une année donnée
easter : Int -> Day_of_year

et le compilateur va se charger de vérifier qu’on ne retourne pas une erreur (un entier négatif, ou supérieur à 366).

En Haskell et OCaml, par exemple, il y a tout un tas d’autres apports du système de type. Par exemple, avec les GADTs, on peut vérifier à la compilation que tous les arbres binaires que l’on va construire sont bien balancés, ou qu’une liste passée en paramètre est toujours non-vide. Ça permet d’avoir une sorte de pattern matching mais à la compilation plutôt qu’à l’exécution. On peut aussi utiliser le système de type pour faire des calculs à la compilation (un peu comme le template meta-programming en C++, mais de façon propre :p).

Les GADTs viennent des systèmes de types dépendants, dans lesquels on peut par exemple typer le fait qu’un programme prenne en entrée une liste de n éléments, et sorte une liste de (n+1) éléments :

-- Ajoute un élément à une liste de taille n contenant des a
addElem : List n a -> L (n+1) a

Et c’est le système de types du compilateur qui va se charger de vérifier ça à la compilation (en fait écrire un programme bien typé est la même chose qu’écrire une preuve, que le compilateur va vérifier). Les types dépendants sont classiquement utilisés dans les systèmes de vérification de programmes comme Coq ou Agda, mais les fonctionnalités commencent à arriver dans OCaml et Haskell. Il y a aussi des expériences de langages généralistes entièrement dépendants tels que Idris ou F*.

Pour les systèmes de types homotopes, il va encore falloir attendre un moment avant d’avoir des jolies applications. En gros, en plus d’unifier de nouvelles branches des mathématiques, ça permet d’avoir des types beaucoup plus jolis, ou de transférer une preuve sur un algorithme naïf, à une preuve sur un algorithme optimisé.

Le système de pattern matching de OCaml/Haskell/Scala/F# semble pas mal, mais essaye un langage qui a des types dépendants (ou des types homotopes !), c’est tellement simple à vérifier, que l’on se demande pourquoi les autres langages n’ont pas l’équivalent.

Quand CHP dit « riche » il parle probablement à un niveau non franco-français. En gros, si tu peux te permettre de voyager, d’acheter des pastilles, etc, tu es riche, et l’eau ne sera pas un soucis.

Réalise-t-on par exemple que le couple oreilles/cerveau forme un incroyable analyseur spectral infiniment plus fin que les performances lamentablement grossières de nos yeux dans ce domaine.

C’est complètement hors-sujet, mais tu es en train de comparer les performances du couple oreille/cerveau à celle de la partie purement optique de la vision. Ce faisant, tu omets volontairement de parler du traitement de l’information visuelle dans le cerveau, qui occupe quand même entre le quart et la moitié du cortex selon les primates (dans les 30% chez l’humain, que tu peux comparer aux 3% pour l’audition). On pourrait aussi parler de toutes les structures sous-corticales de pré-traitement, sans compter toute la partie motricité oculaire.

Effectivement l’audition humaine est un « incroyable analyseur spectral ». Mais il ne faut pas déconner, l’un des modèles d’audition les plus utilisés pour représenter l’audition humaine est le chinchilla. On est à des millions d’années d’évolution de là au niveau de la vision.

En même temps le « pétrissage » de l’OP est

remuez avec la cuillère en bois jusqu'à obtenir une pâte uniforme

le titre de la page liée pourrait tout à fait aller pour ce journal :-D

La mie est compacte quand la pâte lève mal. En supposant que les levures soient bonnes, généralement c’est parce que la pâte n’est pas pétrie comme il faut/assez longtemps, ou qu’elle manque d’eau. La pâte sera plus légère si on y ajoute une bonne quantité d’eau, mais sa liquidité la rend alors dure à pétrir, en particulier quand on n’est pas habitué à manipuler un pâton presque liquide. Il y a aussi un grand nombre de techniques pour rendre la pâte encore plus légère, par exemple en la tournant comme de la pâte à croissants.

La croûte se contrôle par la chaleur et l’humidité du four. Pour avoir une pâte fine, il faut que le four soit très chaud quand le pain entre, puis le baisser durant la cuisson. Pour avoir une croûte dorée, il faut un maximum d’humidité lors de sa formation. Le contrôle de l’humidité est un facteur assez problématique pour des fours qui ne sont pas conçus pour faire du pain (la quasi-totalité des fours domestiques), et avoir un pain qui ressemble à celui de la boulangerie suppose un certain DIY du matériel (genre en redirigeant la vapeur d’une cocote minute), en plus d’une énorme expérience des préparateurs (plus la culture des levures et autres levains, plus la sélection des farines, plus …). On peut quand même faire des petits trucs comestibles (genre du pain-brioche sans croûte) en débutant :-)

Avec une fermentation aussi courte tu es loin du levain, c’est une poolish.

Les opérations ensemblistes, les hiérarchies automatiques, et tout un tas d’autres trucs.

Par ailleurs, je remarque que pour les femmes, l'apparence semble encore être un point de fixation pour nombre d'entre nous. Si elle est belle, si elle est maquillée, si elle est nue, si elle ne s'épile pas, si elle a des boutons, des capitons, des kilos en trop, les cheveux gras, un gros nez, on en parle: les diverses publicités en attestent. C'est formidable. Mais ça n'a rien à faire sur Linuxfr.

Est-ce que tu veux dire que les femmes ne parlent pas du cul, des abdos, des pectoraux, de la taille des penis, et d’autres caractéristiques physiques des hommes ? Elles n’en ont en fait que pour la beauté intérieure ? Quant à la publicité, elle montre tout le temps des vieux hommes poilus, boutonneux, et avec de la bedaine (tape, au hasard, calvin klein sur Google Images) ?

Merci d’avoir contribué au mélange constant entre sexisme et sexuel, tout en rajoutant une prétendue asexualité aux femmes.

i.e. ca te coute moins de $1000/an pour toute la smala, pas loin de ce que tu paierais pour ta mutuelle en france

Je ne sais pas où tu travailles, mais perso mon employeur me paie ma sécu et 1000$ ça n’est pas suffisant pour payer deux mois de cotisations. C’est non seulement une des cotisations les moins chères de mon employeur (qui fonctionne par groupes de plusieurs milliers d’employés) vu que je suis dans une catégorie avec peu de risque, en plus en HMO et négocié chaque année, mais aussi une des cotisations les moins chères du coin, vu que mon employeur a des dizaines de milliers de contrat pour négocier. Si ta sécu passe par une petite boîte, ou pire si tu dois la payer toi même, bah c’est beaucoup plus cher que ça, et tu risques de devoir payer une partie de ta poche en cas de soucis.

Et non, en France ce n’est pas la mutuelle qui te rembourses l’équivalent, c’est la sécu. Et oui, ça coûte cher aussi, mais c’est loin d’être autant vu qu’on paye la sécu des jeunes, des vieux, et des défavorisés.

De la crêche à l’université il faut compter dans les 20k$/an par enfant (un peu plus en crêche/maternelle et à l’université, un peu moins entre les deux) pour la scolarité (le double de la France). Là encore il faut rajouter la sécu et tout le tralala. Impossible à assumer pour les salaires les plus bas, et on voit même un grand nombre de gens qui préfèrent attendre (très) longtemps pour faire des gosses (et, oh!, encore des jumeaux!).

Car depuis 1996, Linux est modulaire ce qui enlève l'un des plus gros inconvénients du monolithique et le rapproche d'un système micro-noyau même s'il manque pas mal de choses.

Pas du tout. Le fait que tu puisses rajouter où enlever des composants à chaud ne change rien à l’élément de base d’un micro-noyau : mettre le maximum en espace utilisateur. Au contraire ça empire le problème puisqu’à n’importe quel moment un bout de code potentiellement dangeureux (qui fait foirer l’espace noyau) peut être inséré en mode privilégié.

i386 ou amd64 ? J'étais en amd64

Amd64. Comme dit roychris, mes partitions formatées depuis le cd d’install commencent en 2048. Ça laisse de la place pour les 32k du core.

Je viens de faire une installation de wheezy en mdadm+lvm (raid1) entièrement via l’installeur du cd netinstall (avec partitionnement dans le même installeur), et je n’ai eu absolument aucun soucis ni aucun message d’erreur. Ça serait cool d’avoir le rapport de bogue qui correspond à ce dont tu parles pour qu’on puisse comprendre quelles sont les conditions du problème.