Strict types is a project doing formal notation and serialization for generalized algebraic data types (GADT).

In simple terms, strict encoding is a protocol buffers for functional programming (or, for rust devs, functional-style serde).

Strict encoding is both a language for defining GADT and libraries for their
serialization. It is:

• schema-based (with the schema being strict encoding notation),
• semantic, i.e. defines types not just as they are layed out in memory,
  but also depending on their meaning,
• deterministic, i.e. produces the same result for a given type,
• portable, i.e. can run on any hardware architecture and OS, including
  low-performant embedded systems,
• confined, i.e. provides guarantees and static analysis on a maximum size
  of the typed data,
• formally verifiable.

Strict types is a non-commercial project run by Swiss non-profit UBIDECO Institute (UBIDECO stands for "ubiquitous deterministic computing") on donations. Support of our sponsors is the only way we can continue to work on this project.