Language Reference

The core syntax and semantics of Aura (current prototype).

Keywords

cellvalmuttypeimportifelsewhileinvariantyield

Operators

Token	Meaning	Notes
`=`	assignment	only for existing bindings
`:`	type ascription / annotation	used in bindings and signatures
`->`	flow (sync)	sequencing + capability transfer
`~>`	flow (async)	sequencing + async capability
`==`	equality	boolean result
`!=`	inequality	boolean result
`<, <=, >, >=`	comparison	boolean result
`+, -, *, /`	arithmetic	integer arithmetic (prototype)
`and, or, not`	boolean logic	(spelled out in docs/examples)

Program structure

An Aura program is a list of top-level statements. The most common entry point is a cell.

Entry point

cell name() -> Type: statements...

Why cells?

Cells are a unit of execution and verification: the compiler checks types, the verifier proves safety obligations, and the runtime evaluates the body.

AURA

cell main() -> u32:
  val x: u32 = 42
  yield x

Statements

Common statement forms

val name: Type = expr
mut name: Type = expr
name = expr
if cond: ... else: ...
while cond invariant (expr): ...
yield expr

Yield and blocks

yield returns a value from a block (and must be the last statement in that block).

Expressions

Aura supports integer and string literals, identifiers, unary/binary operators, and calls.

Member calls like model.infer(x) are lowered by the checker/verifier into well-known calls (e.g. ai.infer(model, x)), enabling proof rules.

Lowering (important for plugins)

When syntax looks like a member call, the compiler can lower it into a canonical function call so the verifier/plugin system can attach rules to a single name.

Flow operators

Aura includes a flow operator family used to model capability transfer and sequencing:

-> (sync flow)
~> (async flow)

They behave like “do left, then right”, and the verifier uses them to enforce capability rules (e.g. no unsafe reuse).

Flow sequencing

AURA

cell main() -> u32:
  val a: u32 = 1
  val b: u32 = 2
  val out: u32 = a -> b
  yield out

Types (prototype)

You’ll see these commonly:

u32, bool, string, ()
Tensor types like Tensor<u32, [2, 2, 3]>

Type aliases are supported:

AURA

type Pixels = Tensor<u32, [2,2,3]>

Imports

Imports are currently used as module placeholders (they tell the checker/verifier which namespaces are in scope):

AURA

import aura::tensor
import aura::io

See the “Stdlib, Modules, and Imports” doc for details.

Note

In the current prototype, import is also used by tooling (including the Nexus/plugin pipeline) to decide which domains are active.