Trying to solve the same problems using the same tools over and over again and expecting to repeatedly get different and successful results is indeed pure insanity.
It is by no means an exaggeration to think that we are entrenched in and debilitated by the same patterns of action that formed our personal and professional selves. Whether we like it or not, we, as social animals, belong to certain cultures, (whether it is the Google culture or the Rust community or whichever nation state you’re from) and it’s only human that we appropriate thoughts and behaviours from those groups. I invite you to take a step back and try to analyze things from a different perspective.
In dealing with complex systems, (and we are dealing with complex systems on a daily basis; we are, as a matter of fact, immersed in one) it is imperative that we explore novel approaches. I understand that you feel very strongly about your insert imperative programming language here, because it gets things done and it’s good enough for what it is that you are doing, even though you spend x amount of hours trying to fix bugs, making your fellow devs understand what you were trying to do or even to understand yourself what you wrote a week ago. I also understand that you dismiss visual languages because that one time 2 years ago you played with a version of insert visual language name here and it sucked because of the UI, etc. But in order to understand what Statebox is about you need to get out of your comfort zone and be willing to embrace a change of perspective.
For Statebox to come into existence, that change of perspective needed to happen. The idea of using Petri nets and category theory in an intertwined manner does not come naturally, to say the least. It is, in a sense, an unprecedented way of thinking and solving problems — which turns out to be more efficient than anything else out there. And it helps immensely with the increasing complexity of systems. Statebox is actually built for that!
Moving fast and breaking things simply doesn’t cut it anymore
Nowadays, companies tend to pitch their business models of siloed and quasi innovative problem-solving technology. The whole idea of specialization and offering solutions to particular problems has been haunting us since the time of Adam Smith. Somehow, people seem to forget that no problem arises in isolation. Do we even consider anymore that for a particular problem to come into existence, a complex web of context dependent actions need to happen? And what is the point, may I ask, of solving those problems if they will keep happening, since the source that is causing them has not been addressed? The same way we feed pesticide infested food to millions of people who end up developing health problems from it (not to mention the ecological disaster caused by growing monocrops), then develop and capitalize on medicine that treats those same health problems, the approach to writing code seems to be just as flawed. Badly written code can have deep societal consequences, as well. If someone can change the course of this, it is the developers themselves.
A case for bottom-up formal verification
To illustrate, let’s take the over-referenced example of the DAO hack. We know what went wrong with it, but somehow, after all these years, typed languages are still not used to write smart contracts. Devs are still hammering away using the usual untyped tools, while other companies come into existence promising quick fixes to patch up what goes wrong with said method. And while operational semantics and model checking serve their purpose in the current ecosystem, there is a better way. We believe using formal tools to begin with is the way to go.
Bottom-up formal verification uses category theory and type theory. It creates a solid, verified foundation on which other layers can be built. This approach is very general and reusable. And while in the beginning it is abstract and limited in functionality, it proves extremely advantageous in the long run.
This is in contrast with the usual approach to formal verification, which consists in taking a piece of software, formalizing its operational semantics using an environment like Coq, and making sure that everything is correct. The top-down approach is particularly weak to scaling, since it allows the codebase to grow in any direction, often in an unprincipled way. It’s not a mystery that producing formally verified code in this way is a very slow and expensive process.
On the contrary, relying on a strong type-system — such as those with dependent types — allows to prove properties of the software bottom-up, as the developing goes. In this setting, developing is slower, but after a given “module” has been completed its behavior will be completely known, and we will be able to compositionally plug in into a bigger structure.
The beauty of category theory
This is the beauty of category theory: it allows you to build sound, verifiable code out of little pieces of code. Statebox has built-in compositionality both within its code (which is verified bottom-up) and within its paradigm (programming with Statebox ensures a compositional bottom-up approach to verification). Moreover, since programming with Statebox is visual, it offers what is probably the easiest way to produce verified software on the market.
If you are interested in functional programming and category theory, do check out our other Medium posts and the resources on our website.
Update
The first business application of the Statebox language is being developed on process.io. Sign up for a beta trial now!
