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. You can learn more on the about page
What sets Statebox apart from other languages?
Statebox is designed to be self-optimizing, open (technology agnostic), adaptive, terminating, error-cognizant, composable, and most distinctively—visual.
What makes Statebox a visual language?
Petri nets are the natural representation of decentralized computation and concurrency. By utilizing them as program models (model of computation), the entire language is diagrammatic, and this allows one to inspect the flow of the process executed by the program. The user immediately sees and understands the concrete realization of the abstract design by inspecting the visual representation in the form of Petri nets. Aside from Petri nets, most features in Statebox have a diagrammatic counterpart, so the code can be visually debugged at any level. The diagrammatics are guaranteed to be consistent with the underlying code they represent via mathematical results based on category theory.
Why are you using functional programming?
Our team is composed of functional programmers. Additionally, functional programming lends itself to preserving mathematical properties when implementing code, especially if described in terms of category theory.
How do you use Petri nets to write software?
Petri nets are used to glue “functions” together; Petri nets give “protocol” scaffolding; the transitions are then labeled by deterministic functions defining what computation runs as a consequence of firing transitions.
How is Statebox related to blockchain?
The system is structured as a P2P blockchain: asymmetric encryption is used to manage identity and sign transactions; state of the system is computed from a transaction log. The entire system is deterministic.
What types of correctness proofs does Statebox intend to use?
We plan to use state space analysis, type checking of logic programs, dependent typing * Proof of process correctness: no deadlock, liveness, etc. * Proof of function correctness: typechecking, termination guarantee, etc. * Global proofs: crypto economic equilibria * System proofs: compiler and evaluator work as advertised
Watch Josh Harvey talk about some of these properties during his presentation at the Second Statebox Summit.
What’s the difference between Statebox nets and standard Petri nets?
There is no real standard for Petri nets. Moreover, Petri nets are not done categorically which is precisely how Statebox is using them. Statebox also uses wiring diagrams of open Petri nets.
What are the advantages of Statebox over a standard finite state machine for any application?
Petri nets are the natural generalization of state machines to a concurrent framework. This means that any state machine is also a Petri net, and that the Statebox formalism is at least as powerful as state machines are. Clearly, in addition to this, Statebox performs better in environments where concurrency is needed.
On the other hand, Petri nets share with state machines the property of not being Turing-complete, a fact that should be considered as an advantage in environments where correctness is paramount: non-Turing completeness ensures program termination and makes possible to prove a series of desiderable properties for software to have. Check the monograph for more information about this.
Are there any performance issues in using Statebox for UI?
Which Statebox tools will be open source?
We are planning on open sourcing very soon. A Statebox studio will be available at the beginning on next year. It allows one to click through a process, examine the types of transitions and places, automatically generate forms for different data types, inspect the history of fired transitions and more.
Are there (business) situations which cannot be modelled with Statebox?
The most popular tool to draft business processes is BPMN (Business Process Model and Notation). There is a straightforward translation from BPMN processes to Petri nets, so everything that can be modeled using former can surely be modeled in our framework with the latter. Moreover, Petri nets offer several advantages over BPMN, the main one being that Petri nets are very well formally defined, while BPMN consists of different standards often incompatibile between each other.
Petri nets are an excellent tool to model processes, therefore they are not the best choice when applications are very simple process-wise. For example, a typical ERC20 token contract constitutes a very simple process, and albeit it can be formalized in Statebox, this would be overkill.