Preoscript · a language growing inside the two-phones library

Promises,
priced.

The two-phones library maps which promises survive two devices meeting, and prices the exits when they can't. Preoscript is the language where you write such promises · and the compiler holds you to the physics. It is easiest to define by the three things it refuses to let you say.

Refusal one: stable against what?

"This value is final" is not a sentence in preoscript. Final against delivery of what was already sent? Against new writers? Against a roster change? A stability claim must name the future it is stable against, and the certificate that proves it is indexed by that exact future · a certificate for another future or world does not typecheck. Evidence cannot escape the scope it was earned in and be quietly reused somewhere braver.

Refusal two: no fork collapsed by accident.

When two replicas produce genuinely different answers, downstream code that renders one of them as "the" answer does not compile. But "you cannot silently collapse a fork" never means "you cannot pick." The enforceable property is narrower and sharper:

No branch selection occurs through an implicit coercion.

Resolution is explicit and retained in the type: resolve verdict by era_order yields ResolvedBy EraOrder Claim · the value carries the policy that chose it, and, where disclosure rules allow, the alternatives it suppressed. A branch can be chosen. It cannot be chosen invisibly.

Refusal three: optimism about cost.

Coordination has a price, and preoscript treats the two directions of a budget check as different kinds of evidence. A semantic lower bound can reject a budget: no plan preserving this promise fits under that ceiling. But nothing short of a witnessed plan with a proved cost can accept one · a floor or a bare number alone cannot accept the budget. The compiler is not allowed to be optimistic on your behalf, and there are theorems in the tree that refuse exactly that: acceptance cannot be derived from a crossing count or a peer-meeting floor.

The tree is honest about the boundary, in its own ledger: the unrestricted "floor" of a workload is not a function · a ForcedFloor is a forced floor, witnessed by one decomposition, never "the" supremum. What ships instead is an executable finite contract: over an explicitly supplied universe of decompositions, the checker returns an achieved maximum with a proof no listed decomposition beats it, an exhaustive proof that none is valid, or an over-cap refusal that states exactly what it would have had to search. Reading any of those as the unrestricted floor is the scope error the types exist to prevent.

The receipts.

The quickstart is executable today, and it is deliberately explicit · one checked term at every stage:

preo_program Journey            · binds app state to a typed schema; queries, holes,
                                  and analyses all come from this one checked term
QueryFuture                     · names WHICH future the question is asked against
preo_certificate QueryCertificate
                                · indexed by that exact future · any other refuses
preo_plan JourneyPlan           · searches a capped, authored action universe;
                                  retains the selected plan's proof
preo_budget JourneyBudget      · consumes the plan's ProfileUpperBound ·
                                  a floor or a number alone cannot accept

From there the program's rows are assembled into a canonical binary artifact through checked additions only, and the claim doesn't stop at "serialization exists": v3_bytes_reopen_exact proves the canonical bytes decode back to exactly the term you wrote, and v3_bytes_executable_exact proves the stack-safe emitted bytes equal those canonical bytes. Inspection tools read any frame or journal back. The language ships its own receipts.

Budgets, when they arrive at acceptance, are pointwise over five separate currencies rather than one number · because a peer barrier, an arbiter cut, a round, a rollback, and a user prompt are not the same coin, and a deployment that fears rollback should not be forced to share a scalar with one that fears meetings.

How it got its type system.

The core design was reshaped in public correspondence. An external reviewer read the first memo and returned a verdict · the design had crossed the line into being language-worthy · followed by a counterexample that rebuilt its center. The draft had a scalar coordination grade: a session costs n meetings. But minimizing after composing is not composing the minimums:

min_σ(c₁(σ) + c₂(σ)) ≠ min_σ c₁(σ) + min_σ c₂(σ)

Each stream alone might have a seam that frees it, while no single seam frees both · so a scalar undercounts precisely when components share a strategy. The repair became the language's spine: type obligations, not counts. A declaration carries what it demands · frontiers, seals, certificates, strategy variables · and the number is a projection computed after composition, when the shared choices are actually known. The count is an interpretation of the object. It is not the object's type.