Le laboratoire Microsoft Research travaille à plusieurs projets visant à faire progresser le domaine du développement de logiciels, notamment en automatisant et rationalisant des tâches de programmation, ce qui est considéré comme pouvant faire partie du futur du développement de logiciels. Voici deux de ces projets, les langages Bosque et F*.

Le langage Bosque

Le langage de programmation Bosque est une expérience de conception de langage de programmation régularisé pour un cycle de vie de développement logiciel rapide et fiable assisté par machine. Il s'agit d'un effort de co-conception de langage et d'outils axé sur l'étude des implications théoriques et pratiques de :

• Concevoir explicitement un langage de représentation intermédiaire de code (ou bytecode) qui permet un raisonnement de code automatisé approfondi et le déploiement d'outils de développement, de compilateurs et de systèmes d'exécution de nouvelle génération.
• Tirer parti de la puissance de la représentation intermédiaire pour fournir un langage de programmation qui est à la fois facilement accessible aux développeurs modernes et qui fournit un ensemble riche de fonctionnalités de langage utiles pour développer des applications à haute fiabilité et hautes performances.
• Adopter une perspective de développement cloud en premier lieu sur la programmation pour relever les défis émergentspour un modèle de développement cloud distribué basé sur des architectures de microservices, sans serveur et RESTful.

Voici à quoi ressemble du code Bosque :

Le langage Bosque est présenté plus en détail ici. Le langage Bosque est un logiciel libre sous licence MIT disponible sur GitHub.

Le langage F*

F* est un langage de programmation fonctionnel à usage général avec des effets destinés à la vérification de programme. Il combine l'automatisation d'un outil de vérification déductive soutenu par SMT avec la puissance expressive d'un assistant de preuve basé sur des types dépendants. Après vérification, les programmes F* peuvent être extraits en code OCaml, F#, C, WASM ou ASM efficace. Cela permet de vérifier l'exactitude fonctionnelle et la sécurité d'applications réalistes. Le principal cas d'utilisation en cours de F* est la création d'un remplacement vérifié et instantané pour l'ensemble de la pile HTTPS dans Project Everest, un effort de collaboration pluriannuel axé sur la création d'une pile de communications vérifiée et sécurisée conçue pour améliorer la sécurité de HTTPS

Le langage F*, ou FStar, est un logiciel libre sous licence Apache 2.0 disponible sur GitHub. Il dispose également d'un site officile, star-lang.org qui propose un didacticiel.