Reference 01 Principles

1. Principles

Velle describes, it doesn't execute — and those are two separate phases, not one. First, make declarative statements about a system's conceptual models: shapes, relationships, rules, behaviors. That description is complete, meaningful, and self-consistent entirely on its own. Velle is then "compiled" to make runtime decisions — storage strategy, caching, mutability, execution order, data structures, traditional computer-science machinery generally. Velle's own scope stops at can this be declaratively stated; it never extends to how should this be executed. If a design question can only be answered by talking about caching, mutable-vs-immutable storage, or when a computation runs, it has strayed into the second phase and doesn't belong in this document.

"Compiling" means validating a coherent spec, not primarily building an executable. The compiler's main job is checking that shapes, relationships, and rules form a strongly-typed, self-coherent system description — producing runnable code is a possible downstream output, not the defining purpose (the same instinct already behind refinement exhaustiveness/overlap checking, ## Refinements, mapping totality checking, ## for, and the one-writer and disarm proofs, ## Assignment (mutation in place) and ## Run-once guards). This gives ambiguity a home: a construct that would resolve one way today and a different way after some unrelated, later change to the spec (a field added to some other shape, say) is a compile error, not a runtime concern or a style nit — compiling is the later event that forces a human to notice and be explicit, rather than the moment a silent, schema-dependent resolution quietly starts pointing somewhere else.

Because ambiguity can be introduced by a change anywhere in the spec, "compiling" has to mean re-validating the whole spec as one coherent unit every time, not incrementally re-checking just the file or shape that changed — a traditional compiler's file-scoped, incrementally-cached model doesn't fit here, since the whole point is catching effects at a distance (a field added to Referral invalidating a Customer refinement that never mentions the change). Velle's "compiler" is closer to a global logic/consistency checker running over the whole spec as a single knowledge base — the same category of thing as a theorem prover or constraint solver checking a whole model for coherence — than to a traditional per-file compiler, even though it also happens to be the thing that may eventually emit code.