Get Started

Aela is a software platform for creating formally verifiable, memory safe, and highly reliable applications. What's included in the compiler:

• Works in any editor
• Provides a built in linter, formatter, and LSP.
• A local, offline-first agent that understands the compiler and your codebase and can talk to your other AI services.
• Supports JIT module (that's hot reloading for compiled programs, aka: edit and continue)

Install the compiler

In a new directory, create a new project using the following command.

This will create some default files.

Edit the index.json file to name your project.

Next you’ll edit the main.ae file

To build your project, run the following command.

You’ll see a new directory with the compiled program that you can run.

Compiler Modes

aec build

This is your traditional, one-shot Ahead-Of-Time (AOT) compiler command.

aec run

This is a convenience command for development.

aec daemonize

This command exposes the engine's interactive mode directly to the command line.

aec package

This is a higher-level workflow and distribution tool.

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:

For functions, Aela uses a unified parameter list with a ; split: fn id(T; x:T) -> T (compile‑time params before ; , run‑time after). See the Functions section.

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 .

Arrays & Maps

• Dynamic slices: T[] — size known at run time; indexing and length available via stdlib.
• Fixed arrays: T[N] — size is part of the type; N must be compile‑time evaluable.
• Maps: map(K, V) — associative container; keys and values are regular types.

References (borrowing)

&T is a borrowed reference to T .

• 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.

Function & Closure Types

Function types and values share the same shape: fn(params) -> Return with optional modifiers.

Modifiers:

• pure — no observable side effects; enables stronger reasoning/optimizations.
• thread — safe to run in a separate thread (may be combined with pure ).
• async — produces a Future(Return) ; use await to get the value.

Unified parameter list (declarations):

Enums (sum types)

Enums declare a closed set of variants and are exhaustively pattern‑matched.

Futures & Async

async functions return future values that represent a computation in progress. Conceptually, the type is Future(T) , and await yields T .

How the Compiler Thinks About Types (High‑Level)

Internally, every type has a kind (primitive, struct, enum, map, array, function, optional, reference, etc.) and a canonical signature string (e.g., "fn(i32)->bool" ). The compiler interns types in a cache so that equality checks are fast pointer comparisons.

• Compatibility: types_are_compatible(dst, src) determines assignment/call compatibility (more than just raw equality when coercions are allowed).
• Optional & None: represented distinctly ( TYPE_OPTIONAL around a base, and a special TYPE_NONE ).
• Closures: carry a function type plus captured environment.
• Modules: form a namespace; the module itself has a type used by the compiler for resolution.

You normally don’t see these details, but they explain why types print consistently and compare cheaply.

Minimal Grammar Reminders (surface)

• Map: map(K, V)
• Optional: T?
• Reference: &T
• Array: T[expr] (fixed) or T[] (slice)
• Function type: pure fn(T1, T2) -> R
• Type application: Name(T, U)

For advanced material (refinements { x: T where φ } and dependent forms like Vec(T, N) ), see the companion doc.

Best Practices

• Prefer named aliases for recurring shapes: type Port = { p: i32 where 1024 <= p && p <= 65535 };
• Use ? sparingly; prefer sum types (e.g., Result ) when you want the caller to handle both cases explicitly.
• Keep function types pure when possible; it improves composability.
• Choose fixed arrays ( T[N] ) when size is intrinsic and enables better checking/optimization.

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.

• The condition must be an expression evaluating to bool .
• Both then_branch and else_branch must be statements , usually blocks.

Examples

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 Expression

Syntax

Description

Exhaustive pattern matching. Each match arm uses a pattern and a block.

• _ is the wildcard pattern (required if not all cases are covered).
• Patterns can be:
• Literals: 1 , "foo" , 'c' , true , false
• Identifiers: binds the value
• Constructor patterns: Some(x) , Err(e)

Example

5. return

Syntax

Description

Exits a function immediately with an optional return value.

Examples

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.

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.

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

Out-of-the-box 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

• The 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 ( (int) 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.

Concurrency

Aela's concurrency is built on two orthogonal keywords, async and thread , 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 Keywords: async and thread

It is crucial to understand that `async` and `thread` are two separate modifiers with distinct meanings. Even though they are designed to work in a way that feels cohesive.

async

Marks a function as pausable . An async function can use the await keyword to non-blockingly wait for I/O or other long-running operations. It primarily relates to concurrency .

The decision to have a langauge-native async engine provides significant advantages for compile-time determinism.

thread

Marks a function as a parallel task . Calling a thread fn is a special operation that is non-blocking. It immediately submits the function to the runtime's thread pool for execution and returns a Task handle. It primarily relates to parallelism .

These keywords can be combined to define tasks with different behaviors:

Defining and Spawning Tasks

Threaded tasks are ideal for the parallel processing of CPU intensive workloads.

But sometimes a threaded task to compartmentalize work. For example, you might want some async processing to happen in another thread, separately from a UI thread.

The async keyword is optional and is used if the task needs to await I/O. The function's return type defines the final value returned when the task is complete.

Calling a function marked thread is a non-blocking operation. It starts the task in the background and immediately returns a Thread handle.

Structured Parallelism: thread { ... } Block

The thread block is used to run a group of tasks in parallel and wait for all of them to complete before continuing.

Channels

Channels are used for streaming communication between threads. The type Channel(T) is a valid type according to the TypeApplication grammar rule.

Streams

This pattern pauses the current function to process each message from a channel sequentially.

Events

This registers a handler and immediately returns, allowing the current function to continue its work.

Integrated Vehicle Safety vs. Aftermarket Parts

Think of it like the safety systems in a car.

A Library-Based Ecosystem (like Rust's): This is like buying a car chassis and then adding safety features yourself. You buy airbags from one company, an anti-lock braking system from another, and traction control from a third. They might be excellent components, but they weren't designed to work together as a single, cohesive system.

A Built-in Scheduler (Aela's model): This is like buying a modern car where the manufacturer has designed the airbags, ABS, traction control, and crumple zones to work together as a single, integrated safety system. It's tested as a whole and provides guarantees that the individual parts can't.

Here are the specific safety wins this integration provides.

1. Compile-Time Data-Race Prevention

Because the scheduler is part of the language, the compiler has a deep understanding of what it means to "cross a thread boundary." It can enforce Send and Sync rules at compile-time. This means it's a syntax error to try to send non-thread-safe data into a thread fn or across a channel, completely eliminating an entire class of data-race bugs before the program can even run.

1. A Single, Safe Bridge for Blocking Code

As we discussed, blocking in an async context is a huge foot-gun. A built-in runtime provides one, official, and well-defined function for handling this: std::task::run_blocking(). This prevents a scenario where different libraries provide their own, subtly different (and potentially unsafe) ways of handling blocking calls, which would lead to confusion and bugs.

1. Guaranteed Structured Concurrency

The thread { ... } block is a major safety feature. Because it's a language construct powered by the built-in scheduler, the compiler can absolutely guarantee that all child tasks are completed before the parent function is allowed to continue. This prevents "leaked" tasks and makes error handling robust and predictable. In a library, this guarantee might be weaker or easier to accidentally bypass.

1. Predictable Task Lifecycles

With a built-in scheduler, the behavior of a Task handle is predictable across the entire ecosystem. The rule that a handle will detach on drop is a language-level guarantee. This prevents situations where one library's handle might join on drop while another's aborts, leading to surprising behavior and resource leaks.

In short, a built-in scheduler allows Aela to treat concurrency as a core feature, subject to the same rigorous, compile-time safety analysis as the rest of the language.

Pool Control & Oversubscription

The Aela runtime is built on a work-stealing thread pool that defaults to using the number of logical CPU cores available (std::thread::available_parallelism()).

Pool Size & Pinning: The pool size can be overridden at startup via an environment variable (e.g., AELA_THREAD_COUNT=4). Fine-grained control like core pinning and thread priorities is considered a low-level OS feature and is not exposed through the high-level async/thread API. For expert use cases, a separate std::os::thread module could provide these unsafe, platform-specific controls.

On tiny targets without an OS, the runtime can be compiled in a "pool disabled" mode, using a single-threaded cooperative scheduler.

Oversubscription: The runtime's global task queue is bounded (e.g., a default capacity of 256 tasks). Calling a thread fn is cheap, but if the task queue is full, the call itself becomes an async operation. It will pause the calling function until space becomes available in the queue. This provides natural back-pressure and prevents developers from overwhelming the system.

Formal Verification

This document specifies the design and behavior of Aela's compile-time verification system , which ensures the correctness of a program through formal specifications — namely, invariant and property declarations embedded in impl blocks.

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.

There are two key constructs:

`invariant`: A safety condition that must always hold before and after each function in an `impl` block. property : A liveness or temporal condition that must hold across all valid execution traces of a type’s behavior.

These declarations allow Aela to verify complex asynchronous and stateful systems using SMT solvers or model checking , without requiring users to learn a separate formal language.

Components

The invariant Declaration

An invariant specifies a condition that must hold before and after every function in an impl block.

Rules:

Invariants must be side-effect-free boolean expressions. They may reference any field defined in the corresponding struct . The compiler verifies that every function in the `impl` block preserves the invariant. If the compiler cannot prove an invariant holds across all paths, compilation fails.

In this example, the invariant guarantees that the count is never negative. The verifier ensures this remains true even after increment() executes.

The property Declaration

A property expresses a temporal guarantee — such as liveness or ordering — across the program’s behavior.

Temporal expressions may include:

`always`: The condition must hold at all times. eventually : The condition must hold at some point in the future. `until`, `release`: Conditions over time and ordering. forall , exists : Quantifiers over a domain (e.g., tasks, states).

Rules:

Properties do not affect control flow or behavior. They are used by the compiler to prove guarantees about possible program traces . * Property violations produce counterexample traces at compile time.

Specification Behavior

`invariant` is used for safety ("nothing bad happens"). property is used for liveness ("something good eventually happens").

The compiler treats both as compile-time-only declarations that participate in verification, not execution.

Old State Reference: old(expr)

The old keyword allows a function’s ensures clause to reference the value of an expression before the function was called.

The compiler ensures that the post-state ( count ) relates correctly to the pre-state ( old(count) ).

Quantifiers and Temporal Blocks

Quantifiers can be used in properties to express conditions across many elements or tasks.

Compiler Interactions

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