The closed circuit
Every interaction is a loop from an event back to the screen, and the compiler checks every edge of it.
Every Orb program runs one loop:
Event → Guard → Transition → Effects → UI → EventAn event arrives. If the current state has a transition for it and its guard holds, the transition fires, its effects run in order, the screen redraws, and the new screen offers the next events. Nothing else moves the program.
Walk one step
In this checkout an order starts unpaid. PAY is accepted only when the amount is positive; there is no SHIP out of pending, so an unpaid order cannot ship. That is not a check someone remembered to write; it is the shape of the program.
Checkout
on Order · states: 3 · transitions: 4Unpaid
The same trait as a state machine: each box is a state, each arrow an event that moves it, and the icons on an arrow are the effects that event runs. Hover a symbol to see what it does. How to read AVL
1app std-orb-sample-checkout "1.0.0"
2"std-orb-sample-checkout — the checkout program shown on orb.almadar.io's home page, running: an order that cannot ship before it is paid. The page shows this file as code beside the running trait, and each move is reported (MOVED) so its state machine can follow along."
3orbital Orders {
4 entity Order [runtime] {
5 id : string!
6 total : number
7 }
8
9 trait Checkout -> Order [interaction, instance] {
10 initial: pending
11
12 state pending {
13 INIT -> pending
14 (render-ui main { type: stack, gap: sm, children: [
15 { type: typography, content: "Unpaid", variant: h4 },
16 { type: button, label: "Pay 40", action: PAY, actionPayload: { amount: 40 } }
17 ] })
18 PAY -> paid when (> ?amount 0)
19 (set @entity.total ?amount)
20 (emit MOVED { event: "PAY" })
21 (render-ui main { type: stack, gap: sm, children: [
22 { type: typography, content: "Paid 40", variant: h4 },
23 { type: button, label: "Ship", action: SHIP }
24 ] })
25 }
26
27 state paid {
28 SHIP -> shipped
29 (emit MOVED { event: "SHIP" })
30 (render-ui main { type: stack, gap: sm, children: [
31 { type: typography, content: "Shipped", variant: h4 },
32 { type: button, label: "New order", action: NEW_ORDER }
33 ] })
34 }
35
36 state shipped {
37 NEW_ORDER -> pending
38 (emit MOVED { event: "NEW_ORDER" })
39 (render-ui main { type: stack, gap: sm, children: [
40 { type: typography, content: "Unpaid", variant: h4 },
41 { type: button, label: "Pay 40", action: PAY, actionPayload: { amount: 40 } }
42 ] })
43 }
44
45 emits {
46 PAY {
47 amount : number!
48 }
49 MOVED -> external {
50 event : string!
51 }
52 @description "Each move names the event it took, so a diagram beside the order can follow it."
53 }
54 }
55
56 page "/checkout" -> Checkout
57}What happens when PAY fires:
→
paid(> @payload.amount 0)(set @entity.total @payload.amount)What the compiler checks
Because every edge is declared, orb validate can prove the loop closes:
- Every affordance leads somewhere. A button whose event no state accepts is an error.
- Every state can be left, unless it is meant to be the end, and every state can be reached.
- Every emitted event is heard. An external event with no listener is reported.
- Every overlay is cleared. A modal opened in a state must be closed on every way out of it.
- Every page renders something and every page can be reached.
- Payloads match. An event read as
?amountmust declareamount, with the right type.
The bar is 0 errors and 0 warnings. A warning is a finding, not a floor.
Then verify
Validation proves the program is well formed. orb verify proves it does what it says: it plays every transition, checks the state it lands in, the effects it runs and the screen it draws, and fails on dead affordances and mutations that never persist.
orb verify checkout.lolo
orb verify checkout.lolo --trait Checkout
orb verify checkout.lolo --all--all runs the same circuit in three engines (the Rust kernel, the JavaScript runtime and the compiled app) so they cannot drift apart.
Next
The validation reference lists the checks by code. Composition shows how to reuse whole circuits.
Orb
The language where the rule is the program.