WhippleScriptOne writer. Atomic firings.
A firing commits consumed facts, new facts, effects, and terminal state in one transaction. An instance never observes half a decision.
WhippleScript for developers
Agent workflows with actual invariants.
A typed coordination language that keeps deterministic policy separate from fallible effects—and makes authority, information flow, failure, history, and revision first-class.
review-and-release.whip
rule draft when Ticket as t when writer is available => { tell writer "Draft a fix for {{ t.id }}" with access [repo] then { askHuman choices ["ship", "hold"] "Release the reviewed patch?" } }
Execution model
Rules decide. Effects do.
Rule evaluation is deterministic and side-effect free. Agent turns, model coercions, timers, commands, human asks, messages, and child workflows become durable effects with stable idempotency keys.
Outcomes do not disappear.
Closed-domain cases must be exhaustive. Effect failures are typed; an unobserved terminal failure auto-fails instead of leaving a silent zombie.
Retries do not duplicate intent.
Effect identity includes program version, revision epoch, rule, binding path, and trigger identity. Recovery and re-evaluation dedupe against the same request.
Static boundary
What the compiler can reject.
WhippleScript does not claim general termination. It rejects specific unbounded shapes and forces the important control-flow and data-flow obligations into the program.
No recursive pattern expansion or workflow invocation cycles.
Recursive expansion and invocation graphs are rejected. Agent capacity, leases, counters, timeouts, and work-loop structure make concurrency and waiting explicit.
Declared inputs, outputs, failures, and exhaustive branches.
Fact reads and writes are checked, terminal payloads must match their contract, and finite cases cannot silently omit a variant.
A workflow must have a path to complete or fail.
The checker flags missing terminals, unsafe reads, unhandled failures, shadowed branches, and non-convergent structures. Liveness warnings stay honest where a proof is not available.
Information-flow control
IFC as denied flows, not a permission checklist.
A signed envelope labels real resources on confidentiality and integrity axes. The checker derives provenance through facts, rules, workflow boundaries, prompts, tool results, and provider context.
Source labels
Reader sets + integrity
Combining sources joins compartments. Unaccountable inputs fall back to declared labels.
→
Compiler derivation
Every read to every sink
Facts, terminals, channels, providers, child workflows, model prompts, and tool results.
→
Universal denials
Confidentiality + influence
Only source-marked, schema-bounded declassify or endorse crossings can pass a signed grant.
Version control for live work
History is data, not cleanup.
The event log is append-only. Facts are immutable and content-keyed. File bodies are content-addressed; “current state” is a fold over the lineage.
- Checkpoint a coherent cut across event, fact, transcript, and file planes
- Restore without erasing the abandoned suffix
- Fork agent threads into counterfactual branches with distinct effect keys
Revision without historical fiction
Change the program in flight.
whip revise compatibility-checks a candidate and records an activation event plus revision epoch. Existing work retains its original program version; future commits use the new one.
- Preview with dry-run
- Choose a policy for old queued or running effects
- Verify lifecycle conformance with
whip trace --check
Trust, but make it falsifiable
Formal models are in the CI path.
The published guarantees point to their carriers: Maude executable models, Lean proofs for reader-set algebra, narrowing and non-interference, and TLA+/Apalache models for lifecycle and bounded-safety properties.