This is a set of libraries for working with abstract syntax trees and libraries of strict types – type system made with category theory which ensures provable properties and bounds for the in-memory and serialized type representation.
Strict types is a formal notation for defining and serializing generalized algebraic data types (GADT) in a deterministic and confined way. It is developed with type theory in mind.
Strict Types are:
- 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,
- portabile, i.e. can run on ahy 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 verifiabile.
To learn more about strict encoding read the spec.
Strict types works with type definitions. It allows:
- static analysis of data types, like
- defining semantic type ids;
- specifying exact memory layout;
- type equivalence in terms of semantics and memory layout;
- size of serialized data
- composing types into type libraries;
- versioning type libraries basing on the semantic types;
The library allows to generate & compile strict type libraries (STL) from rust
types implementing StrictEncoding trait -- and ensures that the
deserialization with StrictDecode follows the same memory and semantic layout.