Ramadge–Wonham as the math home for the vibe-linter
Parent: vibe-linter · Reference: ramadge-wonham-supervisory-control
RW is the precise math home for vibe-linter (better than Petri nets). "The supervisor can only disable controllable events, never force the plant" is the mathematical definition of a gatekeeper-not-driver.
The mapping:
- Test results are
Σ_u— you allow running tests, you can't control red/green. So "tests must pass" is not a controllable spec; the controllable version is "commit is disabled until green is observed." RW elevates the gate-not-command intuition to a theorem. supC(K)= synthesis: you declare the property, the linter computes the minimal lock set — the least-restrictive set of commits/actions to disable.- Partial observation = the observation surface: the supervisor sees only the projection (tool calls, not internal reasoning); any spec depending on "what the agent thought" is unexecutable. Lever:
Σ_ocan be bought larger — forcing all actions through tool calls (syscall-ization) enlarges the observation surface.