The Mathematical Specification of the Statebox Language
Statebox Team: Fabrizio Genovese, Jelle Herold

TL;DR
This paper provides a rigorous mathematical foundation for the Statebox programming language, ensuring its consistency and correctness by formally tying together various theoretical structures.
Contribution
It introduces a formal mathematical specification that underpins the Statebox language, enhancing its reliability and facilitating auditing and understanding.
Findings
Mathematical framework ensures language consistency
Formal specification guides implementation process
Supports auditing and verification of the language
Abstract
This document defines the mathematical backbone of the Statebox programming language. In the simplest way possible, Statebox can be seen as a clever way to tie together different theoretical structures to maximize their benefits and limit their downsides. Since consistency and correctness are central requisites for our language, it became clear from the beginning that such tying could not be achieved by just hacking together different pieces of code representing implementations of the structures we wanted to leverage: Rigorous mathematics is employed to ensure both conceptual consistency of the language and reliability of the code itself. The mathematics presented here is what guided the implementation process, and we deemed very useful to release it to the public to help people wanting to audit our work to better understand the code itself.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Radiation Effects in Electronics · Distributed systems and fault tolerance
