Ah oui, je l'avais oublié celui-là, Pascal. Pour D... je suis un peu dubitatif étant donné que c'est un langage très peu utilisé, mais certainement de qualité.
Pour ce qui est de compiler du C avec du C++... je répondrai ce que répondent les vrais programmeurs C++ (mais je n'en suis absolument pas un) : "On ne fait pas du C++ à la mode C".
Envoyé par alex_pi
Pour ce qui est des performances asymptotiques, on est malheureusement forcé de constater que les structures modifiables comme les tables de hachage ou les tableaux sont pour beaucoup d'opérations, mais pas pour la totalité, plus performantes (asymptotiquement) que des AVL ou des listes, sous toutes leurs formes. Pour certaines opérations les strucutres fonctionnelles peuvent s'avérer plus efficaces (asymptotiquement), mais pas pour toutes.
Enfin, je reste persuadé que le problème de la performance en termes de temps de calcul de nos chers programmes, scripts d'affichage de pages web, et tout le beau monde va revenir, un jour à l'autre, sur le devant de la scène. La puissance des CPU stagne (attendons tout de même les premiers CPU gravés en 45 nm... je pense que la différence sera très significative), mais les programmes deviennent plus gros chaque jour, programmés dans des langages lents (Java, PHP, Ruby, Python), avec tout un tas de manies logicielles qui ne servent à rien, sinon à faire le beau devant son patron (comme cette manie de tout sérialiser en XML)...
Il y a quelques années, quand tu avais l'ADSL à la maison, la page s'affichait instantanément : c'était pratiquement que du HTML. Aujourd'hui, les débits ont grossi d'un facteur au moins 10 en zone urbaine, mais beaucoup de pages web mettent jusqu'à plus de 5 - 10 secondes à s'afficher ! Personnellement, je vais très souvent sur eBay, et franchement, il y a des fois où je pense que j'étranglerais les développeurs ! En plus ils ont changé ça (ebay.com, car certains autres sites ebay l'avaient fait avant), et maintenant, c'est encore plus lent !
Résultat, en 5 ou 6 ans : CPU x 5 ou 6 (pas en fréquence, hein, mais en nombre d'opérations !), RAM x 10 (facilement...), débit x 10... mais tout est plus lent, mis à part les video.
Le paradoxe est là.
A quoi sert la puissance de nos ordinateurs ?
Et bien elle sert à faire des trucs aussi intelligents que getTrucMuche(b){ return b.getMachinTruc()}... mais 1 000 000 000 de fois pas seconde.
Dans les entreprises, avant, on imprimait. Avec l'ordinateur, tout le monde a cru que l'on n'imprimerait plus. Faux, car avec l'ordinateur on peut imprimer deux fois plus vite... et c'est ce qui s'est réellement produit.
Et bien là, c'est pareil : ce genre de truc, personne ne pouvait se le permettre sur des 68000, à moins de le faire peu souvent. Avec l'arrivée du GigaHertz, tout le monde a pensé que tout irait plus vite. Et bien c'est faux, car avec le GigaHertz, on peut se le permettre jusqu'à 1 000 000 000 de fois par seconde.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
On peut utiliser des structures "modifiables" dans un langage fonctionnel. Par exemple OCaml. On peut même souvent les utiliser en conservant la transparence référentielle, en les utilisant de manière "linéaire", c'est à dire en conservant en permanence au plus une référence (adresse, etc.) en écriture vers cette structure (en gros : pas d'aliasing). On peut même demander au compilateur de vérifier cette linéarité à notre place, en la rendant explicite, par exemple par le biais de monades (Haskell) ou de types uniques (Clean), ce qui permet leur utilisation dans les langages fonctionnels "purs".Pour ce qui est des performances asymptotiques, on est malheureusement forcé de constater que les structures modifiables comme les tables de hachage ou les tableaux sont pour beaucoup d'opérations, mais pas pour la totalité, plus performantes (asymptotiquement) que des AVL ou des listes, sous toutes leurs formes. Pour certaines opérations les strucutres fonctionnelles peuvent s'avérer plus efficaces (asymptotiquement), mais pas pour toutes.
On peut donc programmer de façon globalement fonctionnelle, en utilisant au besoin des structures modifiables, et donc en profitant de leurs performances asymptotiques.
Bien sûr, c'est aussi ce que je recommande, partant du principe que C++ est beaucoup mieux que C. Mais si tu as peur de perdre quelques cycles en instanciant une classe, c'est peut-être la solution pour toi. Toujours est-il que les performances de C++ sont très bonnes - ce n'est pas plus lent qu'OCaml, en moyenne.Pour ce qui est de compiler du C avec du C++... je répondrai ce que répondent les vrais programmeurs C++ (mais je n'en suis absolument pas un) : "On ne fait pas du C++ à la mode C".
À pouvoir utiliser des outils de plus haut niveau et diminuer le temps de développement.A quoi sert la puissance de nos ordinateurs ?
Peut-être, mais dans ce cas, c'est Perl, Ruby, JavaScript, PHP et Python qui vont perdre de l'intérêt. Java, C++ et C# resteront, leurs performances sont correctes. Les machines virtuelles s'améliorent avec le temps.Enfin, je reste persuadé que le problème de la performance en termes de temps de calcul de nos chers programmes, scripts d'affichage de pages web, et tout le beau monde va revenir, un jour à l'autre, sur le devant de la scène.
Y a un truc que je ne comprends pas. Tu as dit:
C'était ironique ? Parce que sinon, il va falloir se faire une raison. Ces propriétés sont complètement indécidables. Donc il va falloir soit une forme de type dépendant, soit une possibilité de fournir des preuves au système (en fait si le premier, il faut aussi le deuxième..). Et à coté de ça, tu dis que Coq c'est "de la branlette". Il va falloir choisir à un moment.
Ou alors Perl, Ruby, JS et PHP se doteront de VM décentes. Et c'est justement ce qui est en train d'arriver (bon peut-être pas PHP, il faut pas déconner non plus).Peut-être, mais dans ce cas, c'est Perl, Ruby, JavaScript, PHP et Python qui vont perdre de l'intérêt. Java, C++ et C# resteront, leurs performances sont correctes. Les machines virtuelles s'améliorent avec le temps.
Si, PHP compile sous .Net et ça marche bien. En effet, tous ces langages vont beaucoup améliorer leurs performances. Mais ça restera toujours plus lent, du fait du typage dynamique.
Pour toutes les tâches où les performances ne sont pas cruciales, je pense aussi que ces langages-là vont rester.
Non, je ne dis pas que Coq c'est de la branlette, mais ce n'est pas, à ma connaissance, un langage de programmation, même si on peut lui faire cracher de l'Haskell ou du OCaml... et encore moins un outil très largement diffusé. Je ne lui ôte aucune vertu, ceci dit.
Pour ce qui est de la vérification des tailles à la compilation, je confirme que ce n'est pas de l'ironie. J'y travaille, d'ailleurs, même si mes autres activités ne me permettent pas de m'y consacrer à plein temps.
Il y a deux problèmes.
1- le problème de débordement d'indice, qui est indécidable.
2- le problème de s'assurer que les matrices, ou listes, sont utilisées avec les bonnes tailles, et ce, quelques soient les tailles, qui lui est complètement décidable.
Vérifier la 2- ne veut pas dire que l'on vérifie la 1-, bien-sûr.
Par exemple, si une fonction prend deux listes en argument, la deuxième devant être, pour des raisons algorithmiques, de taille double, le vérifier à la compilation.
Désolé, mais je ne donnerai pas plus de détails sur le forum.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Je ne me suis pas très bien exprimé.
C++ n'est pas lent, mais les pratiques, parfois très lourdes, des gens qui programment en C++ font que les codes C++ sont plus lents que leurs équivalents C.
Je ne parle ici que pour ces programmes qui ont absolument besoin de hautes performances, comme les programmes de calcul intensif, mais parfois, si les programmes étaient faits en C, donc si ils adoptaient un modèle de programmation et d'architecture plus simple, ce serait pas plus mal à mon avis.
Envoyé par InOCamlWeTrust
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Exact ! J'ai des critères différents! J'ai écrit pas mal de code depuis une trentaine d'années et j'ai souvent entendu dire autour de moi que l'important était que le code marche. C'est-à-dire qu'il soit sans bug. Or, pour moi, ce n'est vraiment pas le critère essentiel, au départ. J'ai très souvent eu à intervenir sur du code pondu par d'autres. J'ai déjà vu du code qui marche parfaitement sauf qu'il est complètement incompréhensible et donc toute tentative d'évolution est extrêmement coûteuse et risquée. La moindre petite modification et tout le "bel" ensemble s'écroule sous le poids de ses rustines. Du coup, effectivement, il marche bien car personne ne veut (ne peut!) y toucher. Je préfère de loin un code avec une structure judicieuse et claire, avec de bons modules simples et qui ont du sens. De cette manière, même si le code est bourré d'erreurs, celles-ci sont faciles à détecter et à corriger. Et les évolutions sont alors grandement facilitées.
Pour moi, c'est d'ailleurs le critère pour voir si le code est bien fait: les évolutions sont simples à mettre en oeuvre.
Ce que j'ai décrit ici s'applique aussi à mon propre code. Comme je n'ai pas une bonne mémoire, j'ai besoin que mon code soit bien organisé et documenté pour que je puisse m'y retrouver, même au bout de quelques semaines, mois ou années.
Évidemment, la robustesse du code est indispensable lorsque la tolérance aux erreurs est faible (logiciel médical, fusée, etc.).
)jack(
À moins qu'on n'ait pas le même sens du terme « essentiel », il me semble que ce soit essentiel que ton code marche sans bug, mais pas suffisant certes. Le code le plus modulaire, robuste, rapide, ce-que-tu-veux, est inutile s'il ne respecte pas les besoins et s'il ne « marche » donc pas.
Non ?
C'est évidement indécidable et la vraie question est de savoir s'il est possible de trouver une approximation sure, à l'expressivité raisonnable et passablement utilisable, le tout sans système de preuve. Et dans l'état actuel des choses, j'en doute. Mais vu que tu ne parleras pas de ta solution, fin de la discussion.
Moi je parle bien du point 2-, et non du 1-.
L'expérience montre que 80% - 90% des erreurs dans le programmes de calcul numérique sont dûs à des erreurs de dimensions. Or il est possible en mettant un mécanisme très simple à l'utilisation, et absolument pas contraignant, d'en vérifier la bonne correspondance.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
J'ai bien compris que tu parlais des dimensions matricielles. Simplement, si les dimensions sont dynamiques, on se retrouve avec des quantificateurs universels (il faut bien dire que la multiplication est vraie pour tout n, ou qu'il existe un m tel que la fonction retourne une matrice de taille m x m), et si on veut autoriser les gens à produire des matrices dont les dimensions sont obtenues par multiplication, on sort de l'arithmétique de Presburger, et là, les contraintes ne sont plus décidables. Mais si tu as quelque chose de plus précis, moi ça m'intéresse :-)
On peut bien sûr définir le type des matrices de dimension n*m, comme celui des listes de longueur l, puis imposer que les opérations se passent uniquement sur des dimensions compatibles. Le problème est de vérifier statiquement que des dimensions obtenues dynamiquement seront compatibles entre elle. Et c'est là que ça se corse salement.
Pour les matrices, si j'ai une fonction de création, il faut lui donner le type (n : int) -> (m : int) -> 'a -> mat n m 'a . Et là on a des types dépendants ! Ou à la rigueur, pour faire uniquement des types indicés, avec des types singletons, forall n, m : Int, (int n) -> (int m) -> 'a -> mat n m 'a. Ca devient vite pénible. Ensuite, quand j'ai trois entier m, n, p, que je crée deux matrices par new_mat m n 42 et new_mat n p 69, il faut que je sois capable de suivre d'une façon ou d'une autre que les deux dimensions sont compatibles (au passage, il faut bien entendu que n soit non mutable, sinon c'est foutu) . Mais évidement, les deux matrices sont rarement créé l'une à coté de l'autre. Et si elles étaient créées de façons aussi simple, il y aurait peu de chance de se planter à la base, même sans système de vérification.
Pour prendre des exemples plus simples, sur les listes. Si j'écris la fonction me retournant la liste des diviseurs d'un nombre n, je vais lui donner le type int -> exists l, list l int. Et là je n'a plus seulement une liste, mais un paquet existentiel à ouvrir à chaque fois que je veux atteindre ma liste, et à refermer proprement.
Ensuite on veut écrire des fonctions sur les listes. Une simple fonction de tri par exemple, dont on va vouloir s'assurer qu'elle conserve la taille de la liste. Celle de la lib standard de Caml ne peut pas s'écrire parce qu'on a des listes de listes, et que les listes internes n'ont pas une taille constantes (ou alors on se traine des list l (exists m, list m 'a mais y a moyen d'en chier, surtout pour que le typeur/système s'assure que la taille est conservée). Mais même un simple tri fusion est loin d'être trivial à typer. Prenons l'opération de fusion
Si je veux que ma fonction de tri montre qu'elle conserve la taille, il faut que le système vérifie l'invariant. A condition de le lui fournir, ça doit être possible, puisqu'on n'a que des additions. Mais ce n'est pas trivial.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6 let rec fusion l1 l2 = match l1, l2 with | [], l | l, [] -> l | t1 :: q1, t2 :: q2 -> if t1 <= t2 then t1 :: fusion q1 l2 else t2 :: fusion l1 q2;;
Et dès que les dimensions sont obtenues à partir de produit d'entier (par exemple en découpant une matrice en sous matrices), on sort de l'arithmétique de Presburger, et les contraintes à vérifier (à supposer que l'utilisateur explicite ces contraintes !) ne sont plus décidables.
Bref, je ne dis pas que c'est impossible de proposer un système utilisable. Je dis juste que c'est très complexe et que je suis dubitatif que ce soit faisable sans un système de preuve sur les programmes.
C'est bien, je vois que la réflexion avance dans le bon sens... mais je continue à conserver de l'avance !
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Partager