Welcome!

Welcome to the Gospel documentation. We provide several resources to get you started with formal specifications for your OCaml programs.

• If you are entirely new to Gospel, please head out to the Getting Started section. You'll learn how to install Gospel and then use it to write your first specification.
• The Walk-through section showcases real-world OCaml interfaces, including a comprehensive explanation of the specification process and language features.
• More detailed explanations of the language features are available in the Language Reference section.
• Some information about the Gospel Standard library are available in the corresponding section.
• Short questions sometimes deserve short answers. You can also check out the FAQ section for common questions about Gospel's design, semantics, and features.

We are dedicated to making Gospel an easy-to-use specification language for OCaml developers. Any comment or suggestion on the language or its documentation is welcome. Please feel free to open a discussion on Github to share your ideas or ask questions.