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.

Jeudi 22 janvier est sortie la version 1.3.0 de vera++ : programme permettant de faire des vérifications de style de code sur du C++. Il est scriptable et permet également la refactorisation de code.

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.

En bref : inflectiones est une bibliothèque (Python3, GPLv3) qui permet de conjuguer et de décliner des mots. Le travail inverse (analyser un mot pour en dégager les caractéristiques morphologiques) ne m'intéressant pas, n'a pas été codé. Enfin, seuls quelques exemples tirés du grec ancien et de l'esperanto sont disponibles, voyez les exemples ci-dessous. Le projet n'en est qu'à ses débuts et attend du renfort !

LinuxFr.org propose des dépêches et articles, soumis par tout un chacun, puis revus et corrigés par l'équipe de modération avant publication. C'est la partie la plus visible de LinuxFr.org, ce sont les dépêches qui sont le plus lues et suivies, sur le site, via Atom/RSS, ou bien via partage par messagerie instantanée, par courriel, ou encore via médias sociaux.

Ce que l’on sait moins, c’est que LinuxFr.org vous propose également à tous de tenir vos propres articles directement publiables, sans validation a priori des modérateurs. Ceux-ci s'appellent des journaux. Voici un florilège d'une dizaine de ces journaux parmi les mieux notés par les utilisateurs… qui notent. Lumière sur ceux du mois d'août passé.

• Annonce : Manux 0.0.1 par Emmanuel Colbus ;
• Power8 - OpenPower : l'hégémonie du x86 pourrait-elle être bousculée dans le monde serveur ? par Dabowl_75 ;
• Gnome: ça faisait longtemps qu'on avait pas lancé un flamewar à propos de notre bureau… par gnumdk ;
• Un module noyau pour le support exFAT, en GPLv2 ! par ymorin ;
• Aime-moi tendre, aime-moi vrai. par 못 옷 홋 — 바르텅 마티으 ;
• Retour d'expérience avec le langage J par anaseto ;
• Kit de démarrage Python par flan ;
• Découvrez la compression de données ! (et l'humour algorithmique) par palkeo ;
• bon anniversaire ….. par cortex62 ;
• Ras le bol des plateformes d'e-recrutement par octane.

Le Tcl Core Team est heureux d'annoncer la sortie de la version 8.6 du langage de script Tcl et de la bibliothèque d'interface graphique Tk. C'est la première version stable de la branche Tcl/Tk 8.6 dont le développement a commencé en mars 2008.

Parmi les nouveautés pour Tcl, le support officiel de la programmation orientée objets dans le noyau, l'évaluation stackless, les coroutines, une interface commune d'accès aux bases de données SQL dans le noyau, la gestion des exceptions, les canaux virtuels, le support de la compression zlib dans le noyau.

Parmi les nouveautés pour Tk, le support du format PNG, un nouveau sélecteur de fonte, le déplacement absolu des objets dans le widget canvas et les textes obliques.

À noter un changement d’infrastructure : le développement de Tcl/Tk n'est plus hébergé sur Sourceforge avec CVS mais sur un site spécifique avec le gestionnaire Fossil développé par D. Richard Hipp (le créateur de SQLite). Il en est de même pour les deux bibliothèques standards (Tcllib et Tklib).

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.