A language for stating what must be true of a system, and a compiler that refuses to let you break it. Declare data, behavior, seams, and closures, and a deterministic checker proves on every keystroke that nothing reaches a sealed resource except through its gateway. Ships as a command-line compiler and a desktop IDE.
Author intent. Prove structure. Emit code.
You declare data and the invariants it holds, behavior and what it
guarantees, seams that mediate access to a resource, and closures that seal
that resource behind them. A deterministic checker then proves, structurally and
on every keystroke, that nothing reaches a sealed resource except through its
gateway.
Two surfaces over one language
weave, a command-line compiler: check a spec, view the derived graph, and emit amirror/tree of real code from it.- Weave, a desktop IDE where the same checker runs live, so a violation appears in the gutter and spatially on the graph at the instant it occurs.
The language is defined in docs/weave-language.md, which is the single source
of truth for syntax, semantics, and the checking rules.
What was interesting
Making the check structural rather than analytical. A rule that holds by construction can be proved on every keystroke; one that requires whole-program analysis cannot, and an IDE that goes red half a second late is an IDE nobody trusts.