Strict types AST and typelib implementation

Protobufs for functional programming

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.

Contributing

CONTRIBUTING.md