L'assistant de preuve Coq, deux fois primé l'année dernière, vient de sortir en version 8.5 bêta. Attendue depuis plus d'un an déjà, on trouvera au menu de cette version un nombre certain de changements en profondeur.

Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la correspondance de Curry-Howard, Coq peut être vu aussi bien comme un langage de programmation que comme un système de preuves mathématiques. Il est, de fait, employé par les deux communautés. Parmi les développements en Coq, on peut citer par exemple le compilateur C certifié CompCert sur le versant informatique et la preuve du Théorème de Feit et Thompson sur le versant mathématique. Plus récemment, une des failles d'OpenSSL a été découverte grâce à Coq[^0] . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.

On rappellera dans le reste de la dépêche les grands principes qui sous-tendent Coq, ce qu'il est, ce qu'il n'est pas, puis on détaillera les changements introduits dans cette version.

La version 4.03.0 du langage OCaml est paru le 25 avril 2016. OCaml est un langage fonctionnel de la famille des langages ML (dont font partie SML et F#, ou Rust avec une définition élargie).

OCaml est entre autre utilisé pour implémenter le langage Coccinelle (régulièrement utilisé dans la communauté des développeurs du noyau Linux) ou MirageOS (ensemble de bibliothèques pour construire des unikernels). On compte aussi l'implémentation du langage Hack chez Facebook, l'interpréteur de référence pour le projet WebAssembly, ou encore l'analyseur statique de Code C Frama-C.

Il s'agit d'un langage fonctionnel multi-paradigmes fortement typé qui permet de mélanger librement les paradigmes fonctionnel, impératif et objet. Cette version 4.03 fait suite à la version 4.02 publiée en juillet 2015.

Mozilla et la communauté Rust ont annoncé la version 0.10 de Rust le 3 avril. Rust est un langage de programmation développé par Mozilla. La version 0.1 a été annoncée par Mozilla le 20 janvier 2012. Pour découvrir le langage, on peut se référer au nouveau site web sur lequel on peut lire :

Rust est un langage de programmation système qui est extrêmement rapide, empêche presque tous les plantages et élimine les accès concurrent.

Rust se veut donc une alternative à C/C++, comme D et Go, et possède tout comme ces derniers un ramasse-miettes, mais qui est optionnel. Sa syntaxe est proche de celle du C/C++/Java tout en étant beaucoup plus expressif. Sa force est de mélanger les fonctionnalités de différents paradigmes, beaucoup venant du fonctionnel (immuabilité par défaut, modèle objet proche de celui d'Haskell, fermetures, etc). Il met l'accent sur la sûreté d'exécution, notamment grâce à son système élaboré de pointeurs intelligents et son système de types forts, sans sacrifier les performances.

Depuis la version 0.9, qui a fait l’objet d’une dépêche, les efforts ont notamment porté au cours des 1500 changements sur la simplification du langage. Le langage Rust n'est pas stabilisé, cela viendra avec la version 1.0.

Cette itération de développement a apporté le découpage de la bibliothèque libextra, introduit des extensions de syntaxe inter crate, amélioré la manipulation des pointeurs avec le trait Deref et la gestion des erreurs des entrées/sorties.
En dehors du compilateur, cette nouvelle version a vu l'introduction d'un nouveau processus de RFC ainsi que la construction quotidienne des installateurs binaires.

Des améliorations ont été données à l'infrastructure de tests et aux scripts de construction. Des installeurs sont désormais disponibles pour Linux, MacOS et Windows. Même si certains font tourner Rust sur ARM, ce n'est pas une architecture proposée dans la documentation.

Comme pour les précédentes versions, cette version 0.10 doit être considérée comme une version alpha, appropriée pour les adopteurs précoces et les amateurs de langages.

Gambas est un langage de programmation orienté objet, basé sur un interpréteur BASIC, et une plate‐forme de développement complète comportant, entre autres, un compilateur, un interpréteur, un ensemble de modules complémentaires (appelés composants) et un environnement de développement intégré. Le tout est distribué sous licence GNU GPL v2 ou supérieure.

La précédente dépêche datant de septembre 2012, profitons de la sortie de la version 3.12 pour présenter comment le langage a évolué depuis six ans.

Nous invitons ceux qui ne connaîtraient pas Gambas à lire préalablement la présentation du logiciel sur le site Web, ainsi que la dépêche précédente.

Comme dans la dépêche précédente, il y a quelques coups de gueules, mais ils sont cette fois répartis dans le texte (et partiellement édulcorés en modération).

Rust est un langage de programmation conçu pour répondre aux problématiques modernes des gros logiciels clients et serveurs utilisant Internet, en particulier la sécurité, la gestion de la mémoire et la parallélisation. Il concurrence donc directement les langages C et C++.

Vendredi 15 mai 2015, trois ans et demi après la sortie de la version 0.1, Rust sort en version 1.0 ! Il y a eu beaucoup de changements depuis : le langage a très fortement évolué, une communauté de développeurs/euses s’est formée, de nombreuses bibliothèques et un guide d’apprentissage du langage ont été créés, et la documentation a été améliorée.

L’arrivée d’une version stable est un évènement bienvenu puisqu’elle permet de pouvoir utiliser le langage plus sereinement. Le langage s’ouvre donc un peu à un public plus large que l’enthousiaste et aventureuse équipe de développement de Servo ou autres pionniers/ères dans l’utilisation de Rust. Que ce soit dans des contextes personnels ou professionnels, les changements réguliers dans le langage repoussaient de nombreux/ses utilisateurs/trices potentiel·le·s.

D’après Wikipédia, « Rust est un langage de programmation compilé multi-paradigme conçu et développé par Mozilla Research. Il a été conçu pour être « un langage sécurisé, concurrent, pratique », prenant en charge les styles de programmation purement fonctionnelle, modèle d'acteur, procédurale et orientée objet. »

Rust a été largement couvert sur LinuxFr.org, à travers les versions 0.7, 0.8, 0.9, 0.10, 0.11, 0.12, la version 1.0-alpha, et enfin la version 1.0.

Après des années d’efforts, nous sommes heureux d’avoir libéré le code d’une nouvelle technologie Web nommée Opa. La licence choisie est la GNU Affero General Public License version 3 (AGPLv3).

Cette dépêche a pour but de vous expliquer ce qu’est, et n’est pas, Opa.

Après plusieurs années passées à parlementer, la nouvelle norme Ada 2012 vient enfin d'être publiée par l'ISO sous le numéro ISO/IEC 8652:2012. Il s'agit donc de la quatrième révision du langage ajoutant ainsi différentes fonctionnalités par rapport à la version 2005.

N. D. M. : GNAT est le compilateur Ada du projet GNU, faisant partie de GNU Compiler Collection (GCC). Toujours en logiciel libre, on peut citer MaRTE OS un système d'exploitation libre temps-réel en Ada.

La version 4.07.0 du langage OCaml a été publiée le 10 juillet 2018 soit quelques mois après la sortie de la version 4.06.0, annoncée le 3 novembre 2017. OCaml est un langage fonctionnel de la famille des langages ML (dont font partie SML et F#). Il s’agit d’un langage fonctionnel multi‐paradigme fortement typé qui permet de mélanger librement les trois paradigmes : fonctionnel, impératif et objet.

OCaml arrive en version 4.07 avec un tout nouvel espace de noms, Stdlib, pour sa bibliothèque standard. Ce nouvel espace de noms présage l’intégration progressive de nouveaux modules dans la bibliothèque standard.

Un autre changement majeur, OCaml 4.06 marque la fin de la transition vers des chaînes de caractères immuables, changement amorcé dès OCaml 4.02 .

À côté de ces changements majeurs, on retrouve de nombreuses améliorations de qualité de vie : de nouveaux opérateurs d’indexation et des champs hérités pour les types objets. Mais aussi pas mal de travail de fond pour préparer l’intégration de la branche multicore, améliorer les passes d’optimisations Flambda, ou faire évoluer le système de types en fixant des irrégularités.