Language Tour

Learn DEXA in about 5 minutes

This is the fast track: what DEXA looks like, what’s implemented right now, and how to read real code without digging through the compiler.

Explicit types and simple expressions.
Functions, branching, loops.
let vs let mut and scopes.
Basic models/contracts wired into the typechecker.

Under the hood: parser → typechecker → DX-IR → interpreter. No magic runtime, no hidden globals.

Example · Tiny program

fn max(a: int, b: int) -> int {
    if a > b {
        return a;
    } else {
        return b;
    }
}

fn main() -> int {
    let mut x: int = 0;
    x = max(1 + 2, 3 * 4); // 12
    return x;
}

1 · Values & types

Primitive types implemented today

int — 64-bit signed integer.
float — 64-bit floating point.
bool — true / false.
string — immutable UTF-8 string.
unit — “no value”, used when functions don’t return anything.
address — concrete address/identity type used by models and contracts.
model records — nominal record types (e.g. Wallet) with named fields.

There are no implicit coercions. In particular, converting a string into an address must be explicit via address("...").

Literals in practice

fn demo() {
    let a: int = 42;
    let pi: float = 3.1415;
    let ok: bool = true;
    let msg: string = "hello from DEXA";
    return;
}

2 · Functions & calls

Declaring functions

Functions are declared with fn. Parameters must have types, return type is optional (defaults to unit).

fn add(a: int, b: int) -> int {
    return a + b;
}

fn log(msg: string) {
    // returns unit implicitly
    return;
}

Calling functions

Calls are typechecked: arity and parameter types must match the function’s signature.

fn main() -> int {
    let x: int = add(1, 2);   // ok
    // add(true, 2);          // ❌ type error (bool vs int)
    return x;
}

3 · Branching & booleans

If / else + comparisons

Conditions must be bool. Comparisons and logical operators feed into that.

fn classify(x: int) -> bool {
    if x >= 0 && x < 10 {
        return true;
    } else {
        return false;
    }
}

Assertions with require

require is checked by the typechecker (first argument must be bool). If it’s false, execution aborts and the run returns a classified failure result.

fn main() {
    let x: int = 5;
    require(x > 0);
    require(x > 0, "x must be > 0");
    return;
}

4 · Mutability, scopes & loops

let vs let mut + shadowing

Immutability by default. You opt into mutation with mut. Inner blocks can shadow outer bindings safely.

fn main() -> int {
    let mut x: int = 10;

    if x > 5 {
        let mut x: int = 1;
        x = x + 1; // inner x
    }

    return x; // 10 (outer x)
}

Loops that actually run

while, loop, break, and continue are wired through parser → typechecker → DX-IR → interpreter.

fn main() -> int {
    let mut i: int = 0;
    let mut acc: int = 0;

    while i < 10 {
        acc = acc + i;
        i = i + 1;
    }

    require(acc == 45, "expected 45 from 0..9");

    let mut j: int = 0;
    let mut hits: int = 0;

    loop {
        if j == 3 {
            break;
        }

        hits = hits + 1;
        j = j + 1;
    }

    require(hits == 3, "loop/break broken");
    return 0;
}

5 · Models & contracts (current shape)

DEXA ships today with model — nominal record types used to represent structured data. The contract surface shown here is a design preview for the DX-VM backend: it is not implemented in the current interpreter, but illustrates how DEXA’s deterministic core maps cleanly into verifiable contract execution.

Model snapshot (implemented today)

model Encoder {
    owner: address
    weight: float
}

fn new_encoder(a: address, w: float) -> Encoder {
    return Encoder {
        owner: a,
        weight: w
    };
}

Fully implemented: nominal records, typechecked fields, and runtime record values.

Contract snapshot (future design)

contract Vault {
    asset<Token> balance

    fn withdraw(to: Address, amount: Token) {
        require(balance >= amount);
        balance -= amount;
        transfer(to, amount);
    }
}

Not implemented yet — this is a DX-VM design preview only. The asset<T> type, contract storage, and inter-contract calls will arrive in the “contract subset” milestone after the core language and execution model are fully locked in.

Shown here to illustrate how require, structured types, and deterministic execution extend naturally to verifiable smart-contract semantics.

6 · Example: wallet model + tests (runs today)

This is roughly the program the reference interpreter is running when you execute wallet.dexa main. It shows:

A nominal model Wallet with an address owner.
Pure functions new_wallet, credit, and debit.
Runtime checks with require(...) for invariants.
Three tiny “tests” that just call into your functions and assert behaviour.

If any require fails, execution stops immediately and the run returns ProgramResult::RequireFail with the failure message plus trace/gas.

Example · Safe wallet

model Wallet {
    owner: address
    balance: int
}

fn new_wallet(owner: address) -> Wallet {
    let w: Wallet = Wallet {
        owner: owner,
        balance: 0,
    };
    require(w.balance == 0, "new wallet should start at 0");
    return w;
}

fn credit(w: Wallet, amount: int) -> Wallet {
    require(amount > 0, "amount must be positive");

    let mut w2: Wallet = w;
    let new_balance: int = w2.balance + amount;

    w2 = Wallet {
        owner: w2.owner,
        balance: new_balance,
    };

    return w2;
}

fn debit(w: Wallet, amount: int) -> Wallet {
    require(amount > 0, "amount must be positive");
    require(w.balance >= amount, "insufficient funds");

    let new_balance: int = w.balance - amount;

    let w2: Wallet = Wallet {
        owner: w.owner,
        balance: new_balance,
    };

    return w2;
}

fn debug_example() {
    let w: Wallet = new_wallet(address("addr:debug"));
    let w2: Wallet = credit(w, 5);
    let w3: Wallet = debit(w2, 2);

    print("debug wallet after credit:");
    print(w2);

    print("debug wallet after debit:");
    print(w3);

    print("debug wallet final balance:");
    print(w3.balance);

    return;
}

fn test_new_wallet_zero_balance() {
    let w: Wallet = new_wallet(address("addr:test"));
    require(w.balance == 0, "new wallet should start at 0");
    return;
}

fn test_credit_increases_balance() {
    let w: Wallet = new_wallet(address("addr:test"));
    let w2: Wallet = credit(w, 10);
    require(w2.balance == 10, "credit should increase balance by amount");
    return;
}

fn test_debit_decreases_balance() {
    let w: Wallet = new_wallet(address("addr:test"));
    let w2: Wallet = credit(w, 10);
    let w3: Wallet = debit(w2, 3);
    require(w3.balance == 7, "debit should decrease balance by amount");
    return;
}

fn main() -> int {
    test_new_wallet_zero_balance();
    test_credit_increases_balance();
    test_debit_decreases_balance();
    debug_example();
    return 0;
}

What you can actually run today

Right now, DEXA’s reference implementation is an interpreter over DX-IR, with a structured result type:

Parse .dexa into an AST.
Typecheck functions, locals, models/contracts, and require calls.
Lower to DX-IR with blocks, locals, If, While, Loop, Return, calls, and records.
Interpret the IR to produce a ProgramResult instead of a bare value.

In practice this means: running main gives you the return value plus every print(...) in order, a function-level call trace, and a deterministic “steps used” count. If a require(cond, msg?) fails, execution stops immediately and you get a classified RequireFail result instead of a generic runtime error.

GPU kernels, full tensor semantics, and the DX-VM backend are next steps — this tour shows the core you can already write and reason about today, with an execution model that’s ready to be dropped onto more serious backends later.