What is Statebox?
Statebox is developing a technological stack based on a visual programming language. It's not a general purpose programming language but one focused on modeling and executing processes. The Statebox language is built using a functional programming approach which utilizes, amongst other things, category theory, Petri nets, open games, logic programming and cryptography.
Main properties of the Statebox language:
- Abstraction - the core of the language is a mathematically minimalistic structure aimed to facilitate reasoning about its behaviour
- Compositionality - the entire stack is designed from a category theory perspective in order to increase compositionality, which is quite different from modularity.
- Visual - use of diagrams and Petri nets for their computational and diagrammatic reasoning properties.
- 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).
The ecosystem for the language is composed of several main parts:
- 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.
- AQL (Algebraic Query Language) - category theory is a foundational principle at Statebox and we want our data to be categorical as well. That's why we're collaborating with Categorical Informatics to bring AQL to our ecosystem.