Perthmâd a écrit 224 commentaires

Le terme de juriste qui en jette, c'est griveler.

Certes, il tiennent une position extrême, et loin de moi l'idée de la justifier, mais il faut quand même reconnaître qu'aujourd'hui, l'équilibre du droit d'auteur est rompu, et que ce n'est pas en jouant l'autiste façon MPAA qu'on résoudra le problème.

Je suis convaincu que 70 ans après la mort de l'auteur pour s'élever dans le domaine public[1], c'est beaucoup trop long, surtout à l'ère de l'Internet. OK, aujourd'hui nombreux sont les gens qui produisent des ressources libres ; cependant, il y a une énorme zone grise qui ne cesse de croître[2], et nous sommes en train de nous tirer une balle dans le pied au niveau de la diffusion de la culture.

C'est pourquoi les zozos de The Pirate Bay ont sinon l'art du moins l'envie de poser le problème en termes clairs. Soyons réaliste, demandons l'impossible.

[1] Sans compter les magouilles sur l'interprétation de la loi avec le coup du « mort pour la patrie », et les années de guerre qui auraient dû être incluses dans la réforme des 70 ans... Et avec un peu de mauvaise foi on obtient ça : http://fr.wikisource.org/wiki/Discussion_Wikisource:Demande_(...)

[2] http://fr.wikipedia.org/wiki/Loi_am%C3%A9ricaine_d'extension(...)

Encore raté, c'est une erreur d'arrondi flottant ! la bonne réponse est évidemment 0 : il est bien connu que le clavier bépo est une invention des envahisseurs de la planète Zokbar III qui s'en servent pour sécuriser les données de leur plan d'invasion.

J'ai fait le bench avec OCaml, et le code natif est plus rapide que le C compilé avec gcc sans optimisations, par contre il y a un facteur deux en faveur du C avec -O3.


let entries = 10000

let loop entries =
let d = Array.make entries 1 in
for i = 2 to pred (entries / 2) do
let j = ref (2 * i) in
while !j < entries do
d.(!j) <- d.(!j) + i;
j := !j + i
done
done;
for i = 0 to entries - 1 do
if d.(i) < entries && d.(d.(i)) = i && i <= d.(i) then
Printf.printf "%i %i\n" i d.(i)
done

let () = for i = 0 to 100 do loop entries done


Par contre c'est clairement pas une manière fonctionnelle d'écrire les choses, et habituellement, je n'utilise jamais les boucles for et while en OCaml.

Non, c'est un JC des Caux.

J'aurais plutôt dit :

Les fonctionnalités qui ne se voient pas n'existent pas.

Scala, je connais pas, mais voilà un résumé biaisé des autres.

Le Lisp me colle des boutons, car je déteste le typage dynamique. Sans parler de la syntaxe abstruse (Lots of Stupid and Insipid Parenthesis).

De l'autre côté de la barrière, Haskell et OCaml étant des ML, ils profitent tous deux de l'inférence de types, et ça c'est vraiment bien. J'ai une nette préférence pour OCaml, cependant, car il est multiparadigme et call-by-value. Il est vrai que l'utilisation de monades rajoute une couche de sûreté sur le code, mais je trouve ça lourd ; de même, on peut avoir besoin de call-by-need par moment, mais on peut l'émuler en call-by-value, donc ça en limite l'intérêt.

Notons quand même à la décharge d'Haskell que GHC a plein d'extension qui tuent, genre les typeclasses et l'ordre supérieur, mais j'imagine que ça ne sert pas trop à un débutant.

Ou mieux, essaye des langages d'hommes, comme OCaml ou Haskell. L'inférence de type c'est déjà une superbe protection contre les erreurs d'inattention, alors que le dynamisme total de Python est la porte ouverte à toutes les fenêtres.

L'étape d'après, si tu veux être sûr de ne pas laisser passer un bug, c'est de prouver ton programme.

mais tu possède tous les fermants nécessaires en toi

Pour quelqu'un qui veut faire du code ouvert, c'est plutôt un handicap !

Le diable est dans le détail.

Par expérience, je pense qu'on comprend beaucoup mieux une démonstration après l'avoir implémentée en Coq qu'après l'avoir prouvée trois fois sur papier.

Je veux bien croire que la première preuve de 1976 était peu fiable, vu qu'elle était écrite dans un langage qui ne garantissait en rien la correction du résultat (me semble que c'était du C, mais je ne suis pas sûr). Mais dire que la preuve moderne en Coq est sale[1], c'est transférer la saleté du problème vers la preuve.

La démonstration du théorème des quatre couleurs est fondamentalement technique au vu de la quantité de sous-cas à explorer. Beaucoup de problèmes de graphes sont dans cette situation, ce qui fait que la preuve ne peut pas être facilement appréhendée par un être humain. Et ça n'est pas pour plaire aux matheux, qui n'arrêtent pas de grogner contre la preuve assistée par ordinateur sous des prétextes philosophiques.

[1] Par contre, le code de Coq est plutôt sale, lui.

Histoire d'augmenter encore un peu plus le désarroi de Madame Michu, Apple frappe un grand coup :

Fourni avec chaque nouveau Mac, Boot Camp vous permet d'exécuter Windows en mode natif, comme si votre Mac était un PC.

Ça fait juste belle lurette que les Macs sont des PC...

Moi, je crois que ça va coûter très cher à BP de toute façon :

http://www.lefigaro.fr/societes/2010/04/30/04015-20100430ART(...)

Et à propos de ta remarque, les formes deux-vingts et trois-vingts sont attestées en ancien français, qui connaissait un système vigésimal dans la langue populaire.

http://fr.wikipedia.org/wiki/Syst%C3%A8me_vic%C3%A9simal

Bon, je vais mettre tout le monde d'accord en jouant mon réactionnaire.

Autrefois, quand la langue française devait inventer des mots, elle créait des néologismes repompés du grec et du latin. Ça en jetait, vu le prestiges de ces langues-là. À un point tel que même ces envahisseurs de la perfide Albion nous repiquaient ces mots.

Seulement, aujourd'hui, tout se perd ma bonne dame. Plus personne ne parle le latin ou le grec, et forcément, ces vieux ronds de cuir de l'Académie, pour faire hype[1], préfèrent utiliser des mots incongrus (la liste est longue), voire remplacent un emprunt par un autre (le fameux ramdam[2], altération de l'arabe ramadan...)

Ainsi donc, pour le cas du multi-threading, je propose multilice si l'on penche pour nos amis latins, ou encore polymite, si l'on préfère l'hellène. C'est-y pas mieux comme ça ?

[1] Emprunté au grec...

[2] Moi j'aurais bien traduit buzz par bourdon, comme celui qu'on met sur les binious...

Et il y a encore plus puissant que le goto et les autres formes de contrôle du pauvre : call/cc, la primitive ultime des langages fonctionnels.

Fortement typable, sûr, efficace (ou pas).
Incompréhensible pour le profane.

Que demande le peuple ?

Si tu aimes les scripts des langages pour scientifiques, je te conseille un bien meilleur langage tout aussi Turing-complet : Ltac, le langage des tactiques de Coq. Dynamiquement typé, à la syntaxe abstruse et à la sémantique pas clairement définie.

Une question en l'air, les langages d'assistant à la preuve sont-ils vraiment des langages de programmation ? Ils ne sont pas Turing-complet, la faute à Gödel : va coder un interpréteur d'un tel langage dans lui-même...

Ça n'a pas trop de sens de dire qu'on ne peut pas trouver la valeur exacte... Il serait plus correct de dire que ce nombre n'admet pas de décomposition analytique « sympathique. »

Parce que sinon, tu peux poser arbitrairement que telle symbole représentera ce nombre[1], et paf ça fait des chocapics.

[1] On fait ça d'habitude avec les formules récurrentes : e, π, ζ(2)...

Techniquement, on peut aussi faire une machine de Turing avec un ruban infini d'un seul côté.

Ça a le même pouvoir expressif en termes de calculabilité. Une manière de voir ça c'est qu'un ruban bi-infini, tu peux choisir arbitrairement une case et le plier en deux à cet endroit : te voilà avec un ruban infini d'un seul côté.

Par contre, en termes de complexité temporelle, il me semble que tu récupère un petit overhead à cause de la transformation (ça doit être un facteur constant 2 à vue de nez).

Si et c'est bien pour ça que ça existe pas les machines de Turing.

Dans le même genre, mais en Légo (et en flash) :

http://www.youtube.com/watch?v=cYw2ewoO6c4

Et histoire de nous changer un peu des éternels débats stériles vi-emacs ou KDE-Gnome, je vous propose un troll modèle de calcul : machine de Turing ou lambda-calcul ?

C tro for se sit ,jkif tro dla bal!

Un grand pouvoir implique de grandes responsabilités.

Je ne suis pas d'accord sur les deux points.

D'abord, la différence entre un coca et un pepsi, c'est assez criant. Les deux n'ont pas du tout le même goût.

Par ailleurs, le JPEG est (souvent) reconnaissable au fait qu'il quadrille l'image par carrés de 8×8 pixels, et ça fait des trucs moches dans les zones où il y a beaucoup de variations à cause de la transformée de Fourier. Bon, c'est sûr que si tu fais ça avec des résolutions de fou, ça ne se verra pas. Mais ça reste moche.

Faut leur faire faire du Coq (cf. Coq_(logiciel)) !

Ils n'ont plus qu'à extraire le programme de la preuve :D

Techniquement on s'en fiche complètement de la distro sur laquelle tu tournes. Tu reste sous Emacs, c'est tout.

Rapport au concours, tu parles de l'épreuve de l'ENS ? Si c'est le cas , vu que cette année c'est à Lyon, il y a des chances que tu me croises parmi les personnes qui t'accueilleront :P

Bon courage, sans ça.