Statebox is developing a visual language for modeling processes in a compositional way, and a technology stack for executing them.
In doing so, we rely on groundbreaking mathematical research in the areas of category theory, type theory, Petri nets, open games, cryptography, and others.
We incorporate these into a formally verified functional programming approach, which allows us to provide unprecedented correctness guarantees.
The main properties of the Statebox language are:
Visual - use of diagrams and Petri nets for their computational and diagrammatic reasoning properties.
Compositional - the entire stack is designed from a category theory perspective in order to maximize compositionality, not to be confused with modularity.
Correct by Construction - end-to-end correctness proofs are a fundamental design principle, not an afterthought. According to this philosophy we prefer a restricted, always terminating language (a non Turing complete one).
Abstraction - the core of the language is a mathematically minimalistic structure aimed to facilitate reasoning about its behaviour
The main parts of the ecosystem are:
Visual Editor - allows for drawing and interacting with the Statebox flavour of Petri nets as well as their analysis (reachability, deadlocks, termination etc.).
Engine - a dependently typed core which ensures that the mathematical foundations specified in the monograph are preserved and implemented in a sound way.
Typedefs - an intermediary language for translating types from Statebox processes into target languages. It is essentially a well structured data encoder/decoder. It's developed by Statebox and you can find out more on github and the official website.
CQL (Categorical Query Language) - category theory is a foundational principle at Statebox and we want our data to be categorical as well. We developed a CQL implementation in Haskell in close collaboration with Conexus.ai.