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 (interpreter level).
unit — “no value”, used when functions don’t return anything.

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 a builtin checked by the typechecker: the first argument must be bool. If it’s false, the program aborts.

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)

The long-term pitch is “one language for models and contracts”. The compiler already knows about model and contract declarations and typechecks their fields and bodies.

Model snapshot

model Encoder {
    flag debug: bool = false

    fn encode(x: int) -> int {
        if debug {
            require(x >= 0, "x must be >= 0");
        }
        return x + 1;
    }
}

Bad field initialisers (e.g. debug: bool = 1) are rejected at typecheck time.

Contract snapshot

contract Vault {
    asset<Token> balance

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

Asset semantics and full DX-VM behaviour are still evolving, but the syntax and typechecking rules are being defined now.

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, the interpreter stops with a clear error like require failed: insufficient funds.

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("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("addr:test");
    require(w.balance == 0, "new wallet should start at 0");
    return;
}

fn test_credit_increases_balance() {
    let w: Wallet = new_wallet("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("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:

Parse .dexa into an AST.
Typecheck functions, locals, models, contracts, and require calls.
Lower to DX-IR with blocks, locals, Let, Store, If, While, Loop, Return, and calls.
Interpret the IR to produce a value (int, float, bool, unit, or a Wallet record printed via print).

GPU kernels, full tensor semantics, and the DX-VM backend are next steps — the point of this tour is the core you can already write and reason about.