A summary of Bolt:

Capabilities: linear, thread, read

Traits have a capability associated with them, and consist of a list of required fields.

Classes implement a single trait and associated capability and consist of a list of directly-accessible fields.

Bolt's expression syntax was inspired by Slang in 1B Compilers Construction, supporting first-order functions and structured fork-join concurrency through finish-async construct.

Bolt's type-checker performs full type inference.

The data-race type-checker enforces each of the capabilities, as well as enforcing that a given alias to a mutable object can only be accessed in a single thread.

The interpreter translates the typed AST to bytecode executed on a stack machine, with a thread pool where each thread has a local stack and there is a global heap, and the threads are scheduled manually. The interpreter runs in OCaml.

The expect tests consist of Bolt programs and their outputs for each of the stages: parsing, type-checking, data-race type-checking and for the execution trace of the interpreter. A subset of these contain data-races and are flagged as such by the data-race type-checker.