Welcome to Cogent’s documentation!¶
Cogent is a restricted, polymorphic, higher-order and purely functional language with uniqueness types and without the need for a trusted runtime or garbage collector.
Cogent is restricted. Cogent is not a general-purpose language. It omits certain features that one might come to expect from a programming language. For instance, Cogent doesn’t support general recursion.
Cogent is polymorphic. Parametrically. This is similar to templates in C++, or generics in Rust.
Cogent is higher-order. Functions are values—they can be function arguments.
Cogent is purely functional, in the sense of the functional programming paradigm: functions are stateless, and the result of a function is deterministically defined by the arguments to the function, just like a mathematical function.
Cogent has uniqueness types: as a means to control references, every linear object (roughly equivalent to heap-allocated object) can only have one unique reference.
Cogent has no trusted runtime. Cogent compiler generates C code, so the trusted component is limited to the C runtime system.
Cogent has no garbage collector. Since Cogent compiler generates C code, we would manage memory manually, like we do in any C program.
Cogent has a certifying compiler. Cogent is designed for writing and formally verifying systems code. That’s why we compromise on language expressiveness for verifiability.
This documentation is for anyone who wants to try out or use Cogent. We assume that you have a basic understanding of the Cogent project already, including what Cogent is about, the approach that we take in this research, and what Cogent brings you. If you don’t, you may want to first read about the Cogent project.
- 1. Preamble
- 2. Cogent Quick-Start Guide
- 3. Cogent Installation Guide
- 4. Cogent Surface Syntax
- 5. Antiquoted C
- 6. How To Use The Cogent Compiler
- 7. Verification
- 8. Meta-Documentation