GoKawiilblog / structural-correctness
Type systems are great: they catch huge swaths of bugs at compile time, and contribute to a grammar/vocab of forward development for your app. Like type systems, modern tools for verifying correctness leverage structural descriptions of the problem, via graph-structured model of the domain:
Type systems describe programs as a graph of types, functions, traits/etc, and their relationships. Types are nodes, with relationships like returns , accepts , implements , etc as edges.
describe programs as a graph of types, functions, traits/etc, and their relationships. Types are nodes, with relationships like , , , etc as edges. Build systems like bazel have build targets as nodes and dependencies as edges between them. Without explicit deps stated, unstated packages are not provided to build targets even if they are built by other means, fulfilling hermiticity and trivial deployability.
like bazel have build targets as nodes and dependencies as edges between them. Without explicit deps stated, unstated packages are not provided to build targets even if they are built by other means, fulfilling hermiticity and trivial deployability. Interface description languages have messages types and services as nodes, with return types and parameter types as edges (a restricted type system).
have messages types and services as nodes, with return types and parameter types as edges (a restricted type system). Databases use foreign keys (edges) to describe the relationship between related table rows (nodes). However, databases also use check contraints to implement correctness: not structural, but useful predicates to express aspects can't can't be described additively.
STRUCTURAL CORRECTNESS Model your domain as a graph of typed nodes and edges. The best of these graphs are definitional: the structure that describes the system is the system. No edge, no capability.
Each domain has its own vocab of node and edge types. Bazel is a nice example of the richness via different edge types: deps means "link this code," srcs means "compile these files," data means "make available at runtime." Each is a different edge type in the target graph, and each constitutes a different capability. Elegant choice of node and edge types result in expressive and powerful tools. Many of these correctness tools leverage both structural correctness and predicates to describe valid configurations.
The best of these graph-structured systems are constitutive/definitional: they both define "what is valid" and "how outputs are computed". In bazel, a target can't import a module it doesn't dep end on. This provides two valuable features: a) the verifiable invariant must be stated for the system to function, so you end up with a verifiable system by default, and b) it provides a brevity in specificaiton thanks to stated attributes and relationships doing double duty for behavior and validation. Building a bazel project forces you to describe the explicit structure of your product, and leaves you with a means to verify it as you continue to develop.
These two points about "each domain has its own nounds and verbs" and "definitional graph structured systems" are why bazel is such a good substrate for describing your whole product in: Bazel lets you define arbitrary node types for your domain concepts (packages, services, datasets), constrain their relationships via typed edges, and then derive your entire build/test/deploy pipeline from that single structural description. A service, its metrics endpoint, and the Prometheus deployment that scrapes it can all be nodes in the same graph — their relationships declared once and used to compile, deploy, and verify the whole system.
... continue reading