Building DEXA from the inside out

This update is about discipline: DEXA now has an explicit IR validation pass that runs after lowering and before interpretation. If the compiler pipeline ever emits inconsistent IR, it fails immediately — no “mystery runtime behaviour”, no papering over bugs.

• IR validation is a hard firewall between lowering and the interpreter.
• Validation is schema-aware via a program context (models + contracts).
• Unknown record types, unknown fields, and duplicate fields are rejected.
• RecordLit nodes must be fully materialized: every declared field is present post-lowering.
• No implicit coercions exist: string does not silently become address. You must call address("...").

The record rules are now explicit and enforced:

# Record literals (no base) are fully materialized in lowering:
model Wallet { owner: address; balance: int = 0; }

fn main() -> int {
    let w: Wallet = Wallet { owner: address("alice") };
    return w.balance; # == 0
}

Record updates are intentionally conservative in v0.x: the parser currently supports a base-only update form. Overrides are coming later, but the semantics are already guarded:

# Record update (implemented grammar today):
# Type { ..base }

model A { x: int = 0; }
model B { x: int = 0; }

fn main() -> int {
    let b: B = B { x: 1 };
    let a: A = A { ..b }; # hard error (wrong nominal type)
    return 0;
}

The validator also learned how to infer record type names from locals in the common case, not just from inline literals, so these checks don’t disappear as soon as you assign to a variable.

Net result: fewer “cool features” on the surface, but much stronger guarantees underneath. This is the kind of boring work that keeps a language from turning into a haunted house later.

The interpreter now returns something more honest than “here’s an int, good luck”. The runtime has grown a real execution model: every run of main produces a structured ProgramResult with the final value, captured prints, a call trace, and a gas-like step counter.

ProgramResult::Ok {
    value: Value,
    prints: Vec<String>,
    trace: ExecutionTrace,
    gas: GasMeter,
}

ProgramResult::RequireFail {
    message: String,
    trace: ExecutionTrace,
    gas: GasMeter,
}

• value is whatever main returns: int, bool, a record, or unit.
• prints is a vector of strings produced by print(expr) in order. The interpreter never writes directly to stdout; hosts decide how to surface it.
• trace records function entries (e.g. main → transfer → debit) so failures and weird behaviour have a concrete path attached.
• gas is a simple step counter that increments for every statement, expression, and function entry. It’s not a fee model yet, just a deterministic “how much work did this run do?” number.

require(cond, msg?) is now classified instead of being “just another runtime error”. When the condition is false, execution aborts immediately and the interpreter returns ProgramResult::RequireFail with the message, plus the trace/gas accumulated so far. When it’s true, require is a no-op that evaluates to unit.

fn main() -> int {
    require(balance > 0, "balance must be positive");
    print(balance);
    return balance;
}

At the spec level this locks in a contract: “same source, same ProgramResult for a given input”. Future backends (DX-VM, GPU, whatever) have to uphold that, so this interpreter becomes the semantic oracle.

There are also new tests around traces and gas: checking that main shows up in the trace, nested calls appear in order, and “heavier” programs consume more steps than trivial ones. It’s not glamorous work, but this is the layer everything else is going to stand on.

The core runtime finally understands something more interesting than raw ints and floats. This drop adds nominal records, a first-class address type, and a tiny wallet example that runs end-to-end through DX-IR.

• Runtime values grew a Record variant with a nominal type_name and field map.
• Everything implements Display, so print doesn’t just dump Debug noise anymore.
• address exists as a real type at runtime, with a small coercion from string when binding params / locals.
• A Wallet model plus new_wallet, credit, and debit functions serve as the canonical “safe state update” example.
• Three tiny test-style functions assert the behaviour of the wallet using require, and main just runs them.

The current reference sample looks like this:

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 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;
}

To run this from the repo root right now:

cargo run -- examples/wallet.dexa

The tour page now shows this program directly, so the website and the interpreter stop lying about what the language can actually do.

The core language finally behaves like something you can reason about over time: structured loops, typechecked models/contracts, and error messages that don’t feel like a slap in the dark.

• while, loop, break, continue wired end-to-end (parser → typechecker → IR → interpreter).
• Model and contract bodies are now typechecked — bad field types are rejected.
• Parser and typechecker errors include line/column and a caret, e.g. error at 5:11: expected '{{' (found Colon).
• Negative tests like bad_parse.dexa, bad_type.dexa, and bad_model.dexa drive the shape of the diagnostics.

The canonical “does this even work?” sample right now is a tiny loop harness:

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;
}

On top of this, models/contracts get their own typechecked bodies — you can’t sneak an int into a field that declared as bool anymore without the compiler yelling.

The compiler finally grew up a bit. Locals aren’t just nameless slots hanging off an AST anymore — they live in real scopes, can be let or let mut, and lower into a small IR the interpreter can actually execute.

• let mut support with type-checked assignments.
• Block-scoped locals with shadowing inside if blocks and nested blocks.
• Assignments lower to IR Store ops instead of hacky rewrites.
• Interpreter now runs against DX-IR, not the AST, which keeps future backends sane.

The following program runs end-to-end and demonstrates let mut, shadowing, and the IR interpreter:

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

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

    return x;
}

This returns 10 from the outer x. The inner x is a separate binding that lives and dies inside the if block — which is exactly what you want before you start doing anything serious with state.

The first version of the DEXA site talked a big game about AI, smart contracts and deterministic compute. Underneath, the compiler was basically a parser that printed ASTs. Cute, but useless.

The last few iterations turned DEXA into an actual language core:

• Structured AST for functions, blocks, if / else, and expressions.
• A typechecker that understands int, bool, float, string, and unit.
• Function signatures, argument typechecking, and return type validation.
• let vs let mut with enforced immutability.
• Block scopes + shadowing (inner x can hide outer x safely).
• IR and an interpreter that can actually execute simple programs and produce a value.

Example of what currently runs end-to-end:

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;
}

The CLI is still intentionally minimal:

cargo run -- ../examples/hello.dexa

Next steps: extend the type system toward tensors and asset types, and start mapping this IR to a verifiable VM instead of just an in-process interpreter.