Thirsty-Langv0.9.0 Overview Features Status Security Proof Releases Install Specification Grammar Playground

Specification · v0.9.0

Language reference

A reference for the portal teaching subset: core/governed modules, contracts, and sample policies. The pinned UTF 101 manual is the complete release reference, including context normalization, language types, and runtime boundaries.

Evaluation model

1. A program declares a module in core (ordinary runtime) or governed mode.
2. Governed functions (glass) carry requires / ensures contracts, checked around the call. A failed precondition refuses the call before the body runs.
3. A policy (T.A.R.L.) is first-match-wins: when conditions map to policy dispositions ALLOW, DENY, or ESCALATE. End with when true => DENY.
4. No matching rule, missing policy, or a failed contract resolves to DENY — deny-by-default.
5. Every run emits a deterministic decision hash and an ordered audit trace.

Keywords

Declarations

module

Declares a module and its execution mode: `core` (ordinary runtime) or `governed` (contracts + policy before effects).

module bank: governed

glass

Declares a function. May carry `requires`/`ensures` contracts that are enforced around the call.

glass withdraw(amt) requires amt > 0 { return amt }

drink

Binds a value into scope.

drink balance = 100

fountain

Declares a class (Tier 2 — Thirst of Gods). Full OOP surface in the toolchain.

fountain Counter { drink count: Int = 0 }

Control

pour

Outputs a value through the runtime.

pour "hello, thirsty world!"

requires

Precondition contract on a `glass`. If it fails, the governed call is refused before the body runs.

glass f(x) requires x > 0 { ... }

ensures

Postcondition contract. `result` is bound; if it fails, the result is inadmissible.

glass f(x) ensures result >= 0 { ... }

invariant

An invariant that must hold across an operation. Turns governance into an executable check.

invariant balance >= 0

policy / when

A T.A.R.L. policy: first-match-wins rules mapping conditions to policy dispositions. End with `when true => DENY`.

policy access
when role == "admin" => ALLOW

Policy dispositions

ALLOW

The policy admits the request to the next governance gate. It does not by itself produce a terminal execution ALLOW.

when user.role == "admin" => ALLOW

DENY

Fail-closed policy refusal. The default current: no policy, authority, or proof means DENY.

when true => DENY

ESCALATE

Hold execution and route to an adjudication or approval path. ESCALATE is not a terminal execution verdict.

when action == "delete" => ESCALATE

Operators

and / or / not / in

Boolean and membership operators. `and`/`or`/`not` alias `&& || !`; `in` tests list membership.

when user.ip in blacklist => DENY

Literals

true / false / null

Literal values.

drink ready = true

Governance context

Programs evaluate against a pre-seeded context. These variables model the runtime conditions a governance kernel would supply. Override any of them with let to explore different scenarios.

Field	Type	Meaning
user.role	string	Role of the acting principal (e.g. admin, member).
user.ip	string	Source address; often matched against a blacklist.
action	string	The requested action (read, write, delete, …).
resource	string	Target the action operates on.
authority	string	Proven authority claim (signed in hardened mode).
risk	number	Optional risk score used by risk-aware rules.

Policy dispositions

These are T.A.R.L. evaluation results. They are distinct from the runtime's terminal execution verdicts: ALLOW, DENY, and SAFE_HALT.

ALLOW

Policy admits the request to the next governance gate. It is not a terminal execution ALLOW by itself.

DENY

Fail-closed. No policy, authority, or proof — or a failed contract — means the action is refused. The default current.

ESCALATE

Hold execution and route to adjudication or approval. No effect is permitted while this disposition remains unresolved.