Type systems are great: they catch huge swaths of bugs quickly at compile time, and contribute to a grammar/vocab of forward development for your app. Like type systems, modern tools for correctness verification leverage structural description of the problem domain, via additive and subtractive rules:
- Type systems make data shape and interface structural, catching value errors and null pointers.
- Build systems (like bazel) make build dependency structural via default hermeticity.
- Interface description languages like protobuf make system interfaces cross-language properties by tightly coupling across languages via generated code.
- Database constraints like foreign keys and check constraints enforce properties regardless of data and schema changes.
- Benchmarks and load simulators assert on the performance properties of a system (e.g. only things that allow perf to be above this level are allowed).
A useful distinction emerges here between additive and subtractive verification tools: Additive tools are default-deny, allowing you to describe specifics that are allowed. Imagine the rust type system: no program is valid until types and interfaces are declared that allow it to be correct. Subtractive tools are default-allow, allowing you to carve out rules that are disallowed. Imagine a database check constraint: all data operations are allowed except for those that don't pass the check.
For the best of the additive tools, the declaration is the functional description, and enables the primary functioning of the system. For example, describing bazel targets and deps is both a) what allows you to reproducibly build your monorepo, and b) is what makes verification work: if you don't declare a dep, its not available and the build fails. The best codebases are able to leverage additive tools for most verification, and are able to leverage subtractive tools for the rest (through this lens, unit tests actually look pretty bad). Engineers can move fast because they can be confident that any problems they introduce will be caught by their correctness tools
But what about state?
Commonly, some state verifications are implemented in the database via check constraints, and yet more are implemented in application logic via ORMs/data layers. Because these verification tools are subractive, making state bullet proof with them always feels laborious and incomplete. The inherently subtractive checks only cover the things you remember to specify, which is essentially never enough.
Colored Petri Nets (CPNs) do something interesting here, making state transitions structural along with state data types. Said another way, no data changes are allowed outside of explicitly stated and well defined transitions, each with a set of bound tokens matching specific preconditions, and producing specific tokens to specific output places. It's via explicit transitions that, like bazel, CPNs manage to land in the ideal "additive structural and functional description" sweet spot.
Personally, I'm bullish on this unification of state and transition: databases generally only handle the data + type side of this plus subtractive tools like check contraints and row level security. CPNs could be the substrate we describe our apps in: state, transitions, authorization, and coordination unified in one additive artifact — where today those concerns are scattered across application code, database constraints, and middleware, each verified separately and incompletely.
As a new domain there's a lot of learning ahead about what kinds of bugs could emerge from these systems, or what kind of operations and performance trade-offs need to be made. Type systems are famously not-free. But I see an even larger amount of opportunity to go with it.