Types

Quick Reference

Postfix builders: you can apply ? , array [...] , and type application ( ... ) to base types where applicable.

Nominal & Parameterized Types

Structs and enums define named (nominal) types. They may take type parameters and, as the language evolves, const parameters . Use ordinary type application:

Reference Types

&T is a borrowed reference to T . In Aela, the mut keyword isn't part of a type; it's a marker on a parameter or call argument that grants temporary, mutable access (a "mutable loan") to a value.

• Mutable vs immutable is governed by parameter modifiers ( mut ) and aliasing rules enforced by the analyzer (no shared mutability without atomics).
• Think of &T as a view ; the underlying ownership model is enforced by the compiler.

This declares: "This function requires a mutable loan for param. I intend to modify the original value that the caller passes."

This declares: "I am granting a mutable loan to foo for this function call. I am aware that foo may modify it."

This design makes it explicit at both the function's definition site and the call site exactly where a value is allowed to be changed, aligning with the "in-out parameter" model many developers are familiar with.

Operators

Literals

Literals are notations for representing fixed values directly in source code. Aela supports a rich set of literals for primitive and aggregate data types.

Numeric Literals

Numeric literals represent number values. They can be integers or floating-point numbers and can include type suffixes and numeric separators for readability.

Integer Literals

Integer literals represent whole numbers. They can be specified in decimal or hexadecimal format.

Decimal: Standard base-10 numbers (e.g., `123`, `42`, `1000`). Hexadecimal: Base-16 numbers, prefixed with 0x (e.g., 0xFF , 0xdeadbeef ). Numeric Separator: * The underscore _ can be used to improve readability in long numbers (e.g., 1_000_000 , 0xDE_AD_BE_EF ).

By default, an integer literal is of type i32 . You can specify a different integer type using a suffix.

Example:

Floating-Point Literals

Floating-point literals represent numbers with a fractional component.

Decimal Notation: `3.14`, `0.001`, `1.0` Scientific Notation: 1.5e10 ( 1.5 × 10¹⁰ ), 2.5e-3 ( 2.5 × 10⁻³ ) Numeric Separator: * _ can be used in integer or fractional parts (e.g., 1_234.567_890 )

By default, a floating-point literal is of type f64 .

Example:

Duration Literals

Duration literals represent a span of time and are of the first-class Duration type. They are formed by an integer or floating-point literal followed by a unit suffix.

Example:

Boolean Literals

Boolean literals represent truth values and are of type bool .

`true`: Represents logical truth. false : Represents logical falsehood.

Example:

Character Literals

A character literal represents a single Unicode scalar value (stored as a u32 ). Enclosed in single quotes ( ' ).

Example:

String Literals

String literals represent sequences of characters and are of type string . Aela supports two forms:

Single-Line Strings

Enclosed in double quotes ( " ). Support escape sequences:

`\n` newline \r carriage return `\t` tab \\ backslash * \" double quote

Example:

Multi-Line Strings

Enclosed in backticks (` ` ). These are *raw*: preserve all whitespace and newlines. Only \` (escaped backtick) and \\\` (escaped backslash) are special.

Example:

Aggregate Literals

Aggregate literals create container values like arrays and structs.

Array Literals

A comma-separated list inside [] . Elements must share a compatible type. Empty arrays require a type annotation.

Example:

Struct Literals

Create a struct instance with {} .

Named Struct Literal: Prefix with the struct type. Field Shorthand: Use x instead of x: x . Spread Operator: * Use ... to copy fields from another struct.

Example:

All Literals in Action

Flow Control

This document covers all flow control constructs in Aela, including conditionals, loops, and matching.

1. if / else

Syntax

Description

Standard conditional branching. if statements have two primary forms:

Boolean Condition: The standard form evaluates a which must result in a bool. If true, the then_statement (usually a block) is executed. If false, the optional else_statement is executed.

Pattern-Match Binding (if-let): This form attempts to match the result of against the given .

If the match is successful, any variables bound in the are introduced, and the then_block is executed. These new variables are only in scope inside this block.

If the match is unsuccessful, the else statement is executed.

2. while Loop

Syntax

Description

Loops as long as the condition evaluates to true .

Example

3. for Loop

Syntax

Description

Iterates over a collection or generator. Declarations must bind variables with types.

Example

4. match

Aela supports two distinct forms of `match` :

1. Statement `match` — used for control flow and side effects
2. Expression `match` — used to compute a value

Which form you get is determined syntactically , not by context.

4.1 Statement match

A statement `match` is used for control flow. Each arm executes a block of statements and does not produce a value.

Block arms `{ ... }` are allowed return , break , and side effects are allowed * The match itself has no value

This form is typically used for branching logic, validation, logging, or early returns.

4.2 Expression match

An expression `match` computes a value.

• Each arm must be a single expression
• Block bodies `{ ... }` are not allowed
• The match must be exhaustive
• All arm expressions must unify to a single type

This restriction avoids implicit returns, ambiguous control flow, and complex typing rules.

Note

Block arms are not allowed in expression-matches!

Instead, move side effects outside the expression match.

In Aela, blocks are statements , not expressions. A block does not produce a value unless explicitly used as part of a language construct that allows expressions. The reason for this is, we optimize for explicitness, predictability, and bounded complexity. It separates control flow from value computation .

• Statement `match` - control flow, blocks, side effects
• Expression `match` - values only, expressions only

NOTE

No implicit block return or tail-values. No semicolon footguns.

This creates a well-known class of bugs:

• missing semicolon changes semantics
• especially dangerous for JS/C-family programmers
• hard to spot in reviews

Aela eliminates an entire class of bugs here:

• blocks never yield values
• expressions yield values
• the grammar enforces the distinction

Instead of a lint rule its a language guarantee. You don't need a never type. And it keeps things easier to learn.

4.3 Struct Literals in Expression Matches

Brace syntax { ... } is still allowed in expression matches when it is a struct literal, not a block.

If a brace body does not form a valid struct literal, it is rejected with an error.

4.4 Summary

5. return

Aela requires explicit `return` statements for all function exits. Functions do not implicitly return the value of their final expression. This is an intentional design choice that prioritizes clarity and predictability over implicit behavior.

Syntax

Examples

Description

Exits a function immediately with the return value perscribed by the function signature.

Function boundaries are explicit

Requiring return makes it immediately obvious where a function exits and what value is returned. This is especially important in functions with multiple branches or early exits.

There is no ambiguity about what value leaves the function.

Avoids semicolon-sensitive behavior

In expression-oriented languages, a missing semicolon can silently change behavior: Aela avoids this entire class of bugs by never treating the final expression of a function as an implicit return.

Prevents accidental returns

Without implicit returns, writing an expression at the end of a function body does not change control flow: This makes accidental returns impossible and forces intent to be explicit.

4. Keeps return semantics simple and consistent

In Aela, return always means "Exit the current function immediately!" It's never overloaded to mean...

• return from a block
• yield from a match arm
• produce the value of an expression

This simplicity avoids subtle interactions with pattern matching, block structure, and type inference.

Summary

6. break

Syntax

Description

Terminates the nearest enclosing loop.

7. continue

Syntax

Description

Skips to the next iteration of the nearest enclosing loop.

8. Blocks and Statement Composition

Syntax

Description

A block groups multiple statements into a single compound statement. Used for control flow bodies.

NOTE

Blocks never yield implicit values!

Example

9. Expression Statements

Syntax

Description

Evaluates an expression for side effects. Common for function calls or assignments.

Example

Optional

The Optional type provide a safe and explicit way to handle values that may or may not be present. Instead of using special values like null or -1 which can lead to runtime errors, Aela uses the Option type to wrap a potential value. The compiler will then enforce checks to ensure you handle the "empty" case safely.

Declaring an Optional Type

You can declare a variable or field as optional using two equivalent syntaxes:

1. The `?` Suffix (Recommended) : This is the preferred, idiomatic syntax.
2. It's a concise way to mark a type as optional.

1. The `Option(T)` Syntax : This is the formal, nominal type. The T?
2. syntax is simply sugar for this. It can be useful in complex, nested type
3. signatures for clarity.

Creating Optional Values

An optional variable can be in one of two states: it either contains a value, or it's empty. You use the Some and None keywords to create these states.

None : The Empty State

The None keyword represents the absence of a value. You can assign it to any optional variable, and the compiler will infer the correct type from the context.

To create an optional that contains a value, you wrap the value with the Some constructor.

The Optional-Coalescing Operator (??) (For Defaults)

This is the best way to unwrap an optional by providing a fallback value to use if the optional is None. The term "coalesce" means to merge or come together; this operator coalesces the optional's potential value and the default value into a single, guaranteed, non-optional result.

Using Optional Values

Aela provides mechanisms to safely work with optional values, preventing you from accidentally using an empty value as if it contained something.

Optional Chaining (?.)

The primary way to access members of an optional struct is with the optional chaining operator, ?.. If the optional is None, the entire expression short-circuits and evaluates to None. If it contains a value, the member access proceeds.

The result of an optional chain is always another optional.

Explicit Checking (Match Statement)

Use match statements to explicitly handle the Some and None cases, allowing you to unwrap the value and perform more complex logic.

Optionals & None vs. Void

• T? means maybe a `T` . Use match , ?. , or ?? to handle absence.
• none / null is the empty value that inhabits optional types.
• void means no value is returned (a function that completes for effects only). It is not the same as none .

Mutability

Aela enforces safety and clarity by requiring that any function intending to modify data must be explicitly marked. This prevents accidental changes and makes code easier to reason about. This is achieved through the mut keyword.

The Principle: Safe by Default

In Aela, all function parameters are immutable (read-only) by default. When you pass a variable to a function, you are providing a read-only view of it.

Granting Permission to Mutate

To allow a function to modify a parameter, you must use the mut keyword in two places:

1. The Function Definition: To declare that the function requires mutable
2. access.
3. The Call Site: To explicitly acknowledge that you are passing a variable
4. to be changed.

This two-part system makes mutation a clear and intentional act.

In the Function Definition

Prefix the parameter you want to make mutable with mut . This is the function's "contract," stating its intent to modify the argument.

At the Call Site

When you call a function that expects a mutable parameter, you must also prefix the argument with mut . This confirms you understand the variable will be modified.

The compiler will produce an error if you try to pass a mutable argument without the mut keyword, or if you try to pass an immutable ( let ) variable to a function that expects a mutable one. This ensures there are no surprises about where your data can be changed.

Errors

Errors are simple, the verifier runs the check borrows and the life-times of variables and properties.

Structs, Impl Blocks, and Memory Layout

struct Declarations: The Data Blueprint

A struct defines a composite data type. Its sole purpose is to describe the memory layout of a collection of named fields. Structs contain ONLY data members.

Syntax

Example

Defines a type named 'Packet' that holds a sequence number, a size, and a single-byte flag.

impl Blocks: Attaching Behavior

An impl (implementation) block associates functions with an existing struct type. These functions are called methods. The impl block does NOT alter the struct's memory layout or size.

Details

• Methods are private by default. To allow a method or constructor to be called from another module, it must be marked with the public keyword.
• The fn constructor is a special function that initializes the struct's memory. It is called when using the new keyword.
• Methods are regular functions that receive a reference to an instance of the struct as their first parameter, named self.
• Self (capital 'S') is a type alias for the struct being implemented.
• Multiple impl blocks can exist for the same struct. The compiler merges them.

Example

Memory Layout and Padding

Aela adopts C-style struct memory layout rules, including padding and alignment, to ensure efficient memory access and ABI compatibility.

1. Sequential Layout: Fields are laid out in memory in the exact
2. order they are declared in the struct definition.

1. Alignment: Each field is aligned to a memory address that is a
2. multiple of its own size (or the platform's word size for larger
3. types). The compiler inserts unused "padding" bytes to enforce this.

1. Struct Padding: The total size of the struct itself is padded to be a
2. multiple of the alignment of its largest member. This ensures that
3. in an array of structs, every element is properly aligned.

Rules:

Visual Layout (on a typical 64-bit system):

TOTAL SIZE: 8 bytes

Heap vs. Stack Allocation

Aela supports both heap and stack allocation for structs, giving the programmer control over memory management and performance.

Stack allocation (Default for local variables):

• How: A struct is allocated on the stack by declaring a variable of
• the struct type and initializing it with a struct literal. The new
• keyword is NOT used.
• Lifetime: The memory is valid only within the scope where it is
• declared (e.g., inside a function). It is automatically reclaimed
• when the scope is exited.
• Performance: Extremely fast. Allocation and deallocation are nearly
• instant, involving only minor adjustments to the stack pointer.

Heap Allocation (Explicit):

• How: A struct is allocated on the heap using the new keyword, which
• returns a reference ( & ) to the object.
• Lifetime: The memory persists until it is no longer referenced. Its
• lifetime is managed by the runtime's reference counter, not tied to a
• specific scope.
• Performance: Slower than stack allocation. Involves a call to the
• system's memory allocator ( malloc ) and requires runtime overhead for
• reference counting.

When to use which:

• STACK: Use for most local, temporary data. It's the idiomatic and
• most performant choice for data that does not need to outlive the
• function in which it was created.
• HEAP: Use when a struct instance must be shared or returned from a
• function and needs to have a lifetime independent of any single
• scope. Also used for very large structs to avoid overflowing the stack.

Opaque Structs

Safety & Undefined Behavior (UB)

The primary benefit of opaque structs is preventing a whole class of undefined behavior by strengthening type safety at the language boundary.

How Safety is Increased

Eliminates Type Confusion: Before, you might have used a generic type like `u64` or `&void` to represent a C handle. The compiler had no way to know that a `u64` from `database_connect()` was different from a `u64` from `file_open()`. You could accidentally pass a database handle to a file function, leading to memory corruption or crashes. Now, `&DatabaseHandle` and `&FileHandle` are distinct, incompatible types *. The Aela compiler will issue a compile-time error if you try to misuse them, completely eliminating this risk.

Prevents Invalid Operations in Aela: * By disallowing member access and instantiation, we prevent Aela code from making assumptions about the C data structure. Aela code cannot accidentally:

Read from or write to a field that doesn't exist or has a different offset (`my_handle.field`). Create a struct of the wrong size on the stack ( let handle: StringBuilder ). * Perform pointer arithmetic on the handle. The only thing Aela code can do is treat the handle as an opaque value to be passed back to the C library, which is the only safe way to interact with it.

For Users of Opaque Structs

Your documentation should include:

1. Purpose and Syntax: Explain that opaque structs are for safely handling foreign pointers/handles. Show the syntax:

1. Rules of Engagement: Clearly state the allowed and disallowed operations we implemented.

Allowed: Passing to/from FFI functions, assigning to other variables of the same type, comparing for equality. Disallowed: Member access ( . ), instantiation ( new ), and dereferencing. Always use a reference ( &MyFFIHandle ).

1. A Mandatory Safety Section on Lifetimes: This section must be prominent. It should explain the dangling pointer risk and establish a clear best practice.

When working with opaque handles, you are responsible for managing their memory. Most C libraries provide functions for creating and destroying these objects. You must call the destruction function to prevent memory leaks and undefined behavior.

Interfaces

This document specifies the design and behavior of Aela's system for polymorphism, which is based on interface, struct, and impl...as... declarations.

Overview

Aela's polymorphism is designed to be explicit, safe, and familiar. It allows developers to write flexible code that can operate on different data types in a uniform way, a concept known as dynamic dispatch. This is achieved by separating a contract's definition (the interface) from its implementation (the struct and impl block).

The core philosophy is:

Interfaces define abstract contracts or capabilities.

Structs define concrete data structures.

impl...as... blocks prove that a concrete struct satisfies an abstract interface.

Components

The interface Declaration

An interface defines a set of method signatures that a concrete type must implement to conform to the contract.

Rules:

An interface block can only contain method signatures. It cannot contain any data fields.

Method signatures within an interface must not have a body. They must end with a semicolon ;.

The self parameter in an interface method must be of a reference type (e.g., &self).

The struct Declaration

A struct defines a concrete data type. Its role is unchanged.

Rules:

A struct can only contain data fields. Method implementations are defined separately in impl blocks.

The impl...as... Declaration

This block connects a concrete struct to an interface, proving that the struct fulfills the contract.

Rules:

The impl block must provide a concrete implementation for every method defined in the .

The signature of each implemented method must be compatible with the corresponding signature in the interface.

A single struct may implement multiple interfaces by using separate impl...as... blocks for each one.

Interface Types

A variable can be declared with an interface type by using a reference. This creates a "trait object" or "fat pointer" that can hold any concrete type that implements the interface.

Syntax: &

Behavior: A variable of type & is a fat pointer containing two components:

A pointer to the instance data (e.g., a &User).

A pointer to the v-table for the specific (Struct, Interface) implementation.

Duration & Instant

Time-related bugs are notoriously common and usually subtle. The root cause is frequently quantity confusion: when a plain number like 10 or lastUpdated is used, its unit is ambiguous. Does it represent 10 seconds, 10 milliseconds, or 10 microseconds? The programmer's intent is lost, hidden in variable names or documentation, leading to misinterpretations and errors.

Duration a first-class type with built-in literals. This design has two major benefits:

Improved Comprehension: Code becomes self-documenting. A value like 250ms is unambiguous; it cannot be mistaken for seconds or any other unit. This clarity makes code easier to read, write, and maintain. An expression like let timeout = 1s + 500ms; is immediately understandable without needing to look up function definitions or comments.

Clarified Intent & Type Safety: By distinguishing Duration from numeric types, the compiler can enforce correctness. You cannot accidentally add a raw number to a duration (5s + 3 is a compile-time error), which prevents nonsensical operations. Function signatures become more expressive and safe, for example fn sleep(for: Duration). This forces the caller to be explicit (e.g., sleep(for: 500ms)), eliminating the possibility of passing a value with the wrong unit.

The Duration type moves the handling of time units from a convention to a language-enforced guarantee, significantly reducing a whole class of common bugs.

Literals & type

• Literals: INT_LITERAL DurationUnit or FLOAT_LITERAL DurationUnit (e.g., 250ms , 1.5s ).
• Type: Duration is a first-class scalar quantity (internally monotonic-time ticks; implementation detail).
• Sign: Duration is signed . -5s is allowed via unary minus.
• No implicit numeric conversions: Duration never implicitly converts to/from numeric types.

Unary

Binary with Duration

Float scalars

Disallowed by default: Duration * F64 , Duration / F64 Rationale: silent precision loss. Provide library helpers instead (e.g., Duration::from_seconds_f64(x) ).

Comparison

Instant

Casting / construction

• Allowed: explicit constructors, e.g. Duration::from_ms(250) , Duration::seconds_f64(1.5) .
• Disallowed: implicit casts ( (i32) d , (f64) d ).

Overflow & division semantics

• Checked arithmetic by default: + , - , * on Duration panic on overflow (or trap).
• Provide library variants:

• checked_add , checked_sub , checked_mul → Option
• saturating_add , saturating_sub , saturating_mul
• Division: d / n truncates toward zero; n must be nonzero.
• d / d returns F64 (no truncation).

Examples

Suffix/literal interaction (clarity)

• 1s + 500ms is fine; units normalize.
• 1.5s is legal as a literal; it’s converted to integral ticks (ns) with rounding toward zero during lex/const-eval. (If you prefer bankers-rounding, specify that instead.)
• No ambiguity with range tokens: ensure lexer orders '...' , '..=' , '..' (longest first) and treats ms/min etc. as unit suffixes , not identifiers.

Arenas

Overview

Aela's has a three-part model for safe, dynamic memory management. The model is designed to provide explicit, and verifiable memory control for both hosted (OS) and freestanding (bare-metal) environments.

The model consists of:

• An intrinsic Arena type for memory provisioning.
• A transactional reserve statement for scoped memory reservation.
• A context-aware new keyword for object allocation.

The implementation is based on compile-time AST tagging, ensuring zero runtime overhead and inherent safety for asynchronous and multi-threaded code.

The Arena

The Arena is a primitive type known to the compiler, used for managing a block of memory.

Syntax

An Arena is provisioned using a special form of the new expression.

Semantics

new {} : A runtime operation for hosted environments. It calls the system allocator (e.g., malloc). This expression is fallible and should be treated as returning an Option(Arena).

new static { size: ... } : A compile-time instruction. It directs the linker to reserve a fixed-size block of memory in the final binary's static data region (e.g., .bss). This is the primary mechanism for provisioning memory on bare metal.

The reserve Statement (Transactional Reservation)

The reserve statement transactionally reserves memory from an Arena for a specific lexical scope.

Syntax

Semantics

The reserve statement attempts to acquire size_expr bytes from the given arena_expr.

If the reservation is successful, the first Block is executed.

If the reservation fails (the arena has insufficient capacity), the else Block is executed.

A successful reservation creates a special allocation context that is active for the duration of the success block and any functions called from within it.

The new Keyword (Allocation)

The new keyword creates an object instance. Its behavior is context-dependent and verified by the compiler.

Semantics

The compiler enforces three distinct behaviors for new:

Hosted Default Context: When compiling for a hosted target and not inside a reserve block, new allocates from the system heap.

Freestanding Default Context: When compiling for a bare-metal target and not inside a reserve block, a call to new is a compile-time error. This ensures no accidental heap usage on constrained devices.

reserve Context: Inside a successful reserve block, new allocates from the reserved memory. This allocation is infallible and returns a value of type T, not Option(T).

Complete Bare-Metal Example

Buffers

Introduction

Buffer(T) is a fundamental intrinsic type that provides a low-level, direct interface to a contiguous block of allocated memory (from where depending on if you do or don't use a reserve block). It is the primitive that higher-level, safe collection types like Vec(T) and String are built.

As an intrinsic , the compiler has special knowledge of Buffer(T) , allowing it to enforce powerful compile-time guarantees about memory ownership and borrowing. It's important to understand that Buffer(T) is intentionally designed as an unsafe primitive . Its core operations do not perform runtime bounds checking, providing a zero-overhead foundation for performance-critical code and the standard library. Your code can make it safe

Core Concepts

Representation

A Buffer(T) is a "fat pointer" containing two fields:

1. A raw pointer to the start of the memory block.
2. The capacity of the buffer (the total number of elements it can hold).

A Buffer(T) only tracks its total capacity. It does not track how many elements are currently initialized or in use (its length ). This responsibility is left to higher-level abstractions.

Ownership

The Buffer(T) value is the unique owner of the memory it controls. The compiler's verifier enforces this ownership model strictly:

• When a Buffer(T) is moved, ownership is transferred. The original variable can no longer be used.
• When a Buffer(T) variable goes out of scope, its memory is automatically deallocated.
• The std::buffer::drop intrinsic can be used to explicitly deallocate the memory, consuming the buffer variable.

This model guarantees at compile time that the buffer's memory is freed exactly once, eliminating memory leaks and double-free errors.

The Intrinsic API

The following functions provide the raw manipulation capabilities for Buffer(T) .

std::buffer::alloc

std::buffer::write

std::buffer::read

std::buffer::capacity

std::buffer::drop

std::buffer::view

std::buffer::slice

The Safety Model: A Layered Approach

The safety of Buffer(T) and its ecosystem is best understood as a series of layers, where stronger guarantees are built upon more primitive ones.

Layer 1: The Unsafe Buffer(T) Primitive

The intrinsic functions themselves form the base layer. They are designed to be as close to the machine as possible. std::buffer::write compiles to a single store instruction, and std::buffer::read to a single load . They do not have bounds checks because they are meant to be the absolute zero-cost building blocks. This layer is primarily intended for the authors of the standard library and other highly-optimized, low-level code.

Layer 2: Compile-Time Safety via the Verifier

The compiler's verifier (or "borrow checker") provides the next layer of safety, and it does so with zero runtime cost . It enforces:

• Ownership & Lifetimes : Guarantees that a Buffer is dropped exactly once and that any view or slice cannot outlive the Buffer it borrows from.
• Aliasing Rules : Prevents data races by ensuring that you cannot have a mutable borrow ( T[] ) at the same time as any other borrow of the same data.

These checks happen entirely at compile time.

Layer 3: Provable Safety via Refinement Types

This is the highest level of safety, allowing for the creation of truly safe abstractions on top of the unsafe Buffer primitive. The language allows types to be "refined" with predicates that the compiler must prove.

A safe Vec(T) type in the standard library would not expose the unsafe read / write intrinsics. Instead, it would provide methods whose signatures use refinement types to enforce correctness:

This system provides two powerful benefits:

1. Compile-Time Proof : If you call my_vec.get(5) and the compiler can prove the vector's length is greater than 5, the safety is guaranteed and the generated code is just a direct memory access. The safety check has zero runtime cost.

1. Compiler-Enforced Runtime Checks : If the compiler cannot prove the index is safe (e.g., it comes from user input), it will issue a compile-time error. This forces the programmer to add an explicit if check, which provides the compiler with the proof it needs inside the if block.

This layered approach is the essence of a zero-cost abstraction: safety is guaranteed by the compiler wherever possible, and runtime costs are only incurred when logically necessary and are made explicit in the program's control flow.

Atomics

Introduction

Atomic(T) is a fundamental intrinsic type designed for high-performance concurrency. It provides a wrapper around primitive types that guarantees safe access across multiple threads.

Unlike standard variables, operations on Atomic(T) are indivisible. However, atomicity alone is insufficient for correctness; memory ordering is equally critical. This API exposes fine-grained control over how the CPU and compiler are allowed to reorder memory operations, enabling the construction of lock-free data structures and synchronization primitives.

Core Concepts

Atomicity & Type Constraints

An operation is atomic if it is indivisible: a thread observes either the old value or the new value, never a "torn" or intermediate state.

Allowed Types : `T` must be a primitive integer, boolean, pointer, or an `enum` with a fixed underlying integer representation (e.g., `repr(u8)`) where all bit patterns are valid. Alignment : Atomic(T) requires natural alignment for T . Static Check : If alignment is statically known to be insufficient, it is a compile-time error . Dynamic Check : If a pointer is misaligned at runtime, the behavior is a guaranteed trap (panic).

Lock-Free Guarantees

While Atomic(T) enables lock-free algorithms, the operations themselves are not guaranteed to be lock-free on all platforms for all types.

Hardware Support : If the target CPU supports atomic instructions for `sizeof(T)`, operations are compiled to those instructions. Software Fallback : If the hardware lacks support (e.g., 64-bit atomics on 32-bit arch), the runtime may use a hidden global lock / hashed lock pool. Intrinsic Check *: Use std::atomic::is_lock_free() -> bool to query if operations on T are truly lock-free on the current target.

Memory Ordering

The Ordering enum controls how operations synchronize with other threads.

1. `Relaxed` : No synchronization. Only atomicity is ensured.
2. `Acquire` : Valid for loads. It ensures that no subsequent memory accesses can be reordered before this operation.
3. `Release` : Valid for stores. It ensures that no previous memory accesses can be reordered after this operation.
4. `AcqRel` : Valid for RMW (Read-Modify-Write). Combines Acquire and Release.
5. `SeqCst` : Strongest ordering. Enforces a total order on all SeqCst operations consistent with program order.

The Synchronization Contract

The primary mechanism for thread coordination is the Acquire-Release pair :

An Acquire operation on an atomic object synchronizes-with a Release operation on the same object if the Acquire reads the value written by that Release (or a value from a release sequence headed by that Release ).

Effect : All memory writes that happened before the Release are guaranteed to be visible to the thread that performed the Acquire .

The Intrinsic API

std::atomic::load

std::atomic::store

std::atomic::exchange

std::atomic::compare_exchange

| Constraints | 1. failure cannot be Release or AcqRel (failure is a load).

1. failure cannot be stronger than success (e.g., if success is Relaxed , failure cannot be SeqCst ). |
2. | Description | Atomically checks if *ptr == expected .

Success : Writes desired using success order. Returns (true, old_val) .

Failure : Loads current value using failure order. Returns (false, current_val) .

Note : old_val and current_val represent the value at ptr immediately before the operation.* |

std::atomic::fetch_add / sub / and / or / xor

Usage & Safety

Concurrency & Parallelism

Aela's model is built on two orthogonal keywords, `async` and `task` , that modify function declarations. These provide a clear, explicit syntax for defining concurrent work. The runtime manages a thread pool to execute these tasks, enabling both I/O-bound concurrency and CPU-bound parallelism that work in concert.

Core Concepts

It is crucial to understand that async and task are separate modifiers with distinct physical meanings, even though they are designed to feel cohesive.

async : The Pausable Function

An async function is a state machine. Calling it does not start execution; it returns a Future (a "cold" task). The code only runs when you explicitly await it or pass it to a poller like std::concurrency::select .

task : The Parallel Job

A task function is a unit of parallel work. Calling it immediately submits the work to the runtime's thread pool and returns a Task handle (a "hot" task). You continue executing while the task runs in the background.

Function Modifiers

You can combine these keywords to define exactly how a function behaves.

Parallelism: task

While async handles waiting (IO), task handles doing (CPU). Aela uses a Work-Stealing Scheduler to distribute CPU-intensive work across a pool of OS threads.

task fn : Hot Execution

A function marked with task is distinct from a normal function or an async function.

Eager Submission: When you call a `task fn`, it is immediately pushed to the global scheduler queue. You do not need to `await` it to start it. The `Task(T)` Handle: It returns a handle that tracks the running job. If you drop the handle, the task continues running (detached). Isolation: * task functions cannot capture references to the surrounding stack unless those references are Send and Sync . They are effectively "spawned" into a new root scope.

task { ... } : Structured Parallelism

The task block is a Fork-Join Barrier . It is designed to safely parallelize work within a single function scope.

The Barrier: The block does not finish until every task spawned inside it has completed. Stack Safety: Because the block guarantees that all inner tasks finish before the function continues, inner tasks can safely borrow variables from the parent function . This is impossible with standard "spawn" functions in other languages (which usually require copying/moving data). Work Stealing: * The tasks inside the block are added to the local worker's queue. Other idle threads will "steal" these tasks to help complete the block faster.

Pool Control & Oversubscription

The runtime manages the complexity of OS threads so you don't have to.

1. Oversubscription: The runtime defaults to one thread per CPU core ( std::task::available_parallelism() ). It is designed to be "oversubscribed" safely. You can spawn thousands of task functions; the runtime will queue them and execute them as fast as possible on the fixed number of worker threads.
2. Backpressure: The scheduler uses a bounded global queue (default capacity: 256 tasks). If you spawn tasks faster than the CPU can process them, calling a task fn will eventually transition from non-blocking to blocking (waiting for a slot in the queue).
3. Environment Control: For deployment tuning, you can override the thread pool size via environment variable: AELA_TASK_COUNT=8 .

Concurrency: async

Sometimes you need a small unit of async work without defining a whole function, or you want to start async work from an sync function.

async fn : A reusable pausable function.

async { ... } : An anonymous Future .

It captures variables from the surrounding scope. Like async fn , it is lazy and it does not run until awaited. All tasks must be completed and handled before before the program will continue.

Control Flow

`await` : Pauses the current function, yielding control back to the runtime until the awaited operation completes. `std::concurrency::block_on` : The bridge between synchronous and asynchronous code. It starts a temporary event loop to drive a future to completion. This is typically used only in main or unit tests. `std::concurrency::select` : Races multiple futures. It waits for the first * one to complete and cancels the others.

Safety

Aela treats the scheduler as a "Safety System" rather than an aftermarket part. Because the runtime is integrated into the language, the compiler can provide stronger guarantees than if it took a library-based approach.

1. Compile-Time Data-Race Prevention: The compiler knows the difference between a local async execution (single-threaded) and a task execution (multi-threaded). It enforces Send and Sync rules strictly at the task boundary.
2. Single Blocking Bridge: A built-in runtime provides one, official way to handle blocking calls: std::task::run_blocking() . This prevents the "Color of your function" problem from causing deadlocks when libraries mix blocking/non-blocking strategies.
3. Guaranteed Cleanup: task handles are tied to the runtime. If a Task handle is dropped, the language enforces a consistent policy (detachment), preventing undefined behavior or zombie threads common in ad-hoc library implementations.

Formal Verification

Overview

Aela enables developers to write mathematically precise specifications that describe the expected state and behavior of a program, which the compiler formally verifies at compile time. These specifications are not runtime code — they do not execute, incur no runtime cost, and exist solely to ensure program correctness before code generation.

• #let (the ghost of...)
• #requires (pre condition)
• #ensures (post condition)
• #invariant (can’t change)
• #variant (must change)

All of them appear before the function/loop they describe. None of these exist at runtime. They’re for the verifier only.

#let — The ghost of...

#let defines a ghost name for an expression, purely for specs.

You can put it right before a function or loop to bind names used in the following specs:

Here:

• oldN is only visible to the verifier.
• oldN does not exist in the compiled code.
• You can use oldN in #requires , #ensures , #invariant , #variant , etc.

Think of #let as: "Give me a ghost name for this value/expression so I can talk about it in my conditions."

#requires — Precondition

#requires means this must be true when we enter this function (or loop). Placed directly above the function:

The verifier checks every call to factorial proves n >= 0 and assumes n >= 0 inside the body. You can also (optionally) apply #requires to loops, if you want to state assumptions at loop entry:

#ensures — Postcondition

#ensures goes right before the function and says: "This will be true after this function returns."

Example:

The verifier proves we assume n >= 0 on entry and the value returned by the function ( result ) always satisfies result >= n .

Summation

#invariant

An invariant can’t change (must stay true during loop). It goes immediately before a loop:

This means:

• Before the first iteration: 0 <= i <= n must hold.
• After every iteration, if we go around again, it must still hold.
• When the loop exits, 0 <= i <= n is still true.

The invariant describes what must not be broken across iterations. It’s not "the variable can’t change"; it’s this relationship must stay true even as variables change.

#variant

#variant also goes right before the loop , together with #invariant :

Here:

• n - i is the variant expression .
• The verifier proves:
• n - i is always ≥ 0 inside the loop.
• On every iteration that continues the loop, n - i gets strictly smaller .

This proves the loop must terminate .

So:

• #invariant - this condition must keep holding.
• #variant - this measure must go down when we repeat.

Your loop may increase i , but your #variant is something that decreases (like n - i ).

Examples

General rule: Directives attach to the next construct.

For functions

For loops

You can stack them:

All of this is compile-time-only verification syntax , erased in the compiled program.

Cheat Sheet

• #let name = expr - Ghost name for expr , only for use in specs.
• #requires P - P must be true before we enter this function/loop.
• #ensures Q - Q will be true when the function returns.
• #invariant I - I must hold before the loop, after each iteration, and when it ends.
• #variant V - V must strictly decrease each time we repeat the loop (and stay in a well-founded set).

All placed before the thing they describe.

FFI

The Foreign Function Interface (FFI) provides a mechanism for Aela code to call functions written in other programming languages, specifically C. This allows you to leverage existing C libraries, write performance-critical code in a lower-level language, or interact directly with the underlying operating system.

The core of Aela's FFI is the ffi definition, which declares a external C functions and their Aela type signatures or varibales and their types. The Aela compiler and runtime use these declarations to handle the "marshalling" of data—the process of converting data between Aela's internal representations and the C Application Binary Interface (ABI).

Declaring an FFI type

You declare a C function or C variable using the ffi keyword.

ABI Contract

A stable C ABI ( ae_c_abi.h ) defines the contract. It specifies the C-side string representation: typedef struct { char* ptr; int64_t len; } AeString;

Compiler Type Mapping

The Aela compiler's types.c maps the language's string type to an LLVM struct with an identical memory layout: %aela.string = type { i8*, i64 } .

Passing Convention

Strings are passed to C functions BY VALUE.

• Aela code generates: call void @c_function(%aela.string %my_string) .
• C code receives: void c_function(AeString my_string) .

Safety & Ownership

• This pass-by-value convention is a "defensive" design.
• The C function gets a copy of the string descriptor, preventing it
• from modifying the original string's length or pointer in Aela's
• memory.
• Aela's runtime retains ownership of the underlying character buffer
• ( char* ). The AeString struct is just a temporary, non-owning view.

: The exact name of the function as it is defined in the C source code.

: The Aela type signature for the C function. This signature is the crucial contract that tells the Aela compiler how to call the C function correctly.

Example

Let's look at the stdio example from the standard library:

This code does the following:

It declares that there is an external C function named ae_stdout_write.

It specifies that from the Aela side, this function should be treated as one that accepts a single Aela string and returns void.

To call this function, you use the standard module access syntax:

The Aela-C ABI and Data Marshalling When an FFI call occurs, the Aela compiler generates "glue" code to translate Aela types into types that C understands. This mapping follows a specific Application Binary Interface (ABI).

Primitive Types

Most Aela primitive types map directly to their C equivalents.

Strings

The Aela string is a "fat pointer" struct containing a pointer to the data and a length. C, however, typically works with null-terminated char* strings.

Aela to C: When you pass an Aela string to an FFI function, the compiler automatically extracts the internal ptr and passes it as a const char* to the C function. The string data is guaranteed to be null-terminated, so standard C string functions can operate on it safely.

FFI Call:

The C function receives a standard C string.

Structs, Arrays, and Closures (Complex Types)

Complex aggregate types like structs, arrays, and closures cannot be passed directly by value to C functions. The ABI for these types is simple: you pass a pointer.

Aela to C: When passing a complex type, Aela passes a pointer to the object's memory layout. Your C code receives an opaque pointer (void\*) to this data. It is your responsibility in C to know the memory layout of the Aela type and cast the pointer accordingly to access its fields.

This is an advanced use case and requires careful handling to avoid memory corruption. You must ensure that the struct definition in your C code exactly matches the memory layout of the Aela struct.

Often you end up with an opaque strct in Aela. These can not have methods or properties.

This design provides a safe and clear boundary. The complex, type-safe variadic handling happens within the Aela runtime, while the FFI call itself remains a simple, direct translation of the string argument to a char*.

Linking C Code To make your C functions available to the Aela compiler, you must compile them into an object file (.o) or a library (.a, .so, .dylib) and include it during the final linking step.

The Aela driver will eventually provide flags to specify these external object files. For now, you would typically use a command like clang to link the Aela-generated object file with your C object file.

1. Compile your Aela code aec your_program.ae -o your_program.o

1. Compile your C code clang -c my_ffi_functions.c -o my_ffi_functions.o

1. Link them together clang your_program.o my_ffi_functions.o -o
2. final_executable

This process creates the final executable where the Aela runtime can find and call your C functions.

Formal Grammar Spec