Towards a specification language and an ecosystem to specify, test, and verify OCaml programs – GOSPEL

The GOSPEL project aims to grow the definition of Gospel, a specification
language for OCaml; to develop an ecosystem of tools that understand Gospel,
including documentation tools, testing tools, and program verification tools;
and to carry out a number of case studies so as to validate the design of
Gospel and the applicability of the tools.

Gospel allows decorating a piece of OCaml code with a specification that
describes how this code can be used and what it does. This specification is
then used by various tools to generate documentation, to perform automated
testing, and to perform automated or interactive program verification.

Gospel aims to become a de facto standard language that programmers can
learn easily and that many tools can adopt as a common basis.

We focus on OCaml because it offers a unique combination of simplicity,
expressive power, efficiency, and long-term stability, and because it is used
in academia and industry to develop complex and critical software. In
comparison with lower-level programming languages, OCaml removes several
sources of unsafe behavior, making program verification easier, but also
offers powerful ways of assembling programs out of basic components, making
specification more challenging.

We wish to demonstrate that Gospel allows catching bugs that OCaml's type
discipline cannot detect and that it allows achieving increased safety at a
relatively small cost.

Our main objectives are:

1. Develop the Gospel language, so as to increase its expressive power, while
keeping it simple.

2. Develop the Gospel tool ecosystem, including the Gospel type-checker, the
Merlin IDE, documentation generation tools, runtime testing tools, and
static verification tools.

3. Stress and demonstrate Gospel via case studies, ranging from simple library
modules to complex pieces of real-world critical software.