GOSPEL — Vers un langage de spécification et un écosystème pour spécifier, tester et vérifier des programmes OCaml

Le projet GOSPEL vise à enrichir la définition de Gospel, un langage de spécification pour OCaml; à développer un écosystème d'outils basés sur Gospel; et à effectuer un certain nombre d'études de cas permettant d'éprouver expérimentalement l'utilisabilité de Gospel. Gospel permet d'annoter du code OCaml avec une spécification qui décrit comment ce code est utilisé et quel service il rend. Cette spécification est ensuite utilisée par divers outils pour engendrer de la documentation, effectuer des tests automatisés, et vérifier la correction fonctionnelle de ce code. Gospel vise à devenir un standard de fait, que les programmeurs peuvent apprendre aisément, et que les outils peuvent adopter comme base commune. Nous choisissons OCaml parce qu'il offre une combinaison unique de simplicité, de pouvoir expressif, d'efficacité, et de stabilité à long terme, et parce qu'il est utilisé dans le monde universitaire et dans l'industrie pour développer des logiciels complexes et critiques. Comparé à des langages de plus bas niveau, OCaml supprime plusieurs sources potentielles de comportement aberrant, ce qui facilite la vérification de programmes, mais propose également des moyens puissants pour assembler un programme à partir de composants élémentaires, ce qui rend la spécification plus difficile. Nous souhaitons démontrer que Gospel permet de détecter des erreurs auxquelles le système de types d'OCaml est insensible, d'où une sûreté accrue pour un surcoût limité. Nos principaux objectifs sont de: 1. Développer le langage Gospel, de façon à accroître son pouvoir expressif, tout en préservant sa simplicité. 2. Développer l'écosystème des outils fondés sur Gospel, dont le typeur de Gospel, l'IDE Merlin, et des outils de documentation, de test, et de vérification. 3. Éprouver Gospel et en démontrer l'intérêt via des études de cas, allant de bibliothèques simples jusqu'à des composants logiciels complexes tirés d'applications industrielles critiques.