Partage

Lisez ici les news de qualité de la v3 du SdZ !

Langages fonctionnels, assistants de preuves et compagnie

21 juillet 2017 à 17:17:34

Bonjour à tous,

Il y a quelques années, la société éditrice du Site du Zéro donnait naissance à un nouveau site, Open Classrooms, fruit d'un long travail de recherche et développement.

De nombreuses fonctionnalités ont fait leur apparition mais beaucoup de membres à l'époque ont déploré la disparition du module de news. Ont également disparu aujourd'hui toutes les archives des news publiées. Une récente demande de consultation de ces archives n'ayant pas donné grand chose, je souhaite partager ici avec vous quelques écrits extraits des abîmes de webarchive.org.

En effet, beaucoup de news publiées sur le SdZ v3 étaient plus des articles de fond que de véritables articles de journalistes d'actualités. Même plusieurs années après leur publication, ces écrits sont encore, à mon avis, tout à fait pertinents et constituent généralement une excellente introduction au sujet qu'ils traitent.

A propos de la licence

Les news étaient publiées sous licence Creative Commons BY-SA. Je signalerai donc toute modification apportée sur le texte original au préalable. Ces news ainsi modifiées (garanties sans aucune modification de fond) sont donc également mises à disposition sous licence Creative Commons BY-SA.

Index des news re-publiées

Assez de bavardages, veuillez trouver ci-dessous le tableau des news re-publiées, classées par ordre chronologique !


Titre Auteur(s) Publiée le
Décès de Robin Milner bluestorm 14/04/2010
Rakudo Star : le langage Perl 6 arrive ! iPoulet 29/07/2010
Les assistants de preuves formelles : zoom sur Coq bluestorm
colbseton
05/04/2011
Ocsigen 2, une bouffée d'air frais pour le web iPoulet 18/10/2011


Important : l'objet du topic est de faire un petit index de quelques news. Si vous voulez poser des questions à propos d'une news en particulier, allez plutôt ouvrir un topic sur un forum approprié ;) Si vous avez souvenir d'une news que vous aimeriez retrouver, signalez-le ici.

-
Edité par unecrevette_ 25 juillet 2017 à 6:44:41

22 juillet 2017 à 17:24:30

News écrite par iPoulet et publiée le 29 juillet 2010, sous licence Creative Commons BY-SA 2.0. Republiée ici avec les modifications suivantes : images supprimées, liens morts effacés.

Rakudo Star : le langage Perl 6 arrive !

C'est un travail de près de dix ans qui aboutit enfin. Le projet Rakudo, conçu pour compiler le langage Perl 6 vers la machine virtuelle Parrot, annonce aujourd'hui sa première version publique, baptisée Rakudo *, ou Rakudo Star. Celle-ci n'est pas encore considérée comme une version stable ni même complète de Perl 6, mais les développeurs de Rakudo espèrent encourager la communauté à tester Perl 6, et à faire remonter des avis sur ce qui fonctionne déjà. Ce compilateur est considéré comme l'implémentation officielle du langage Perl 6, successeur de Perl 5, dont la première version remonte à 1994. De très nombreuses évolutions sont présentées, révélant les modifications importantes qu'ont subi Perl et sa communauté depuis leur création.

La sortie de Rakudo Star est donc une étape majeure dans l'histoire du langage Perl. Par conséquent, cette news est plus longue que ce que l'on peut lire habituellement sur le site : elle détaille d'une part l'histoire de Perl (en retraçant le cheminement qui a conduit à Perl 6), et de l'autre certains des points remarquables de ce nouveau langage. Vous n'êtes pas obligé de tout lire, bien au contraire : à vous de sélectionner ce qui vous intéresse ;) .

L'histoire de Perl 6

Perl est un langage de programmation dynamique de haut niveau, initialement conçu comme un langage de script pour les systèmes de type Unix. En tant que tel, il s'inspire des différents langages habituellement rencontrés sur ces systèmes, à savoir sed, AWK, les langages shells ou le C. Cependant, Perl a connu dans les années 90 un essor très important, et est encore aujourd'hui utilisé pour l'administration système, la programmation réseau et web, la bioinformatique, et, quoique plus rarement, la création d'applications graphiques.

Perl est un langage atypique, possédant une communauté importante mais discrète, une culture très riche et particulière, et des traits de conception assez exceptionnels.

Des débuts jusqu'à l'an 2000

Une grande partie de ces originalités proviennent probablement de la personnalité du créateur de Perl, Larry Wall. En effet, celui-ci n'a pas initialement bénéficié d'une formation d'informaticien, mais de linguiste. Hacker passionné, Wall fréquentait cependant beaucoup d'informaticiens (au quotidien ou via les newsgroups Usenet, qui sont un peu l'ancêtre des forums web), et est par exemple l'auteur du célèbre programme patch.

Ainsi, Wall commence à travailler sur un nouveau langage nommé Pearl dans les années 1987 (renommé Perl depuis car un langage avec ce nom existait en fait déjà). Son but était de proposer un nouvel outil de manipulation de fichiers de texte, à la fois plus simple et complet que sed et AWK. Le newsgroup comp.sources.misc, sur lequel Wall publie les codes source de son travail, reconnaît très vite l'intérêt de Perl. Le langage se développe rapidement, atteignant la version deux en 1988, puis la troisième en 1989.

Durant les années 90, Perl connaît un grand succès, et est le deuxième langage s'étant le plus développé pendant cette décennie (après le langage Java, qui bénéficie du marketing constant de la société SUN Microsystems). Le livre Programming Perl de Larry Wall, publié aux éditions O'Reilly en 1991, se pose comme la référence du langage, et permet sa diffusion. Simultanément, Perl sort en version 4, et celle-ci demeure jusqu'en 1994.

À la fin de l'année, Wall publie Perl 5, qui est une refonte quasi-totale du langage et de l'interpréteur. Perl continue de se développer, et devient, peu de temps après la naissance du web, l'outil de prédilection pour l'écriture de scripts CGI : ces scripts sont la première forme de programmation côté serveur (bien avant PHP, dont la première version a d'ailleurs été écrite en Perl pour simplifier le développement web). Jusqu'en 2000, Perl 5 continue de se développer (Perl 5.6 sort en mars 2000) et supporte petit à petit de nombreuses plate-formes, de Windows à BeOS.

Larry Wall est constamment impliqué dans le développement de Perl, et est d'ailleurs désigné dictateur bénévole à vie par la communauté : par ce titre, les programmeurs utilisant Perl reconnaissent son rôle capital dans le développement du langage, y compris dans les versions futures. Il est intéressant de remarquer que, jusqu'à cette époque, aucune définition formelle du langage n'a été faite : le langage Perl est ce que l'unique interpréteur éponyme, celui auquel Wall contribue, interprète.

Un nouveau langage

Cependant, le développement de Perl connaît au début des années 2000 de grosses difficultés. L'interpréteur est devenu compliqué à maintenir, et encore plus à faire évoluer. Ainsi, à la Conférence des projets Open Source de l'éditeur O'Reilly du mois de juillet 2000, Larry Wall annonce la nécessité de reprendre à nouveau les choses à zéro : c'est la naissance de Perl 6. Mais, selon Wall, Perl 6 doit être un travail communautaire. Il propose ainsi aux développeurs Perl de lui soumettre des RFC, documents dans lesquels ils pourront détailler leurs idées.

Les réponses de la communauté sont nombreuses : de 2000 à 2001, Larry Wall doit étudier au total 361 propositions d'améliorations. Il en tire une série d'articles synthétiques, baptisés les Apocalypses (au premier sens du terme, à savoir des "révélations" faites à la communauté). Cependant, ces articles manquent de clarté, et un autre développeur de la communauté, Damian Conway, se charge de les expliquer dans les Exégèses. Conway écrit également des modules pour Perl 5 permettant d'émuler certains traits de Perl 6, notamment pour appuyer ses explications.

Mais tous ces articles peinent à définir Perl 6, et, en 2004, le langage n'a toujours pas progressé. Une nouvelle série d'articles, plus détaillés, paraissent donc : les Synopses. Ces documents contiennent les spécifications de Perl 6 (c'est à dire les caractéristiques théoriques du langage), et présentent surtout l'intérêt d'être fréquemment mis à jour, au fur et à mesure que les idées au sujet de Perl 6 évoluent.

Une jeune développeuse, Audrey Tang, entreprend alors de développer une implémentation (c'est à dire une version utilisable) de Perl 6, dans le langage de programmation Haskell. Cette version, baptisée Pugs, profite de certaines technologies de Haskell pour se développer rapidement, comme le compilateur GHC et la bibliothèque Parsec. L'implémentation de Tang permet ainsi de finir d'écrire les spécifications de Perl 6 et de commencer à utiliser ce langage. Il est également certain que la conception de Perl 6 a été influencée par Haskell lors de cette phase d'expérimentations, et que, sans Pugs, Perl 6 serait aujourd'hui beaucoup moins avancé.

Parrot et Rakudo

Pendant que Perl 6 prenait forme, la question de l'implémentation officielle du langage était également à l'étude. Dès 2001, des développeurs ont étudié la capacité de la JVM à accueillir une implémentation de Perl 6. Mais cette machine virtuelle se révèle, encore aujourd'hui, être très peu adaptée aux langages dynamiques comme Perl. Il a donc été décidé de développer Parrot, une nouvelle machine virtuelle adaptée aux besoins de Perl 6. Cependant, les développeurs de Parrot, menés par la linguiste et développeuse Allison Randal (autre membre éminent de la communauté Perl), ont été plus ambitieux, et ont conçu une machine virtuelle indépendante de Perl, ainsi qu'un ensemble d'outils facilitant la création de nouveaux compilateurs pour tous les langages. Il est donc possible de développer de nouveaux langages pour Parrot qui seront compatibles avec tous les programmes Perl.

À condition bien sûr qu'un compilateur pour Perl existe ! Et c'est ce rôle que remplit Rakudo (« la voie du chameau » en japonais, le chameau étant l'animal emblématique de Perl). Il utilise au mieux les technologies proposées par Parrot, telles que le Parser Grammar Engine (PGE). Ce dernier permet de définir simplement la syntaxe d'un langage (ce qui, dans le cas de Perl, n'est cependant pas une mince affaire !), et est en fait une implémentation directe dans Parrot des grammaires de Perl 6. De plus, Rakudo est écrit dans le langage NQP, lui aussi proposé par Parrot.

Le développement de Rakudo a été séparé de celui de Parrot en février 2009, et a connu depuis un rythme de développement régulier, proposant une nouvelle version tous les mois. Bien qu'il ne soit pas la première implémentation utilisable de Perl 6, Rakudo a été la plus active ces dernières années.

Les modules de CPAN

Conçu en 1995, le CPAN est une des plus grandes forces de Perl 5 : c'est un ensemble de modules accessibles sur Internet, comprenant aussi bien des bibliothèques pour accéder à des bases de données ou à une interface graphique que des extensions du langage. Il compte actuellement plus de 20 000 modules, qui peuvent être téléchargés et installés automatiquement. Les modules du CPAN devraient être compatibles avec Perl 6 sans demander trop de modifications.

Cependant, certains modules pourraient être écrits spécifiquement pour Perl 6 et Parrot (ce qui permettrait de les utiliser depuis n'importe quel langage supporté par la machine virtuelle), d'où la nécessité d'un nouveau réseau : CPAN 6. Celui-ci est encore en développement à l'heure actuelle. Un dépôt de modules est cependant déjà disponible, ainsi que Proto, un système de gestion des dépendances léger pour installer des modules Perl 6.

Les nouveautés de Perl 6

Perl a toujours été un langage regorgeant de fonctionnalités parfois très pointues, qui permettent aux programmeurs compétents d'écrire des codes beaucoup plus concis que ce qu'ils écriraient dans les langages de plus bas niveau. Mais Perl ne s'utilise comme aucun autre langage : ses particularités sont plus ou moins bien comprises par les débutants ou les développeurs issus d'autres milieux, ce qui contribue à lui donner la réputation d'un langage obscur au comportement bizarre.

Perl 6 introduit donc quelques différences avec Perl 5 qui proviennent d'autres langages, et visent à le rendre un peu plus compréhensible, et un peu plus rigoureux. De plus, un certain nombre de nouvelles fonctionnalités ont été imaginées pendant le développement de Pugs, et proviennent donc du langage fonctionnel Haskell (mais sous une forme adaptée à Perl).

Les sigils et les contextes

Le terme de « sigil » désigne les caractères non-alphabétiques qui précèdent le nom des variables en Perl. Par exemple, les variables « scalaires » (nombres et chaînes) sont précédées d'un dollar, et les tableaux d'un arobase. Ceci trouve son origine dans le passé de linguiste de Larry Wall : pour un être humain, il est naturel de dire

Cette pomme 
Ces pommes
Cette troisième pomme

Les sigils ont donc été inventés pour respecter une forme de séparation entre singulier et pluriel. Ainsi, en Perl 5 on écrivait $apple pour désigner une variable scalaire, @apples pour un tableaux de pommes, et $apples[2] pour désigner la troisième pomme. Le dollar montrait qu'on ne désignait qu'un seul élément, donc servait de singulier.

Le but de cette approche (à distinguer de celle d'AppleScript) était de permettre d'écrire un code assez naturel pour le programmeur : écrire du Perl devait être aussi simple que de parler. Cependant, les concepteurs de Perl ont par la suite remarqué que certaines utilisations des tableaux ou d'autres structures de données devenaient beaucoup trop complexes pour correspondre à la parole humaine. En d'autres termes, ce mécanisme rendait très simple l'écriture de morceaux de code simples, mais devenait trop compliqué pour des utilisations moins basiques.

Il a donc été décidé, en Perl 6, d'associer une fois pour toute un sigil et sa variable (on écrit donc @apples[2]). Mais un autre trait caractéristique de Perl intervient alors pour déterminer la nature de ce qui est renvoyé : le contexte. De même qu'en anglais ou en français une expression peut avoir un sens différent selon ce qui l'entoure, les expressions Perl sont évaluées dans un certain contexte qui peut faire varier leur résultat. Ainsi, on distingue entre autres le contexte scalaire et le contexte des tableaux :

@tableau = ('a', 'b', 'c'); 
$element = @tableau[1]; # Ici $element vaut 'b' 
@extrait = @tableau[1]; # Ici @extrait vaut ('b'), un tableau de 1 élément 

Suivant ce qui se trouve à gauche du symbole = (un scalaire ou un tableau), Perl 6 va comprendre que vous attendez de récupérer un élément scalaire du tableau ou un extrait du tableau (un autre tableau ne contenant qu'une partie des éléments initiaux). Naturellement, les contextes permettent de faire bien d'autres choses, et nous les reverrons dans la suite.

Des objets partout

Les principaux concurrents de Perl se sont tous progressivement dotés d'un système de programmation orientée objet, avec plus ou moins de réussite. Bien que Perl permettait déjà d'utiliser des objets dans sa version 5, ainsi que d'importer des modules proposant un nouveau système (comme Moose), les valeurs de base du langage n'en profitaient pas.

Perl 6 apporte donc des méthodes à toutes les valeurs. Par exemple, les tableaux ont une méthode elem qui renvoie le nombre d'éléments qu'ils contiennent, une méthode end qui renvoie le plus grand indice du tableau (pour en désigner la fin), une méthode pick pour prendre un ou plusieurs éléments au hasard… Pour la plupart des objets, les anciennes fonctions (appelées sous-routines en Perl) restent disponibles, mais ont également été ajoutées aux objets qu'elles concernaient. Par exemple, pour trier un tableau, on utilisera indifféremment @tableau.sort ou sort @tableau.

À ce propos, on utilise désormais le point, et non plus la flèche, pour appeler une méthode ou désigner un attribut.

Typage statique ou dynamique

Perl 6 rompt avec les versions précédentes de Perl en proposant un panel assez vaste de fonctionnalités destinées à vérifier les types d'un programme. Comme avant, les variables peuvent être dynamiquement typées, ce qui veut dire que leur type n'est connu qu'à l'exécution. Mais il est également possible de préciser des types pour ces variables, ce qui permet aussi bien de détecter des erreurs à la compilation que d'effectuer des optimisations, quand c'est possible.

En tout cas, une contrainte de type non-respectée à l'exécution provoquera une erreur. Il est par exemple interdit de faire

my Int $x = 3; # Déclaration de $x comme entier 
$x = "foo"; 

Les types « normaux » (ne jouant pas de rôle particulier) héritent du type Any, qui lui-même hérite du type Mu (parent de tout autre type). Des types génériques sont possibles, par exemple my Int @a = 1, 2, 3; déclare le tableau @a comme étant de type Array of Int. On peut connaître le type d'une variable à l'aide de sa méthode WHAT, et tester la capacité d'une variable à être convertie en un autre type à l'aide de l'opérateur ~~ :

$x ~~ Int {
    say 'Variable $x contains an integer';
}

Il est possible de définir des contraintes plus fortes sur des sous-ensembles de certains types, par exemple un ensemble de nombres pairs :

subset Pairs of Int where -> $n { $n % 2 == 0 } 
my Pairs $n = 2; 
say $n++; # Erreur : $n va recevoir 3, qui ne vérifie pas la contrainte 

Les Synopses de Perl 6 autorisent un compilateur à remarquer aussi tôt que possible des éventuelles erreurs de types (avant l'exécution de l'instruction fautive). Cependant, l'exemple suivant montre que certaines contraintes de types seront de toute façon dynamiques :

my enum Day ['Sun','Mon','Tue','Wed','Thu','Fri','Sat']; 
subset Weekday of Day where 'Mon' .. 'Fri'; # contrainte statique 
subset Today of Day where *.today; # contrainte dynamique 

La synopsis 12 traite plus en détail des questions de dynamisme.

Structures de contrôle et blocs

Les structures de contrôle de Perl 6 ressemblent à celles de Perl 5, mais suivent la tendance de plusieurs langages (Python, Go) à se débarrasser des parenthèses autrefois nécessaires. Par exemple, il est possible d'écrire if $nombre < 42 { ... } . Comme en Perl 5, les modificateurs placés après des instructions sont toujours autorisés : say "Perdu !" if $answer != 42;.

La boucle for ne sert désormais qu'à parcourir des listes (comme foreach autrefois) ; la version de for du langage C s'appelle désormais loop. Pour parcourir une liste, for attend un bloc contenant les instructions à exécuter sur chaque élément. Par exemple pour afficher les entiers de 1 à 10,

for 1..10 -> $x { 
    say $x;
}

ou pour lire les lignes d'un fichier "text.txt"

for lines "text.txt" -> $line {
    say $line.chars;
}

Les blocs correspondent à des morceaux de code pouvant prendre des arguments et être manipulés, comme les fonctions anonymes que l'on trouve dans d'autres langages. Ils peuvent prendre un nombre variable d'arguments : dans ce cas, le comportement de la boucle for est modifié. Par exemple,

my @tableau = <Pierre 14 Marc 12 Laure 13>

for @tableau -> $nom, $age { 
    say "$nom a $age ans." 
}

La synopsis 4traite des structures de contrôle et des blocs.

Sous-routines (ou fonctions)

La définition de fonctions a été grandement revue dans Perl 6. Il est possible de préciser une liste formelle d'arguments, éventuellement accompagnés de types, de valeurs par défaut, ou d'indications sur leur mutabilité. Par exemple,

sub ma_sub (Int $a is rw, $b = 3 is copy) { ... } 

définit une sous-routine ma_sub prenant un paramètre $a pouvant être modifié (il est passé en mode read-write, soit lecture et écriture) et un paramètre $b dont on est sûr qu'il ne sera pas modifié puisqu'il est copié (cependant la copie peut être modifiée à l'intérieur de la sous-routine). De plus, $b est optionnel, sa valeur par défaut est 3.

Les arguments peuvent être nommés, en les préfixant par « : » dans la liste des arguments. Lors de l'appel de la fonction, on écrit alors argument => valeur. Certaines fonctions utilisent ces arguments nommés comme des options : par exemple, la méthode pick des tableaux permet de choisir un élément au hasard dans le tableau, qui sera enlevé. Mais l'argument optionnel nommé replace permet de préciser à pick qu'on souhaite replacer l'élément pioché dans le tableau. On écrit alors @tableau.pick(4, replace => True), ou, plus simplement, @tableau.pick(4, :replace) ce qui est équivalent (mais plus court). Par exemple, on peut simuler le lancement de 4 dés en écrivant (1..6).pick(4, :replace).

L'ancien tableau d'arguments @_ de Perl 5 reste cependant accessible si aucune liste formelle d'arguments n'est spécifiée. ~~Consultez la synopsis 6 sur les sous-routines pour plus d'informations.~~

Un nouveau système d'objets

La programmation objet en Perl a été entièrement repensée. Un certain nombre de nouveaux mot-clefs ont été introduits, permettant de définir des classes de la même manière que dans la plupart des langages de programmation : ici, une classe Rectangle qui hérite d'une classe Shape, avec deux attributs mutables et une méthode.

class Rectangle is Shape {
    has $.width is rw;
    has $.height is rw;

    method area {
        $!width * $!height;
    }
}

Les twigils (sur lesquels nous reviendrons) permettent, comme les sigils en Ruby, de préciser l'accessibilité d'un attribut : on notera $.attribut pour un attribut public, et $!attribut s'il est privé.

Perl 6 offre un autre mécanisme de programmation orientée objet qui ressemble aux classes, mais sans l'idée de hiérarchisation des classes : les rôles. Ils s'utilisent avec le mot-clef does. Par exemple, une classe Chien héritera probablement d'une classe Mammifère, de même qu'une classe Loup. Mais on pourra également définir un rôle AnimalDomestique supporté par tous les chiens, et éventuellement quelques oiseaux, mais pas par les loups - il est clair que ce rôle ne rentre alors pas dans la hiérarchie précédente. De plus, Perl 6 permet de faire jouer un rôle à un objet particulier plutôt qu'à toute sa classe (on pourrait donc avoir des loups domestiques).

Les rôles sont donc un moyen de décrire ce que les objets font, et pas ce qu'ils sont. Par exemple, des objets peuvent supporter les rôles Callable ou Positional pour jouer respectivement le rôle de blocs (pouvant être appelés, i.e. exécutés) ou de tableaux (on pourra alors leur adjoindre le sigil @). Cette fonctionnalité est donc à opposer à des approches comme celle des interfaces ou des ABC, où rôles et héritage sont liés. Elle est également présentée comme plus fiable que le duck typing.

La synopsis 14 traite de la façon dont Perl 6 utilisera les rôles.

Les règles, les regexps et l'analyse syntaxiques

Perl est connu pour ses expressions rationnelles (les « regexps »), qui sont en réalité beaucoup plus puissantes que le modèle théorique dont elles sont inspirées. Perl 6 généralise encore cet outil, afin de le rendre plus adapté pour l'analyse syntaxique (rappelons que Perl doit être utilisé par Parrot pour écrire des compilateurs).

Il est donc possible de décrire des grammaires complètes de façon beaucoup plus lisibles qu'avec de simples regexps. Voici un exemple servant à analyser des URL, pour récupérer par exemple leur nom d'hôte :

grammar URL {
    token TOP {
        <schema> '://' 
        [<hostname> | <ip> ]
        [ ':' <port>]?
        '/' <path>?
    }
    token byte {
        (\d**{1..3}) <?{ $0 < 256 }>
    }
    token ip {
        <byte> [\. <byte> ] ** 3
    }
    token schema {
         \w+
    }
    token hostname {
        (\w+) ( \. \w+ )*
    }
    token port {
        \d+
    }
    token path {
        <[ a..z A..Z 0..9 -_.!~*'():@&=+$,/ ]>+
    }
}

Outre une plus grande lisibilité, les grammaires peuvent être composées. Par exemple, pour se limiter aux URL du protocole HTTP, on peut dériver la grammaire précédente en

grammar URL::HTTP is URL {
    token schema { 'http' }
}

Cependant, il est toujours possible d'utiliser des regexps avec une syntaxe proche de celle de Perl 5, pour faire des substitutions ou des recherches dans une chaîne de caractères :

my $x = 'Abcd';
$x ~~ s:ii/^../foo/; # substitution qui conserve la casse
say $x; # affiche Foocd

Les jonctions

Perl 6 introduit un nouveau type d'objets représentant des calculs effectués de façon parallèle, les jonctions. Par exemple, on exprime l'objet « 1 ou 2 » par 1|2. Il devient alors possible d'écrire if $a == 1|2 . De plus, ces objets supportent les opérations usuelles, qui sont alors distribuées sur tous leurs éléments : (1|2) + 1 == (2|3).

Trois opérateurs servent pour les jonctions : |, & et ^, qui désignent respectivement la disjonction, la conjonction, et l'unicité. Ils correspondent en fait à trois fonctions prédéfinies, any, all et one. Une fonction none est également définie, qui fait le contraire de all. Le but initial était de rester proche (une fois de plus) du langage naturel : on dit souvent « si x est égal à ceci ou cela ». Cependant, il est clair que les jonctions peuvent trouver d'autres applications : il n'est pas exclu de les utiliser pour le calcul parallèle, et il est de plus possible d'écrire, si @items est un tableau d'entiers,

if all(@items) >= 0 {    # Ou none(@items) < 0
    say "Tous positifs !"
}

La paresse

Une des caractéristiques de Perl 6 empruntées à Haskell lors du développement de Pugs est certainement l'évaluation paresseuse : en Haskell, tous les calculs d'un programme sont laissés en suspend, jusqu'au moment où ils sont vraiment nécessaires. Cela permet par exemple de travailler avec des listes infinies : tant qu'on n'essaye pas, par exemple, d'en mesurer la longueur, seul un nombre fini de valeurs est calculé.

En Perl, on se retrouve très vite confronté à l'évaluation paresseuse des listes quand on veut par exemple afficher les lignes d'un fichier en les numérotant : d'après ce qui précède, on serait tenté d'utiliser une boucle for et un bloc pointé, mais jusqu'à combien faudrait-il compter ? Impossible de prévoir. On écrit donc que l'on compte jusqu'à l'infini, en réalité seules les valeurs utiles seront calculées :

my $file = open '/etc/passwd', :r;
for $file.lines Z 1..Inf -> $text, $n {
    say "$n : $line";
}

L'opérateur Z sert à fusionner deux listes en une seule. C'est un raccourci pour « zip » (une fonction qui existe également en Haskell, en OCaml ou en Python), qui regroupe deux listes en une seule - comme une fermeture éclair.

Il est également possible de construire une liste paresseuse à l'aide des mot-clefs gather et take, proches du concept de générateurs en Python. Le premier sert à délimiter un bloc qui sera exécuté à chaque fois que l'on aura besoin d'une nouvelle valeur pour la liste. Le second sert précisément à générer ces valeurs. Il est alors possible d'affecter le résultat à une liste, ce qui construira paresseusement la liste (il faut toutefois utiliser := plutôt que =, ce dernier évaluant toute la liste).

~~La synopsis 9 traite des structures de données de Perl 6.~~

Les multiples opérateurs de Perl 6

Perl est célèbre pour son impressionnante quantité d'opérateurs. Avec Perl 6, c'est pire, à tel point qu'une classification périodique des opérateurs a été établie :D . Jouant un rôle comparable à celui des fonctions d'ordre supérieur, les meta-opérateurs de Perl 6 permettent de réutiliser d'autres opérateurs en les appliquant sur des ensembles de données.

Par exemple, l'opérateur de réduction (noté [ ]) applique successivement une opération à toute une liste. Cela peut par exemple servir à additionner tous les éléments d'une liste : il suffit d'écrire [+] (1, 6, 3, 2) pour calculer 1 + 6 + 3 + 2. De même, il est parfaitement naturel d'écrire if [<=] @tableau pour vérifier que tous les éléments de @tableau sont rangés dans l'ordre croissant. Il est également possible de générer tous les résultats intermédiaires dans une liste, en notant [\ ] plutôt que [ ] : [\*] 1..10 générera la liste des factorielles de 1 à 10.

Plusieurs opérateurs servent à combiner les listes entre elles. C'est le cas de Z, qui « zippe » deux listes (éventuellement à l'aide d'un autre opérateur, par exemple (1, 2) Z+ (3, 4) donne (4, 6)), de X, qui distribue une liste sur l'autre, ou encore des hyper-opérateurs « et » (qui peuvent également être écrits << et >>). Ceux-ci servent à distribuer une opération sur tous les éléments d'une liste - ou, en réalité, d'une structure de données jouant le rôle d'un Iterator. Par exemple, -<< (1,2,3) produit la liste (-1, -2, -3). De plus, (1,1,2,3,5) »+« (1,2,3,5,8) produit (2,3,5,8,13), les éléments étant combinés. Les hyper-opérateurs suivent en réalité des règles complexes, qui semblent pour l'instant être mal supportées par Rakudo.

Enfin, il est possible de définir ses propres opérateurs. Par exemple, on peut définir la factorielle par

sub postfix:<!>($arg) {
    if ($arg == 0) {
        1;
    }
    else { 
        ($arg-1)! * $arg;     # Définition récursive !
    }
}

ou, avec ce qui précède, sub postfix:<!>($arg) { [*] 1..$arg } . Il est possible de gérer finement l'ordre de priorité de chaque opérateur, par rapport à d'autres opérateurs (grâce à des mot-clefs comme is tighter, equiv ou looser), ainsi que de préciser quel type d'opérateur on définit (infixe, postfixe, préfixe, ainsi que circumfix (autour des données) et postcircumfix (comme les crochets d'un dictionnaire)).

Les twigils : des indications de portée

Ruby, en héritant de Perl, a changé quelques caractéristiques, en changeant par exemple le rôle des sigils. Alors qu'en Perl 5 ils indiquent la nature d'une variable, en Ruby ils indiquent sa portée : est-ce une variable globale, locale, l'attribut d'un objet… Perl 6 reprend cette idée, mais sans pour autant supprimer l'idée première des sigils. La solution ? Ajouter un deuxième sigil, placé après le premier - ce que l'on appelle un twigil.

Par exemple, $*foo dénote une variable globale ; $.foo et $!foo, respectivement des attributs publics et privés d'une classe ; $^foo est un paramètre auto-déclaré dans un bloc. Concernant ce dernier, Perl 6 corrige en effet une inélégance de Perl 5, qui consistait à réserver, dans les blocs, certains noms de variables pour leur faire jouer des rôles spéciaux. Ainsi on écrivait sort { $a <=> $b } @array pour trier un tableau. En Perl 6, le twigil ^ permet de déclarer ce genre de paramètre sans rôle spécial : il est équivalent d'écrire sort { $^a <=> $^b } @array .

Quand le bloc prend plusieurs arguments, ceux-ci sont affectés aux paramètres auto-déclarés… par ordre alphabétique. Par exemple :

my @tableau = <Pierre 14 Marc 12 Laure 13>

for @tableau {   # Rappelez-vous, ici on utilisait -> $x, $y
    say "$^alpha a $^bravo ans." 
}

Enfin, les variables traitées à la compilation telles que __LINE__ ou __FILE__ sont remplacées par $?LINE et $?FILE - avec le twigil ?.

L'astérisque * et les blocs

Les programmeurs Perl chevronnés considèrent comme un sport l'écriture de codes les plus courts possible, qui font appel aux nombreux outils du langage. Afin de donner de l'expressivité aux développeurs, Perl 6 définit un objet particulier, *, qui est en fait le seul objet de type Whatever. C'est une valeur spéciale que les développeurs peuvent utiliser comme raccourci pour dire « autant que nécessaire », ou « quoi que ce soit ». Par exemple, @cartes.pick(*) mélange le tableau cartes, car .pick prélève les cartes une par une au hasard jusqu'à ce que le tableau soit vide, et renvoie le tout. De même, on peut par exemple compter jusqu'à l'infini en écrivant 1 ... *, ou générer la liste des puissances de deux avec 1, 2, 4 ... *. Dans un switch, * joue également le rôle de joker.

Mais l'astérisque peut également servir à construire des blocs de code, qui, vous l'aurez compris, jouent un rôle clef dans les programmes Perl 6. Ainsi, écrire par exemple * + * génère le bloc $x, $y -> {$x + $y}. Cela donne donc une grande expressivité à Perl 6 : par exemple, si on sait que la méthode .chop supprime le dernier caractère d'une chaîne, on ne s'étonnera pas que 'Camelia', *.chop ... ''; génère la liste de tous les préfixes du mot « Camelia ». De même, si une classe Etudiants est définie par

class Etudiant {
    has Str $.nom;
    has Int $.annee is rw;
}

on appréciera de pouvoir écrire @students.sort: *.nom; pour trier les étudiants par nom.

Rakudo Star

C'est donc aujourd'hui que la première version publique du compilateur Rakudo est publiée, sous le nom de « Rakudo * ». Selon Patrick Michaud, chef du projet, c'est un clin d'œil à l'objet * de Perl 6 : Rakudo n'est pas encore tout à fait mature, mais il a assez traîné, et ses développeurs le publient « quoi qu'il en soit ». Michaud déplore la lenteur et les quelques bugs qui peuvent encore être rencontrés, mais le développement de Rakudo est actif, et la diffusion de Perl 6 ne pourra qu'attirer des programmeurs et multiplier les rapports de bug.

De plus, Rakudo respecte déjà une très grande partie des spécifications de Perl 6, dont celles qui ont été présentées dans la partie précédente. Rakudo Star est en réalité une distribution contenant la version #31 de Rakudo, ainsi que la machine virtuelle Parrot nécessaire pour exécuter du code.

Un certain nombre de modules sont également livrés, qui permettent par exemple de faire tourner un petit serveur web, d'appeler des bibliothèques C ou Perl 5, ou d'interagir avec des bases de données. Ce sont essentiellement des modules de test, qui pourraient être remplacés par des modules plus standards à l'avenir.

Rakudo Star peut être téléchargé depuis github. Si vous utilisez une distribution GNU/Linux, il est probable que des paquets soient disponibles. Si vous ne souhaitez pas installer Rakudo pour tester Perl 6, il est également possible d'aller parler en privé au robot p6eval sur le réseau irc.freenode.net, en préfixant votre commande par rakudo: pour préciser l'interpréteur. Par exemple :

[23:07] poulet: rakudo: say ([\*] 1..10).perl
[23:07] p6eval: rakudo fe29cd: OUTPUT«(1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800)»

Liens complémentaires

-
Edité par unecrevette_ 23 juillet 2017 à 4:54:37

Staff 22 juillet 2017 à 17:50:51

Bonjour.

"Il y a quelques années, la société éditrice du Site du Zéro donnait naissance à un nouveau site, Open Classrooms (aussi qualifié de SdZ v4)"

Mais... Non ? SDZ v4 était bel et bien SDZ, était sorti avant le passage à OC.

Petit aperçu de la V4.

22 juillet 2017 à 18:07:03

Mes plus plates excuses, je n'ai pas suivi en détail la mort du SdZ. En tous cas merci, c'est corrigé !
22 juillet 2017 à 23:41:18

Je me permets d'ajouter un lien vers ce sujet sur ZesteDeSavoir, où d'autres se sont posés les mêmes question de récupération des anciennes news intéressantes (et ont émis en 2ème page une liste de news récupérables).

-
Edité par entwanne 22 juillet 2017 à 23:43:17

23 juillet 2017 à 5:46:17

News écrite par bluestorm et publiée le 14 avril 2010, sous licence Creative Commons BY-SA 2.0. Republiée ici avec les modifications suivantes : images supprimées, liens morts effacés.

Décès de Robin Milner

L’informatique théorique est une science jeune : bien que certaines de ses idées (dont l’algorithme d'Euclide) remontent à plusieurs millénaires, la plupart de ses grands noms sont encore en vie, et même souvent encore en activité aujourd’hui. La mort de Robin Milner, le 20 mars dernier, à l’âge de 76 ans, nous rappelle que c’est une chance rare, mais aussi une époque qui touche à sa fin.

Né dans une famille de la classe moyenne anglaise, ses résultats scolaires ont permis au jeune Robin Milner d’accéder à une éducation privilégiée, en gagnant des bourses pour l’Eton college en 1946 puis pour l’université de Cambridge en 1952. Il y développa une passion pour les mathématiques et la musique (il jouait du hautbois).

Après avoir envisagé de devenir musicien professionnel, il devint professeur de mathématiques en 1957, puis programmeur chez Ferranti (une firme anglaise qui a développé certains des tous premiers ordinateurs). En 1968, il partit aux États-Unis pour faire de la recherche dans deux domaines balbutiants : l’intelligence artificielle et la preuve assistée par ordinateur. C’est là qu’il développa la première version du système LCF (en), un logiciel que je décrirai rapidement dans la deuxième partie de cette news.

En 1973, Milner rentra au Royaume-Uni avec sa femme, professeur de violon, pour travailler à l’université d’Édimbourg. Il continua le développement du système LCF, pour lequel il développa un nouveau langage de programmation, ML, qui influence toujours de nombreux aspects des langages de programmation modernes.

À partir des années 80, Milner consacre la majorité de son temps de recherche à un sujet qui l’a toujours intéressé, la concurrence : comment modéliser une interaction entre plusieurs systèmes qui fonctionnent simultanément et qui communiquent entre eux ? Il développa le système CCS (en) (Calculus for Communicating Systems), puis le Pi-calcul, langage aujourd’hui à la base des études théoriques des systèmes concurrents.

En 1991, Milner gagna le Turing Award, une des plus prestigieuses récompenses en informatique. Il continua à faire de la recherche jusqu’à sa mort : il passa un an à travailler en France en 2007, et publia en 2009 un livre sur les bigraphes, ses travaux les plus récents dans le domaine de la concurrence.

Robin Milner a marqué les esprits par son insistance sur l’élégance et la rigueur mathématique, les liens entre les aspects théoriques et pratiques des langages de programmation, ses qualités d’administrateur, d’enseignant et de chercheur. Il a toujours fondé sa recherche sur des problèmes pratiques auxquels il apportait des solutions puissantes et flexibles, grâce à l’élégance et au minimalisme des concepts mathématiques de la théorie.

Sources :

LCF

Milner s’était initialement intéressé aux bases de données : comment répondre automatiquement à une requête de l’utilisateur ? Il a ensuite travaillé sur des prouveurs automatiques, qui répondent à d’autres formes de requête : cet énoncé mathématique est-il valide ? Par exemple on lui demande : "Est-ce bien vrai que pour tout nombre entier p, le nombre p + p est pair ?", et il répond : Oui.

C’est un domaine très intéressant, qui est encore un sujet de recherche aujourd’hui, mais qui est toujours fortement limité : trouver des preuves d’énoncés mathématiques intéressants est une activité très difficile, que les ordinateurs ont beaucoup de mal à effectuer automatiquement. L’étape suivante, si l’on veut faire des mathématiques avec un ordinateur, est de passer à un modèle hybride où l’humain peut aider la machine : c’est le principe des assistants de preuve. L’humain donne des indications à l’ordinateur sur la façon dont il faut faire la démonstration mathématique, et le programme se charge de vérifier qu’il n’y a pas d’erreur, que toutes les étapes du raisonnement sont valides.

C’est ce que faisait LCF, un des premiers logiciels de ce genre. Les preuves sont décrites au logiciel sous des formes très strictes, pour qu’il puisse les comprendre. Dans la première version LCF, seul un petit nombre de règles de déduction (« pour prouver ça, il suffit de prouver ceci et cela ») étaient disponibles, mais le système a rapidement été rendu extensible, grâce un langage de programmation dédié que je présenterai dans la section suivante.

Ces outils ne sont pas utiles qu’en mathématiques, mais peuvent aussi servir dans tous les domaines scientifiques, donc en particulier en informatique. À l’époque (début des années 1970), l’informatique théorique avait été mise en ébullition par les travaux de Dana Scott, qui ont permis d’étudier mathématiquement la signification (sémantique) des programmes informatiques. Milner a ainsi utilisé LCF pour vérifier un petit compilateur : si on sait exprimer mathématiquement le sens d’un langage de programmation, et aussi le sens du langage assembleur, on peut prouver qu’un compilateur est correct, c’est-à-dire que le programme assembleur qu’il produit est équivalent au programme dans le langage qu’on lui a donné. C’était à l’époque un essai sur un langage très simple, mais de nos jours on fait des preuves beaucoup plus ambitieuses, comme la vérification complète d’un compilateur du langage C.

Source : From LCF to HOL : a short history (en), par Mike Gordon, un des collaborateurs de Milner.

ML

Avoir un logiciel qui aide à faire des démonstrations, c’est très bien. Mais quand il tombe entre les mains d’une équipe d’informaticiens… ils ont vite envie de programmer ! On peut avoir envie, par exemple, d’écrire des programmes qui font automatiquement certaines parties de la preuve qui sont plus faciles. Cependant, si on laisse les utilisateurs étendre le logiciel avec des scripts, il se pose assez vite une question délicate : si le script utilisé est buggué, est-ce qu’on risque d’obtenir des preuves fausses ?

Il y a plusieurs façons d’éviter ce problème, mais la méthode utilisée par LCF fut totalement novatrice : utiliser le typage du langage de programmation des scripts pour empêcher les preuves erronées. On représente les théorèmes par un type abstrait de données (en), dont les seules opérations disponibles correspondent à un petit ensemble de règles de raisonnement valides. Toute manipulation incorrecte est rejetée comme une erreur de typage par le compilateur. Ainsi, un utilisateur peut écrire un script qui manipule les démonstrations comme il le souhaite, il est sûr qu’il n’introduira jamais d’erreur de raisonnement sans en être averti.

Pour pouvoir faire cela (donc répondre à un problème très concret), Milner a conçu un langage de programmation entièrement nouveau, nommé ML. Cela signifie « Méta-langage », un langage de programmation qui manipule le langage des preuves. Milner et les gens qui travaillaient avec lui se sont peu à peu rendu compte qu’il pouvait en fait servir de langage de programmation généraliste, qu’on pourrait utiliser dans beaucoup d’autres contextes. Ce fut le début des langages de programmation « de la famille ML », comme OCaml, Standard ML (en), et aussi Haskell, qui ont repris le système de typage novateur.

Source : A theory of type polymorphism in programming (en), l’article original de Milner sur le système de typage du langage ML.

Fonctionnalités novatrices du typage ML

Le premier atout du système de typage de ML est le polymorphisme paramétrique. C’est une façon d’exprimer la généricité d’une fonction dans son type : il indique qu’elle peut en fait s’utiliser avec de nombreux types différents, de la même manière à chaque fois. Pour cela, on écrit des « variables de type » ('a, 'b, …), que l’on peut remplacer ensuite par n’importe quel type. Par exemple, la fonction qui renvoie la taille d’une liste est de type 'a list -> int, donc on peut l’utiliser sur des listes d’entiers (int list), de chaînes de caractères (string list), de fonctions entières ((int -> int) list)… La fonction qui prend une liste et renverse l’ordre des éléments est de type 'a list -> 'a list : elle prend une liste de n’importe quel type, et renvoie une liste du même type.

Cette idée était déjà connue des mathématiciens (logiciens), mais n’avait encore jamais été mise en pratique dans un langage de programmation. De nos jours, elle est la base de plusieurs d’entre eux, ainsi que des generics de C# ou Java.

La seconde caractéristique du typage ML est l’inférence de types : en ML, il n’est jamais nécessaire de préciser le type d’une variable, le compilateur le devine tout seul. On reproche souvent aux langages statiquement typés leur verbosité, liée en particulier à la déclaration du type de chaque variable. ML allie la rigueur et la sûreté des langages statiques, avec une certaine légèreté des langages dynamiques. De plus, comme tout ce qui a été conçu par Milner, la rigueur est au rendez-vous : il n’y a jamais de bricolage et le type deviné est toujours le type le plus général possible. Cette inférence est restée longtemps un trésor réservé à des langages fonctionnels peu connus, mais commence enfin à apparaître dans les langages de programmations « grand public » , avec par exemple Scala et C#.

Concurrence et Pi-calcul

Un autre domaine qui a toujours intéressé Milner est la question des interactions entre différents systèmes. Comment représenter et étudier la communication entre différents ordinateurs ?

Il se consacre pleinement à la question à la fin des années 70. C’est une question pratique très pertinente à l’époque : les réseaux entre ordinateurs commençaient à se répandre : le protocole TCP avait été publié en 1974, mais le premier déploiement de réseau d’envergure sous TCP/IP date de 1983. Mais Milner a une vision qui dépasse un cadre donné : il veut un système théorique qui décrit l’interaction entre systèmes et qui soit applicable dans un cadre très large : programmes au sein d’un ordinateur, réseau d’ordinateurs, protocoles de communication, échanges entre des personnes humaines, etc.

En 1980, il publie un livre intitulé A Calculus of Communicating Systems, qui présente sa première réalisation de poids dans le domaine. C’est un langage théorique du même nom (CCS), dans lequel on peut modéliser des systèmes qui évoluent indépendamment, mais qui se synchronisent sur certaines actions.

Par exemple, si vous allez acheter du pain à la boulangerie, vos actions sont indépendantes de celle de votre boulanger, mais il y a un cas particulier de synchronisation : quand vous lui tendez de l’argent, il vous donne du pain, et inversement; l’un n’arrive jamais sans l’autre.

Les applications de ce système CCS sont vastes, de la modélisation d’un distributeur de boissons à l’étude fine de protocoles de communication : est-il possible, par exemple, que deux systèmes se bloquent mutuellement, chacun attendant de l’autre une synchronisation qui ne vient pas ?

Cependant, CCS a des limitations : il ne permet pas de modéliser des réseaux dans lesquels des liens entre deux systèmes se créent ou disparaissent, où la structure du réseau évolue au cours du temps. Milner connaissait ce problème et avait essayé d’intégrer cet aspect à CCS, mais cela n’avait pas marché. Au cours des années 1980, les travaux d’autres chercheurs ouvrent la voie à un modèle plus flexible, et Milner (avec deux autres chercheurs nommés Joachim Parrow et David Walker) les étudie et les améliore entre 86 et 89 : il obtient Pi-calcul (comme la lettre grecque π, choisie un peu au hasard).

C’est un nouveau langage théorique dans lequel les canaux de communications eux-mêmes peuvent être échangés entre les différents systèmes : si j’ai un lien de communication avec A, je peux l’envoyer à B, qui pourra lui aussi parler à A. Ainsi, le réseau peut se reconfigurer au fil du temps. Autrement dit, dans le Pi-calcul, les liens de communication sont eux-mêmes mobiles.

Avec ce formalisme, on peut modéliser la plupart des processus concurrents que l’on rencontre en informatique. L’intérêt d’avoir un modèle théorique, c’est qu’il permet de réduire des systèmes réels, très très compliqués, vers une forme plus abstraite et plus simple, dont on peut étudier les propriétés fondamentales. Par exemple, il est difficile aujourd’hui d’écrire des programmes concurrents (où plusieurs parties du programme s’exécutent indépendamment et interagissent), et cela peut donner lieu à des erreurs très difficiles à repérer, et à corriger. Plutôt qu’essayer de raisonner sur le code concret du programme, qui est très long et très compliqué, le programmeur peut s’arrêter un instant, prendre un papier et un crayon, et construire un modèle du programme (par exemple dans le pi-calcul), qui lui permette de vérifier que la conception ne contient pas d’erreur (pas de risque de blocage du système, d’erreur de synchronisation, etc.) : le système théorique lui donne des outils pour vérifier tout cela rigoureusement. Une fois qu’il est sûr que la conception du programme tient la route, il peut se concentrer sur l’implémentation, qui recèle ses propres difficultés.

Le Pi-calcul a ainsi été utilisé dans des situations très variées : en informatique, il permet de modéliser l’exécution des programmes concurrents, mais aussi par exemple des aspects de sécurité de l’information : est-ce que les données importantes risquent d’être envoyées sur le réseau ? En dehors de l’informatique, il a aussi été adapté pour représenter des réactions chimiques et des systèmes biologiques : un système moléculaire peut être très complexe (énormes molécules, réactions impliquant de nombreuses molécules..), et le Pi-calcul permet de représenter les interactions qui s’y déroulent.

Mais tout n’est pas encore joué : la recherche de modèle d’interactions concurrentes est encore un sujet de recherche actif. De même que Milner était bien conscient des limitations de CCS, certains chercheurs discutent de modifications du Pi-calcul, ou de systèmes alternatifs, et la recherche du langage théorique ultime continue. Milner lui-même y participait, avec son travail sur les bigraphes à la fin des années 2000.

Sources :

Quelques citations pour finir

Pour récompenser le courage de ceux qui ont lu la news jusqu’ici, voici quelques citations de Robin Milner.

Robin Milner raconte sa première rencontre d’un ordinateur, en 1956 : à l’époque, il est choqué par le manque d’élégance des langages de programmation utilisés.

Citation

In 1956 I went on a course on the EDSAC machine here. I regarded programming as really rather inelegant. You’d write one instruction after the other, and it was all rather arbitrary. It seemed to me that programming was not a very beautiful thing. So I resolved that I would never go near a computer in my life!

En 1956, j’ai suivi un cours [à Cambridge] sur la machine EDSAC. J’ai eu l’impression que la programmation n’était vraiment pas très élégante : il fallait écrire une instruction après l’autre, et c’était plutôt arbitraire. Cela m’a donné l’impression que la programmation n’était pas quelque chose de beau. J’ai alors décidé que je ne m’approcherai plus jamais d’un ordinateur !

Citation

We can now begin to describe what goes on outside a computer in the same terms as what goes on inside - i.e. in terms of interaction. [..] We may say that we inhabit [..] an informatic world which demands to be understood just as fundamentally as physicists understand the material world.

Nous commençons à savoir décrire ce qui se passe à l’extérieur de l’ordinateur de la même façon que ce qui se passe à l’intérieur : en termes d’interactions. Nous pouvons dire que nous vivons dans un monde d’information, qui nécessite d’être compris aussi profondément que les physiciens comprennent le monde matériel.

-
Edité par unecrevette_ 23 juillet 2017 à 9:13:02

24 juillet 2017 à 6:04:16

News écrite par bluestorm et colbseton et publiée le 5 avril 2011, sous licence Creative Commons BY-SA 2.0. Republiée ici avec les modifications suivantes : images supprimées, liens morts effacés.

Les assistants de preuves formelles : zoom sur Coq

Dans le domaine des mathématiques assistées par ordinateur et particulièrement en informatique, il existe des logiciels que l'on appelle assistants de preuves. Ils permettent, comme leur nom le laisse deviner, de vérifier la véracité de théorèmes parfois laissés longtemps sans preuve. Dans cette news, nous nous pencherons sur ces assistants, et en particulier Coq. Il ne sera donc pas question ici de parler d'une quelconque nouveauté. Néanmoins, avant de parler de ce logiciel, je vous propose de poser le contexte avec une petite anecdote.

Le théorème des quatre couleurs

Ce fameux problème est un des plus célèbres résultats de mathématiques combinatoires, il est resté longtemps sans preuve malgré son énoncé plus ou moins simple. En effet, il indique que si une carte plane quelconque est découpée en plusieurs régions, alors on peut colorier ces régions avec quatre couleurs différentes sans que deux régions côte à côte aient la même couleur. Bien sûr, la carte n'est pas forcément rectangulaire, la forme varie et il n'est pas rare de trouver des exemples sur des cartes de France ou d'Europe.

Historiquement, c'est en 1852 que Francis Guthrie s'intéresse à la coloriation de la carte des régions d'Angleterre. Il remarque alors qu'il suffit de colorier cette dernière avec quatre couleurs de façon à ce que deux cantons côte à côte soient colorés différemment. Une question survient alors : est-ce que cette propriété est vraie pour toute carte plane (c'est une généralisation) ? Après discussions avec son frère Frederick, mathématicien , la conjecture est publiée en 1878 par Arthur Cayley.

Un an plus tard (très rapidement donc), soit en 1879, Alfred Kempe propose une démonstration de la conjecture qui consistait en une méthode de coloriage appelée chaîne de Kempe. Malheureusement, en 1890, Percy John Heawood montre que la preuve de Kempe s'avère être fausse dans le cas de carte où un pays aurait par exemple cinq frontières, il proposa un contre exemple, le Graphe 4-chromatique de Heawood. En effet, très rapidement les mathématiciens ont préféré traiter le problème sous forme de graphe (ce qui revient bien sûr au même). La démonstration de Kempe s'avère donc fausse, mais ironiquement, elle contenait toutes les idées principales de la vraie preuve.

Dans les années 60, le mathématicien allemand Heinrich Heesch est l'un des premiers à s'intéresser à la résolution de preuve par ordinateur. Il se penche sur le problème des quatre couleurs, et plus particulièrement à sa résolution avec l'outil informatique. Il invente la technique de décharge qui deviendra par la suite essentielle à la preuve. Néanmoins, ce sont deux américains, Kenneth Appel et Wolfgang Haken qui démontrent ce fameux théorème des quatre couleurs en 1976. Ce n'était pas sans conséquences pour la communauté scientifique puisqu'il s'agissait de la première démonstration par ordinateur. Petit à petit, ces assistants sont devenus plus nombreux et se sont développés, c'est entre autres le cas de Coq qui est l'un des plus célèbres.

Les assistants de preuves aident à la démonstration

Les mathématiques sont une discipline extrêmement rigoureuse, car ses objets sont "pur raisonnement", plutôt que des approximations du monde réel. L’idée générale d’une preuve mathématique est de démontrer un résultat en une suite d’étapes de raisonnement correctes, chaque étape étant suffisamment simple pour qu’on puisse la vérifier directement.

Un texte qui décrit un ensemble d’étapes simples permettant, une fois assemblées, d’arriver à un résultat intéressant ; ça ne vous rappelle rien ? C’est aussi de cette façon qu’on décrit les programmes informatiques ! Les informaticiens, surtout ceux qui ont une formation mathématique, ont remarqué cette ressemblance. Les ordinateurs sont des outils très pratiques pour suivre une liste d’étapes simples, même très grosse. On a donc naturellement envie d’écrire des preuves mathématiques comme des programmes que des ordinateurs puissent comprendre. C’est ainsi que l’idée des assistants de preuve, des logiciels qui permettent de faire des preuves sur ordinateur, est née.

Écrire une preuve sur un ordinateur, c’est donc un peu comme programmer. Les concepteurs des assistants de preuve doivent mettre au point un "langage de preuve", dans lequel on écrit les énoncés mathématiques. Une telle preuve est comme un programme, mais il y a une différence importante: on écrit les programmes dans le but de les exécuter plus tard, alors qu’on se contente de vérifier que les preuves sont correctes.

Dans certains langages de programmation, il y a des outils, comme les systèmes de typage (type system) dits "statiques", qui repèrent une partie des erreurs sans lancer le programme, par exemple pendant la compilation ; le reste des erreurs n’est visible qu’à l’exécution. On a aussi développé des systèmes de typage pour les preuves formelles (dependent types), qui sont plus complexes car ils doivent détecter toutes les erreurs de la preuve, et pas seulement une partie.

Depuis le début des années 70, les chercheurs du domaine développent en parallèle des systèmes de preuve et des langages de programmation ; il s’agit en général de langages de programmation fonctionnels (plus proche des mathématiques). Robin Milner a développé ensemble l’assistant de preuve LCF et le langage de programmation ML. Celui-ci a inspiré de nombreux descendants, dont SML, dans lequel est développé l’assistant de preuve Isabelle, OCaml, langage d’implémentation du logiciel Coq, voire Haskell, sur lequel repose le système Agda.

Coq, un assistant développé par l'INRIA

Coq est un des assistants de preuve les plus utilisés aujourd’hui : avec son langage d’implémentation OCaml, c’est un des exemple de succès de la recherche française maintenant utilisés dans le monde entier. Les preuves sont écrites dans un "langage de preuve" qui est aussi un langage de programmation, et qui permet donc aussi d’écrire des programmes. Il possède un système de typage très puissant qui garantit que les preuves sont correctes.

Cette approche combinée, où les preuves sont des programmes, permet d’utiliser le même logiciel pour faire des preuves mathématiques, ou des preuves que des programmes informatiques sont corrects: on définit ce qu’on veut que le programme fasse, sous forme d’une propriété mathématique, et on prouve qu’il vérifie cette propriété. En plus de preuves mathématiques comme le théorème des quatre couleurs, Coq est donc utilisé en informatique, pour vérifier par exemple des algorithmes, des algorithmes et protocoles cryptographiques… Récemment, un compilateur pour le langage C a été écrit entièrement à l’intérieur de Coq, accompagné d’une preuve que le programme assembleur produit est bien équivalent au programme C de départ : le compilateur n’introduit aucun bug.

Malheureusement, l’écriture de preuves vérifiées par ordinateur reste un art réservé à un petit groupe de connaisseurs, beaucoup plus difficile qu’écrire une preuve mathématique sur papier. Sur papier, les mathématiciens s’autorisent à ne pas écrire certains détails, mais il faut absolument tout dire à l’ordinateur ; tout comme il est souvent plus facile de demander à quelqu’un de faire quelque chose que d’écrire un programme qui le fait. Pour améliorer la situation, les assistants de preuve permettent d’utiliser des programmes de recherche automatique de preuve, qui savent "boucher les trous" s’ils sont suffisamment simples, mais l’intégration de ces outils a encore des progrès importants à faire. De même, écrire des programmes vérifiés est difficile et contraignant.

Les méthodes formelles sont déjà utilisées dans les industries où ses difficultés sont compensés par ses avantages, en complément des méthodes de test ; dans certains domaines une erreur peut avoir des conséquences désastreuses, humaines (aéronautique, centrales nucléaires) ou financières, comme pour les fusées spatiales ou chez les fabricants de processeurs : une erreur sur le circuit de multiplication d’un processeur peut coûter des millions…

Enfin, la correspondance preuves-programmes de Coq a un autre intérêt, plus théorique: si les preuves sont écrites de façon "constructive", on peut en extraire un programme qui correspond au contenu calculatoire de la preuve. Par exemple, si un mathématicien prouve dans Coq que tout nombre entier est décomposable en facteurs premiers, on peut en déduire un programme qui prend un entier en entrée, et renvoie la liste de ses facteurs premiers. Ces possibilités ont relancé un débat existant depuis longtemps chez les mathématiciens, les questions de fondements et de constructivisme (tiers exclu, axiome du choix, imprédicativité, etc.). L’informatique a toujours profité des lumières des mathématiques et de la logique, et elle commence à retourner la pareille en apportant un nouveau point de vue et de nouvelles idées…

Sources et liens utiles

Pour aller (vraiment) plus loin (pour aller juste un peu plus loin, consultez les articles de Wikipédia mis en liens dans le texte de la news) :

-
Edité par unecrevette_ 24 juillet 2017 à 6:07:38

25 juillet 2017 à 6:40:06

News écrite par iPoulet et publiée le 10 octobre 2011, sous licence Creative Commons BY-SA 2.0. Republiée ici avec les modifications suivantes : images supprimées, liens morts effacés.

Ocsigen 2, une bouffée d'air frais pour le web

Bien que la programmation web ait été pendant longtemps l'apanage d'une minorité de langages, parmi lesquels on trouvait Perl, PHP ou Java, les choses ont changé. Aujourd'hui, quasiment tous les langages de programmation un peu sérieux possèdent leurs frameworks web, avec leurs points forts et leurs points faibles, et un état d'esprit qui varie souvent fortement d'un framework à l'autre, sous l'influence des langages eux-mêmes.

Ocsigen est un framework web conçu pour le langage OCaml, un langage de programmation fonctionnelle statiquement typé, et développé par le laboratoire français PPS. Relativement différent des technologies auxquelles les développeurs web sont habitués, il propose d'écrire des sites complets, fiables et performants dans le langage OCaml, et a récemment connu d'importantes mises à jour.

Des fondations mûrement réfléchies

Comme beaucoup de technologies alternatives (moins connues que, par exemple, PHP ou Java), Ocsigen tente de présenter des solutions originales à des problèmes récurrents. Avec la version 2, il est possible qu'un certain nombre de ces idées soient suffisamment présentables pour essaimer dans d'autres langages et frameworks, et il est donc intéressant de comprendre pourquoi et comment Ocsigen a vu le jour.

Modéliser les interactions web

L'une des premières sources d'inspiration citées par les auteurs d'Ocsigen est un article de Christian Queinnec (enseignant-chercheur de l'Université de Paris 6) publié en 1999, qui présente notamment un problème récurrent dans les applications web un peu complexes : les formulaires multiples. Lorsqu'un utilisateur passe une commande sur un site de ventes en ligne, il est fréquent qu'il doive valider plusieurs étapes successives (un pour commander des articles, un pour indiquer son adresse de livraison, etc.).

Il est a priori facile de programmer ces interactions avec l'utilisateur : une première idée est d'utiliser des formulaires différents, et des informations sauvegardées par cookies. Mais cette approche a plusieurs défauts : premièrement, que se passe-t-il si l'utilisateur passe plusieurs commandes en même temps ? Les cookies sont partagés par toutes les fenêtres. On pourra alors préférer stocker des informations intermédiaires dans un champ caché.

Mais si notre application souhaite que l'utilisateur adopte un comportement linéaire (un formulaire après l'autre), en réalité les options proposées par le navigateur sont beaucoup plus riches : par exemple, il est possible que l'utilisateur, trouvant que la page se charge lentement, la réactualise (et donc, qu'il renvoie les informations — sans pour autant vouloir passer une deuxième commande). Il est également possible qu'il estime s'être trompé, et qu'il revienne en arrière.

Naturellement, une bonne application doit gérer efficacement tous ces cas de figure. Pour ce faire, Queinnec cherche un moyen de ramener le problème (modéliser les interactions client/serveur) à un autre problème, plus connu. Il propose le mécanisme des continuations, qui ont déjà servi à modéliser des comportements compliqués (comme ceux induits par l'instruction goto de certains langages).

Les services

On voudrait alors utiliser les continuations dans le code d'un site web, pour gérer proprement les actions des utilisateurs. Bien entendu, il est passablement pénible de systématiquement devoir programmer par continuations. C'est là que le concept de framework prend toute son importance : Ocsigen propose un ensemble de concepts et d'outils qui permettent de gérer tout ceci quasi-automatiquement, et distingue les concepts de « services » et de « coservices » (au sens de « services auxiliaires »).

Les premiers correspondant aux services principaux du site, qui sont en quelque sorte des points d'entrée (pouvant être mémorisés dans un signet, par exemple). Les seconds, au contraire, n'existent qu'à côté d'un service principal, et peuvent d'ailleurs être créés dynamiquement (et expirer au-delà d'un délai particulier), ce qui est une façon d'implémenter les continuations.

Prenons un exemple : supposons que nous voulions demander un nombre à l'utilisateur via un formulaire, puis un deuxième dans un second formulaire (lorsque l'utilisateur soumet le premier), et enfin que nous voulions afficher la somme de ces deux nombres lorsqu'il soumet le second formulaire. Bien sûr, l'utilisateur ne doit pas arriver sur la deuxième ou la troisième page sans être passé par la première.

Voici un pseudo-code ressemblant à ce qu'il faudrait écrire avec Ocsigen (mais débarrassé des détails techniques, comme la génération du code HTML — les arguments nommés sont précédés de ~, comme en OCaml) :

let service1 = service ~url:"/calc/" ~paramètres:[] 
let service2 = service ~url:"/calc/" ~paramètres:[entier "i"] 

let handler1 = 
    formulaire 
       ~suivant:service2 
       ~code:( 
         int_input # Entier que l'on passera à service2 
       ) 

let handler2 = 
    let service3 = coservice # Coservice créé dynamiquement 
       ~session:session_courante # Coservice limité à l'utilisateur courant 
       ~paramètres:[entier "j"] in 

    let handler3 = afficher(i + j) in 
    attacher(service3, handler3); 
    formulaire 
       ~suivant:service3, 
       ~code:( 
         int_input # Entier que l'on passera à service3 
       ) 

attacher(service1, handler1); 
attacher(service2, handler2) 

Bien que la syntaxe d'OCaml (et donc le code nécessaire pour utiliser Ocsigen) soit un peu plus compliqué, l'idée y est : le concept un peu difficile à comprendre de continuation est abstrait par la notion de coservice créé dynamiquement.

Ici, les deux services ont la même URL. Selon que l'utilisateur envoie un paramètre ou non, il est donc possible de savoir à quel stade de l'interaction on se trouve. Et le coservice, lui, n'est rattaché à aucun nom : il est donc impossible que le client tombe dessus par hasard.

La programmation fonctionnelle, adaptée pour le web

Parmi les autres travaux précurseurs d'Ocsigen, on trouve également un article de Jean-Vincent Loddo (enseignant-chercheur de l'Université de Paris 13). Celui-ci est notamment l'auteur d'un article sur la programmation fonctionnelle appliquée au développement web.

Selon Loddo, il est facile de se représenter les sites web comme des fonctions, qui dépendent des arguments passés (par requêtes GET ou POST), interrogent éventuellement une base de données, et produisent ensuite un résultat. La nature non connectée du HTTP renforce cette intuition : dans sa conception même, le protocole fait expliciter aux programmeurs les relations entre les différentes pages, et notamment les informations qui doivent être transmises.

Bien que cet argument soit à tempérer, notamment par la présence de sauvegarde d'un état (via les cookies côté client, ou tout autre mécanisme de stockage sur le serveur), il encourage à chercher une nouvelle façon de représenter les services web : pourquoi pas les fonctions, justement ?

Ocsigen, de nouveaux concepts pour le web

Ocsigen diffère des technologies habituellement utilisées pour le web. Ainsi, plutôt que de demander au programmeur d'écrire différents codes sources qui correspondent aux différentes pages du site web (comme on le ferait par exemple en PHP), il propose d'écrire un programme OCaml correspondant au site (éventuellement réparti dans plusieurs fichiers, pour mieux organiser le code, mais ça n'est pas une nécessité), et de compiler tout ce site dans un module, qui sera ensuite chargé par le serveur web, et qui fournira des services aux clients.

La plupart des nouveautés introduites par la version 2 sont des améliorations des idées qui existaient déjà dans Ocsigen. Passons donc en revue les spécificités de la technologie.

Des services typés

À la lumière des travaux précédents, le projet Ocsigen (dirigé par Vincent Balat, enseignant-chercheur de l'Université de Paris 7) propose la programmation (dans le langage OCaml) d'applications riches pour le web, notamment basées sur le concept de services.

Ceux-ci ne dépendent pas du fichier dans lequel ils sont placés (comme ça serait par exemple le cas pour une page web sur un site PHP), mais sont « attachés » par le programmeur à une URL particulière, avec une liste d'arguments que doit pouvoir recevoir le service (et qui peuvent être tout ce que l'on est habitué à envoyer avec un formulaire). Ces arguments doivent être typés, c'est-à-dire que le programmeur doit indiquer leur type (entier, flottant, chaîne… ou de nouveaux types dont le programmeur précise la représentation).

C'est ensuite le serveur particulier d'Ocsigen qui s'occupe de choisir le service correspondant à une URL et à des paramètres donnés. Le fait que les paramètres des services soient typés permet d'éliminer certaines erreurs potentielles, sans qu'il soit nécessaire de tester ces parties minutieusement (et en empêchant les visiteurs de tomber dessus par erreur !).

En outre, dans un code Ocsigen, les différents services du site sont des valeurs OCaml comme les autres, et peuvent être utilisés comme cibles pour les liens et les formulaires (on écrira ainsi let nouveau_formulaire = get_form ~service:service_cible … pour déclarer un formulaire vers un service nommé service_cible). Comme le code OCaml est ensuite compilé, plusieurs vérifications sont faites : notamment, le compilateur s'assure que vous utilisez des services qui existent (ce qui diminue les chances d'introduire des liens morts dans le site). Et surtout, il s'assure que les formulaires envoient bien toutes les données au service ciblé, et qu'elles ont toutes le bon type !

Si ça n'est pas le cas, le service ciblé par l'utilisateur ne sera pas appelé. À la place, celui-ci sera redirigé sur un service traitant d'erreurs (s'il a été défini — ce qui est notamment possible grâce au paramètre ~fallback, lors de la création d'un service POST, ou bien grâce à un traitant « global »).

Un code vérifié

OCaml est un langage statiquement et fortement typé, ce qui veut dire qu'il détermine tous les types des variables utilisées au moment de la compilation (et pas pendant l'exécution, par exemple PHP ou JavaScript), et qu'il s'assure que toutes les opérations utilisées ont un sens qui ne nécessite pas de conversions implicites (contrairement, ici encore, à ces deux langages). Cela permet d'écrire du code plus fiable (car le compilateur ne laisse pas passer d'erreurs de type qui ne seront détectées que pendant l'exécution), et aussi plus rapide (car il optimise en conséquence) lorsque celui-ci est compilé nativement. Comme le compilateur OCaml fait ceci systématiquement (en ne demandant que très peu d'indications de la part du programmeur), pourquoi ne pas l'utiliser pour vérifier également les codes XHTML, JavaScript et SQL ?

Bien qu'une application Ocsigen puisse fonctionner avec un code XHTML écrit indépendamment, l'une des autres idées de Jean-Vincent Loddo était d'utiliser un langage fonctionnel typé moderne pour vérifier le code XHTML écrit par le développeur. Dans Ocsigen, il est ainsi possible de s'assurer que son code XHTML est suffisamment proche des recommandations du W3C, car celui-ci est vérifié à la compilation. Pour cela, un des composants du framework, nommé Eliom, propose beaucoup de fonctions OCaml toutes prêtes, servant à générer le code XHTML. Par exemple, il est nécessaire de passer à la fonction head un titre, tagué avec la fonction title, et c'est également le seul endroit où l'on peut mettre une telle balise : grâce au typage, tout ceci peut être vérifié sans qu'il soit nécessaire d'utiliser des validateurs tiers.

Le programmeur n'est pas obligé de directement se soucier de ces variants polymorphes, et peut utiliser directement les fonctions d'Eliom, qui permettent donc de manipuler le code XHTML directement comme des fonctions OCaml. De même, Eliom fournit un certain nombre de fonctions toutes prêtes pour générer des formulaires typés, ou des liens vers des services qui passent des arguments correctement typés. On élimine donc un ensemble relativement important d'erreurs dans le programme, grâce à l'aide du compilateur. Le code a alors la forme de

let titre = … (* valeur du titre *) 
in 
    (html 
       (head (title titre) []) 
       (body [h1 [titre]; 
          … (* suite de la page *)])) 

D'autres modules sont disponibles, soit pour émettre d'autre code que du XHTML (comme du SVG ou du HTML 5), soit pour utiliser des syntaxes un peu moins lourdes. Mais les vérifications d'Ocsigen ne se limitent de toute façon pas au code serveur et au XHTML : en réalité, le framework va plus loin, et permet d'écrire, en OCaml, du code JavaScript et SQL, et donc de vérifier ceux-là également.

Du JavaScript en OCaml : le compilateur jsofocaml

De plus en plus de technologies permettent aujourd'hui d'écrire des scripts web clients dans un autre langage que JavaScript. Citons par exemple CoffeeScript, Cappuccino, Dart (le nouveau langage de Google)… elles proposent alors des compilateurs qui transforment les programmes écrits dans ces langages en JavaScript, avec une perte d'efficacité le plus souvent insignifiante. Le but est systématiquement d'ajouter des fonctionnalités à JavaScript, comme un typage statique (dans le cas de Dart), ou des messages (pour Objective-J, le langage de Cappuccino).

Ocsigen permet, de la même façon, d'écrire en OCaml du code qui sera ensuite compilé en JavaScript. Cela permet d'écrire dans un même programme OCaml du code qui sera réparti (à la compilation) chez le client et chez le serveur, et donc de partager du code et des types, de rendre le code source plus compréhensible — et surtout de pouvoir écrire des applications clientes en OCaml, ce qui permet de bénéficier des forces de ce langage, dont le typage statique.

Ainsi, les objets JavaScript sont manipulables directement dans du code OCaml, et les deux codes (client et serveur) peuvent communiquer (via par exemple le module Eliom_bus). Parce qu'ils sont écrits dans le même langage, ces codes peuvent représenter les données de la même façon lorsque c'est pertinent : c'est un avantage en termes de facilité de développement, et de sécurité.

Du SQL en OCaml : le module Macaque

Disposer d'un langage fiable et statiquement typé pour écrire l'application serveur ne suffit pas à garantir l'absence d'erreurs de types, dont certaines ne seront découvertes qu'à l'exécution : même si un programme OCaml est typé correctement, certaines fonctions (dites partielles) peuvent échouer à l'exécution, et provoquer des erreurs (qui doivent être traitées par le programmeur, à l'aide de code supplémentaire et rébarbatif).

Ainsi, on voudrait pouvoir écrire des requêtes sur une base de données dans un langage vérifié, éventuellement embarqué dans le langage de programmation serveur. Cela permet, ici encore, de faire correspondre plus fortement les typées utilisés par la base de données, et par le reste de l'application. Au sein d'Ocsigen, le module Macaque (encore relativement incomplet et peu documenté du fait de sa jeunesse) est chargé de jouer les intermédiaires, et permet d'écrire des requêtes par compréhension, directement dans du code OCaml.

Par exemple, une requête SELECT a la forme <:select< row | row in $sql_table$; row.id < 50 >>. Macaque s'occupe, à la compilation, de traduire la deuxième forme en une requête SQL, et permet de vérifier (sans qu'il soit nécessaire de faire de test) que la table utilisée possède les bons champs, que ceux-ci sont bien du type souhaité, etc. Le module permet également d'encoder dans le type (et donc de vérifier) certaines propriétés, comme la non-nullabilité des valeurs (qui garantit, sous certaines conditions, l'impossibilité de travailler par erreur sur une valeur SQL NULL).

Il y aurait encore beaucoup de choses à dire sur Macaque et tous les problèmes que ce module essaye de résoudre. Son auteur (qui n'est autre que bluestorm, élu Zéro de l'année 2007 !) a écrit à son sujet un rapport de stage, qui décrit la problématique et les principaux choix de conception de la bibliothèque, ainsi que quelques articles de blog.

Un petit mot sur Lwt

Conçue à l'origine pour supporter Ocsigen, Lwt est une bibliothèque de multithreading léger pour OCaml. Elle implémente un système de multithreading coopératif, une des façons les plus simples de représenter l'exécution simultanée de plusieurs sous-programmes. L'idée est de donner la main à un programme qui s'exécute jusqu'à ce qu'il décide lui-même de céder sa place (interrompant alors son calcul). Un autre programme est alors choisi, et est exécuté à son tour, et ainsi de suite. Ce mécanisme permet de gérer un grand nombre de threads, et d'économiser de la mémoire en évitant de dupliquer une pile et tout un contexte d'exécution.

Mais là où réside sa force principale, c'est dans la facilité déconcertante qu'offre Lwt pour faire de la programmation asynchrone (accès aux fichiers, envoi ou réception de données sur le réseau, etc.) : lors d'une opération bloquante, les autres threads sont automatiquement exécutés pendant l'attente et une fois que le résultat est apparu, le thread qui a fait l'appel est réveillé.

Enfin, Lwt vient avec une large bibliothèque couvrant beaucoup de besoins : manipulations de fichiers, communication sur le réseau, exécution de processus, etc. Les différents composants d'Ocsigen s'appuient dessus, ce qui garantit une capacité de passage à l'échelle raisonnablement bonne. Le programmeur est également invité à les utiliser pour structurer l'exécution de son programme, dans le style monadique. Un port de la bibliothèque a également été réalisé pour JavaScript, sous le nom de Lwt_js : les threads légers s'adaptent parfaitement au cadre d'exécution mono-threadé de JavaScript.

Quel sera le web de demain ?

Parmi les frameworks web commerciaux utilisés aujourd'hui, il est clair qu'Ocsigen est absolument insignifiant. Très peu de sites sérieux l'utilisent, et à peine plus de projets communautaires. Cependant, bien qu'elle soit encore inachevée et trop peu documentée, la version 2 du framework confirme une bonne compréhension du problème initial, ainsi qu'une mise en œuvre réussie : les développeurs ont réussi à obtenir un ensemble de bibliothèques puissantes, qui peuvent être combinées pour produire des sites web efficaces.

Au final, sans le soutien adéquat, il est peu probable qu'Ocsigen s'impose un jour comme un ténor des frameworks web. En revanche, il confirme l'intérêt de continuer à explorer de nouveaux concepts pour la programmation (et le web en particulier), et suggère de nouvelles pistes à suivre dans des technologies plus traditionnelles — et peut déjà se montrer très utile et pratique.

Liens complémentaires

  • L'article original sur Ocsigen dont est extrait cette news, du même auteur.
  • Le site web d'Ocsigen, qui contient toute la documentation du framework. Le tutoriel officiel est basé sur des exemples concrets, et notamment sur la création d'une application de dessin collaboratif. Attention, il est nécessaire de déjà avoir appris OCaml.
  • Une introduction en français à Ocsigen 2, qui propose plus d'explications pour les débutants, et fournit un exemple très simple. À suivre.
  • La récente thèse de Benjamin Canou sur la programmation web typée, qui détaille notamment O'Browser, une machine virtuelle pour OCaml en JavaScript (une approche différente de celle décrite plus haut). Claire, complète et écrite en français, cette thèse aborde également un tour d'horizon des technologies web comparables à Ocsigen (et notamment Opa, développé par la société française MLState).
  • Des projets similaires : Lift, un framework web MVC dans le langage statiquement typé Scala ; HOP, un autre framework complet de développement web, plus orienté vers le développement d'applications de bureau ; Links, un framework plus simple mais comparable ; Ur/Web, qui revendique une plus grande flexibilité et un typage plus avancé.

Merci à asmanur pour son paragraphe sur Lwt et ses différents conseils. Merci également à anmee et spider-mario, et aux développeurs du projet qui ont accepté de relire cette dépêche.

-
Edité par unecrevette_ 25 juillet 2017 à 6:43:35

27 juillet 2017 à 4:30:52

Un grand merci à la modération pour avoir épinglé ce sujet en post-it. On espère que ça permettra à un maximum de gens de découvrir de nouvelles choses !

-
Edité par unecrevette_ 27 juillet 2017 à 4:31:07

Lisez ici les news de qualité de la v3 du SdZ !

× Après avoir cliqué sur "Répondre" vous serez invité à vous connecter pour que votre message soit publié.
  • Editeur
  • Markdown