Language

Systems syntax designed to carry correctness intent.

Aura’s current language surface combines significant indentation, `cell` declarations, contracts, refinements, explicit trust boundaries and resource-sensitive rules. This page describes what is implemented/reference-backed today — not a hypothetical frozen 1.0 grammar.

Small example

Contracts live beside code.

cell bounded_inc(x: u32[0..99]) -> u32:
    requires x < 100
    ensures result <= 100

    val next: u32 = x + 1
    assert next <= 100
    next

Precedence

When documents disagree, code wins.

Aura already has historical design and milestone documents with syntax that can run ahead of the compiler. Public language documentation therefore follows a strict order: current implementation → compact SDK reference → focused current verifier/protocol docs → historical design material.

Normative snapshot

Current surface

The language you can reason about today.

The compact public surface is intentionally conservative. That is a feature for a pre-stable language: examples should teach syntax the repository can defend.

val · val mut

Bindings

Immutable and mutable value bindings with optional/explicit type information where supported.

cell · extern cell · trusted extern cell

Cells

Functions plus explicit foreign-code boundaries and deliberate trust annotations.

if · match · while

Control flow

Core control-flow forms with proof-oriented loop annotations.

u32 · bool · String · Unit · Tensor · Model · Style

Current built-ins

A current snapshot, not a frozen 1.0 type-system promise.

u32[0..100]

Refinements

Range constraints are available as verifier-visible type information.

layout: · render:

UI syntax

Current reference-backed application syntax used by the evolving Lumina layer.

Proof vocabulary

Correctness constructs stay close to the statement they constrain.

Contracts

requires · ensures · assert · assume

Correctness intent is visible at boundaries and inside functions.

Refinements

u32[0..100]

Range information can participate directly in proof obligations.

Loop reasoning

invariant · decreases

Loops can expose inductive invariants and termination-oriented hints.

Explicit trust

unsafe: · trusted extern cell

Foreign code is placed inside a visible trust boundary rather than hidden.

Flow

-> · ~>

The current reference distinguishes synchronous and asynchronous flow operators.

Resource semantics

Tensor · Model · Style

Current MVP rules describe move behavior for resource-like values.

Resources

Move-oriented rules exist without pretending Aura is Rust.

The current reference describes move behavior for resource-like values such as Tensor, Model and Style. The codebase also contains broader ownership, move-tracking, capability and linear-type infrastructure. Until those converge into a stable normative spec, the website separates implemented analysis from stable language guarantees.

Foreign code

Trust must be visible.

extern cell native_read(fd: u32) -> u32
trusted extern cell audited_clock() -> u32

unsafe:
    native_read(fd)

An untrusted foreign call requires an explicit `unsafe:` boundary in the current model. A trusted extern means the project accepts that implementation into its trusted base — it does not mean Aura proved it.

The language guide is conservative on purpose.

Pre-stable languages earn trust by distinguishing what exists from what is merely designed.

Read the reference