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

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.