[Débat] Que pensez-vous du Langage Anubis ?

[Caine]

Il y a déjà un forum sur le site même de l'auteur.

Et ce langage est très intéressant.

Ma compétence de prédilection est sans nul doute le débug. J'ai programmé dans plus de 10 langages.

Anubis ma immédiatement convaincu.

[@drien]

ça manque un peu d'explications sur le déploiment, dès que j'ai le temps de m'y mettre et de tester des programmes j'écrirais peut-être un petit truc...

[Caine]

Le déploiement est simple:
Il faut bien sûr l'archive que tu peux télécharger sur le site,
Il faut deux fichiers qui sont fournis au membres sur demande (un simple click)
L'install shield est simple et sans surprises.

Ensuite, il suffit de suivre le tutoriel du site.

[DrTopos]

Envoyé par @drien

ça manque un peu d'explications sur le déploiment, dès que j'ai le temps de m'y mettre et de tester des programmes j'écrirais peut-être un petit truc...

Qu'est-ce que tu entends par déploiment ? S'il y a quelque chose à améliorer, merci de donner des précisions (ici ou sur le forum du site du langage).

[DrTopos]

Envoyé par Caine

Il faut deux fichiers qui sont fournis au membres sur demande (un simple click)

Non, c'est fini ce système avec deux fichiers spéciaux. Il suffit de télécharger l'archive. Si c'est sous Windows, il faut simplement exécuter l'archive (qui est un programme d'installation), si c'est sous Linux, il faut détarer l'archive ?.tar.gz dans un répertoire temporaire et exécuter './install' dans ce répertoire.

Par ailleurs, à tous ceux qui sont à la versionn 1.5, je conseille vivement de passer à la version 1.6.

[Caine]

Autant pour moi

Je n'ai pas encore chargé la version 1.6.

Encore tous mes encouragements pour les développeurs de ce langage!

Les dernières évolutions sont une bonne avancée pour un projet que j'ai en tête. Le support d'une base de donnée

[BigTotoro]

Je me permet d'intervenir dans ce fil consacré à Anubis pour signaler la sortie d'Anubis 1.7 sur le site du language http://www.anubis-language.com
Cette version 1.7 apporte une accélération significative de la machine virtuelle de l'ordre de 4 à 10 fois selon les cas.

Il y a maintenant aussi sur ce site, une section d'échange de source Anubis, un peu à la code project.

[Promeneur]

Question naïve, quand on n'est pas mathématicien, ce langage est-il abordable et a-t-il de l'intérêt ?

[gorgonite]

Envoyé par Promeneur

Question naïve, quand on n'est pas mathématicien, ce langage est-il abordable et a-t-il de l'intérêt ?

tu veux dire chercheur en informatique fondamentale... parce que parmi les mathématiciens :
+ maths fondamentales -> ils ne touchent pas à un ordi (peut-être pour du Latex)
+ maths appliquées -> fortran, c++, ou matlab suivant les types

enfin, c'est une opinion personnelle, car de toute façon, plus on fait d'info théorique, et plus on fait de maths en fait



perso, je ne peux pas te répondre, je n'ai pas encore testé ce langage... mais je vais essayer dès que j'aurais fini mon master

[DrTopos]

Envoyé par Promeneur

Question naïve, quand on n'est pas mathématicien, ce langage est-il abordable et a-t-il de l'intérêt ?

Reponse: oui.

Anubis a été conçu selon des principes mathématiques, mais ceux-ci sont essentiellement invisibles pour l'utilisateur, qui se trouve simplement en présence d'un langage fonctionel, pas plus difficile à aborder (même plutôt moins) que CAML ou Haskell. Jusqu'à présent, parmi les personnes que je connais et qui ont utilisé Anubis, aucune (à part moi-même) n'est mathématicien. Voila pour ce qui est d'être abordable.

Pour ce qui est de l'intérêt, je peux simplement dire que diverses choses absolument étrangères aux mathématiques ont été réalisées avec. On trouvera dans la bibliothèque un serveur HTTP/HTTPS, un exemple très simple de programme client/serveur, et diverses autres choses qui démontrent qu'Anubis est un langage généraliste.

Mais ce qui fait le principal intérêt d'Anubis à mon avis, c'est son très haut degré de sûreté. Anubis est un champion de la brièveté du déboggage (pratiquement inexistant). Ce niveau de sûreté, vient bien entendu de la nature mathématique de sa conception.

Anubis revendique un certain nombre de différences avec les autres langages fonctionels. L'une des plus flagrantes est l'absence totale de notion d'exception, mais il y en a d'autres.

Bonne découverte.

P.S. Je signale par ailleurs que l'équipe Anubis a pris la décision de mettre Anubis en open source. Cette décision sera effective après un nettoyage des sources d'ici quelques mois.

[DrTopos]

Envoyé par gorgonite

... parce que parmi les mathématiciens :
+ maths fondamentales -> ils ne touchent pas à un ordi (peut-être pour du Latex)
+ maths appliquées -> fortran, c++, ou matlab suivant les types

Allons, allons, pas de sectarisme.... Bon, ce que tu dis est assez vrai en général (hélas), mais tu vois bien qu'il y a au moins un contre-exemple.

Envoyé par gorgonite

enfin, c'est une opinion personnelle, car de toute façon, plus on fait d'info théorique, et plus on fait de maths en fait

C'est clairement indispensable, puisque les mathématiques ne sont rien d'autre qu'un moyen universel de formaliser, c'est à dire de rendre clair ce qui est obscur.

Envoyé par gorgonite

perso, je ne peux pas te répondre, je n'ai pas encore testé ce langage... mais je vais essayer dès que j'aurais fini mon master

Excellente idée. Bravo ! Et tous mes voeux pour ton master.

[gorgonite]

Envoyé par DrTopos

Allons, allons, pas de sectarisme.... Bon, ce que tu dis est assez vrai en général (hélas), mais tu vois bien qu'il y a au moins un contre-exemple.

je connais de nombreux contre-exemples, mais ils "trainent" de plus en plus du côté de l'info théorique, et non des maths pures ou des maths appliquées

Envoyé par DrTopos

P.S. Je signale par ailleurs que l'équipe Anubis a pris la décision de mettre Anubis en open source. Cette décision sera effective après un nettoyage des sources d'ici quelques mois.

excellent...
on pourra bientôt l'avoir dans les paquetages de sa distribution préférée... il n'y aura plus d'excuses pour ne pas l'installer

Envoyé par DrTopos

Excellente idée. Bravo ! Et tous mes voeux pour ton master.

ce sera fini en septembre

[Promeneur]

Envoyé par DrTopos

Anubis a été conçu selon des principes mathématiques, mais ceux-ci sont essentiellement invisibles pour l'utilisateur, qui se trouve simplement en présence d'un langage fonctionel, pas plus difficile à aborder (même plutôt moins) que CAML ou Haskell. Jusqu'à présent, parmi les personnes que je connais et qui ont utilisé Anubis, aucune (à part moi-même) n'est mathématicien. Voila pour ce qui est d'être abordable.

Pareil pour la version 2, avec, si j'ai bien compris,avec des notions d'énnoncé et de preuve ? Pour le non mathématicien que je suis, cela sonne comme un bon moyen de s'assurer que le résultat esr conforme aux spécifications, mais j'ai peut-être mal compris.






Et une question iconoclaste, une version .Net en préparatioon ?

[gorgonite]

Envoyé par Promeneur

Et une question iconoclaste, une version .Net en préparatioon ?

ça demande pas mal de boulot de porter une vm sur une autre... et ça n'a pas forcémment un grand intérêt, qui se sert de IronPython ou de JPython ?

[Promeneur]

Envoyé par gorgonite

et ça n'a pas forcémment un grand intérêt, qui se sert de IronPython ou de JPython ?

Mais beaucoup de gens se servent de Dot.net . Y apporter de nouveaux outils est toujours intéressant. Il y a des choses pour lesquelle le C# n'est pas forcément le plus adapté, et ajouter des DLL écrites avec d'autres langages peut faire gagner du temps...

Mais je conçois que cela soit trop de boulot à faire .

[Tommy31]

Bon pas lu entierement le thread, donc question peut-etre déjà posée. Mais qu'en est-il de la licence du compilateur et du langage ? C'est de l'open source ?

EDIT
ok, c'est de l'open source
grillé sur le coup

[SpiceGuid]

@DrTopos

Question: j'ai mal compris ou bien la version 2 offrirait un filtrage des types sommes compatible avec l'élimination des coupures (ce qui permettrait la preuve de programme par la correspondance de Curry-Howard) ? Si oui alors ce serait une avancée majeure en matière de qualité logiciel. Mais dans ce cas pourquoi mettre en avant vos topos plutôt que les DDT (Dependant Data Types) mieux connus ? Quelle publication nous permettrait de comparer les deux approches ?

[DrTopos]

Envoyé par SpiceGuid

@DrTopos

Question: j'ai mal compris ou bien la version 2 offrirait un filtrage des types sommes compatible avec l'élimination des coupures (ce qui permettrait la preuve de programme par la correspondance de Curry-Howard) ?

Il ne me semble pas que les types sommes aient jamais été incompatibles avec l'élimination des coupures, laquelle est d'ailleurs plutôt en général remplacée par la normalisation forte à la Tait-Girard. Par ailleurs, la correspondance de Curry-Howard, sur laquelle j'ai eu l'occasion de m'exprimer assez longuement dans un autre fil de ce forum est un mécanisme permettant de transformer les preuves en programmes (ou de voir les preuves comme des programmes) mais ne constitue pas à proprement parler un outil de preuve de programmes.

Envoyé par SpiceGuid

Si oui alors ce serait une avancée majeure en matière de qualité logiciel.

'majeure' je ne sais pas. Ce n'est pas à moi de le dire en tout cas. Mais bien entendu, si je fais tout cela c'est pour améliorer la sûreté en conception logicielle (et pour être tout à fait honnête, c'est surtout le plaisir de mettre en application la théorie des topos qui me motive).

Envoyé par SpiceGuid

Mais dans ce cas pourquoi mettre en avant vos topos plutôt que les DDT (Dependant Data Types) mieux connus ? Quelle publication nous permettrait de comparer les deux approches ?

Les DDT sont les piliers des système à la Martin-Löf, qui sont aussi très liés à Curry-Howard. Ces systèmes ont un énorme défaut sémantique, dont on commence à peine, dans les milieux de logique informatique à s'apercevoir. Il s'agit du fait que dans de tels systèmes, l'injection d'un sous-ensemble dans un ensemble (ou d'un sous-type dans un type) n'est pas toujours prouvablement injective. Ceci en fait des systèmes complètement inédéquats pour la formalisation des mathématiques, et partant de là fort suspects pour la preuve de programmes. J'explique tout cela dans exposé que j'ai fait à l'Université de Marseille-Luminy, fin mai dernier (en présence d'ailleurs de Jean-Yves Girard lui-même, qui est d'accord avec mon analyse), et qu'on peut trouver ici.

Les topos n'empèchent d'ailleurs pas les DDT, comme on peut le voir dans mon exposé (et il y aura des DDT en Anubis 2). On verra également dans cet exposé pourquoi la définition même du classifiant du foncteur des sous-objets (le concept fondamental des topos) peut-être vu comme une version 'sémantique' de la correspondance Curry-Howard.

Quand aux topos eux-même, il s'agit d'une branche de la logique que je considère comme beaucoup plus moderne et pertinente que les théories de types et tout ce qui tourne autour de la correspondance de Curry-Howard et de la théorie des types de Martin-Löf, qui sont, je crois, d'une grande naïveté (avis personnel mais partagé par de nombreux mathématiciens, surtout américains, canadiens et australiens d'ailleurs, les européens étant très en retard dans ce domaine). Bien entendu, aborder cette théorie (celle des topos) est difficile (niveau d'abstraction élevé, réflexes de catégoricien indispensables, etc...), mais je ne connais pas de mathématicien ayant fait l'effort d'apprendre cette théorie, qui ne se soit pas trouvé enthousiasmé par sa puissance conceptuelle et sa pertinence behavioriste. la grande différence est qu'on aborde les problèmes de l'informatique par la sémantique au lieu de les aborder par la seule syntaxe. On évite ainsi de tomber dans des concepts qui s'avère ensuite n'avoir pas grand sens, et de faire (comme le dit J-Y Girard) de ``l'astronomie ptolémaïque''. Pour des références sur la théorie des topos, on peut consulter la bibliographie de mon exposé cité plus haut.

[SpiceGuid]

Effectivement, la lecture de votre exposé à l'Université de Marseille-Luminy est la documentation indispensable pour situer les topos par rapport aux typages Martin-Löf et Hindley-Milner.

J'en fais ici un résumé simplificateur (que je vous invite à corriger) pour ceux que j'imagine nombreux et qui voudraient une comparaison rapide avec Haskell (pour le typage Hindley-Milner) et Epigram (pour le typage Martin-Löf):

• D'un point de vue architectural le système exposé propose une formalisation à deux niveaux, le premier niveau est un lambda-calcul, le second niveau est un calcul des séquents, les deux niveaux sont isomorphes mais seul le premier niveau (les valeurs) est équipé de règles de réduction (la béta-réduction), la réduction du second niveau (les énoncés et les preuves) est à la charge du lecteur et/ou de l'assistant de preuve
• D'un point de vue qualitatif on peut s'attendre à une meilleure lisibilité et une meilleure prouvabilité par rapport à un typage Hindley-Milner qui ne vise qu'à se prémunir des erreurs à l'exécution sans chercher à améliorer la prouvabilité de la post-condition
• L'avantage du système proposé par rapport au typage Martin-Löf c'est le découplage de la charge du calcul d'avec la charge de la preuve, de sorte que l'on peut choisir son système de preuve indépendamment du système de calcul
• L'inconvénient c'est qu'au contraire d'un typage à la Martin-Löf le système de preuve ne pourra pas être utilisé pour guider l'écriture simultanée du calcul et de la preuve, de ce fait lorsque la preuve est obligatoire elle sera plus coûteuse en va-et-vient de réécritures
• Au final on pourrait dire qu'il s'agit d'une version pessimiste du typage Martin-Löf qui se révèlera moins handicapante dans le cas défavorable mais aussi moins payante dans le cas favorable
• Le système n'exclut pas une extension intégrant une réduction sur le calcul des séquents qui le rendrait équivalent au typage Martin-Löf, mais l'auteur doute qu'une telle extension soit réellement bénéficiaire, en particulier il avance des arguments selon lesquels un calcul des séquents complètement isomorphe au lambda-calcul n'est pas un calcul confluent (ne satisfait pas le 1er théorème de Church-Rosser)

Je me permet également de vous citer pour vous aider à mieux situer Anubis dans le monde des langages fonctionnelles modernes:

Il se peut qu'aucune clause de Horn ne 'matche', de même qu'il se peut qu'aucun filtre ne laisse passer une donnée.

Le compilateur OCaml décourage déjà assez fortement le filtrage non exhaustif.

encore que je soupçonne fortement le compilateur Caml d'être capable d'optimiser de telle façon d'aboutir au même saut unique

Exact, on pourrait même dire que le programmeur Anubis fait manuellement le travail d'un compilateur de filtrage, il n'y a aucun gain de performance à espérer des conditionnelles telles qu'Anubis les propose actuellement.

A vrai dire, je considère que la plupart des choses qui sont des 'raccourcis de programmation' ont en général la contre-partie d'obscurcir la sémantique.

Tout à fait d'accord, mais le choix des gardes non-disjointes n'a pas été fait à la légère, il est issu d'années de débats et de retour d'expérience des programmeurs SML et Miranda. Le consensus s'est fait depuis longtemps autour de l'idée que le filtrage déterministe (toutes les gardes sont deux-à-deux disjointes) rend certaines fonctions trop difficiles à écrire ou oblige à dupliquer du code. Le prix à payer pour ce confort est une baisse de lisibilité (il faut lire le filtrage de haut-en-bas, le comble pour un langage qui ne se veut pas séquentiel).

Mais pour moi ce n'est pas du confort, c'est du laxisme et la porte ouverte aux bugs. D'ailleurs, on voit bien que le filtrage tel qu'il existe en Caml ne permet pas d'éliminer la notion d'exception.

Certains programmeurs Caml préfèrent renvoyer un type somme plutôt que de déclencher une exception, il faut alors filtrer le résultat au lieu de capturer l'exception.

[DrTopos]

Une réponse rapide à SpiceGuid. J'en ferai peut-être une plus détaillée demain (la nuit porte conseil).

Je suis très déconcerté par votre résumé de mon exposé. J'avoue ne pas le reconnaître. J'en reparlerai plus tard (quand j'aurai peut-être mieux compris votre point de vue). J'ai toutefois l'impression que vous vous situez à un niveau surtout syntaxique et calculatoire, puisque vous insistez sur la confluence du calcul, sur les performances, etc... Mon soucis (du moins en ce qui concerne cet exposé) était surtout d'avoir un système dans lequel les mathématiques sont celles de tout le monde, et non pas des mathématiques exotiques (le fait qu'une injection canonique ne soit pas injective est tout à fait exotique). En fait, mon exposé porte surtout sur la notion d'égalité entre données, et bien sûr d'égalité entre preuves, une notion de nature clairement sémantique.

En ce qui concerne vos remarques sur Anubis. Je suis d'abord satisfait de constater qu'on est d'accord sur l'essentiel à propos du filtrage et des exceptions. Je fais quand même remarquer qu'une différence essentielle entre Caml et Anubis est que là où Caml décourage fortement, Anubis interdit. Et je crois qu'il ne faut pas sous-estimer cette différence, qui peut être un atout de sureté très important surtout dans un développement en équipe. Je pense souvent plus au point de vue du décideur (le patron) qu'à celui du développeur (qui doit faire ce que le patron lui demande). Maintenant, l'expérience avec Anubis montre aussi qu'un compilateur très peu permissif, même s'il est énervant au début, devient un atout très apprécié par les développeurs car il les déstresse.