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 watch

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

aec package

This is a higher-level workflow and distribution tool.

Module and Package System

Aela's module system is designed for organizing code into reusable and maintainable packages. The entire system is controlled by a manifest file named index.json .

Packages are precompiled binaries, this makes them fast, but they can also ship with the source code and that wont make them any slower. See the GUI module for a comprehensive example of a multi-platform module.

Package Manifest

Every Aela project is a package, and every package is defined by an index.json file at its root. This file tells the compiler everything it needs to know about your project.

Key Fields

• "name": The official name of your package (e.g., "my-app").
• "version": The version number (e.g., "0.1.0").
• "entry": The relative path to the main source file that acts as
• the entry point for compilation (e.g., "src/main.ae").

Example

Managing Dependencies

You can include other Aela packages in your project by listing them in the "dependencies" section of your index.json .

• The key is the name you will use to import the module (e.g., "ui").
• The value is the relative path from your index.json to the
• dependency's root directory.

Example

Exports

By default, all functions, structs, and variables defined in a file are private to that file. To make a symbol visible to other modules, you must explicitly mark it with the export keyword.

Example

Re-exports

Imports

You use the import statement to bring exported symbols from other modules into the current file. Aela supports two forms of imports.

Namespace Import

This is the most common form. It imports all exported symbols from a module under a single namespace alias.

Syntax

Example

Named Imports

This allows you to import specific functions or types directly into the current scope, without needing a namespace qualifier.

Syntax

Example EXAMPLE

Advanced Build Configuration (FFI)

The index.json manifest also allows you to control the native build process, which is essential for linking against C, C++, or Objective-C code when using the Foreign Function Interface (FFI).

Key Sections

• "sources": A list of native source files (.c, .mm, etc.) to be
• compiled alongside your Aela code.
• "link": A list of flags to pass to the system linker (e.g., clang).

Notes

• Both "sources" and "link" flags can be specified per-platform
• (e.g., "darwin", "linux", "windows") or as "shared" for all platforms.
• The compiler automatically includes the linker flags from all packages
• listed in your "dependencies" section.

Example

This configuration tells the Aela compiler:

1. On macOS, compile the src/native/apple.mm Objective-C++ file.
2. When linking the final executable, add flags to link against the
3. Foundation, AppKit, and ObjectiveC system frameworks.

Type System Features

Refinement Types

Refinement types allow you to create a subtype from an existing type by adding constraints that are checked at compile time. This is useful for creating more precise and bug-resistant types.

Example

You can define a type that only allows positive integers, preventing invalid values at compile time.

Example: Non-Empty String

Refinements can use functions or properties in their conditions.

The primary benefit is turning potential runtime errors (like invalid arguments) into compile-time errors.

Dependent Types

Dependent types allow a type's definition to depend on a value, not just another type. This lets you encode properties like the size of a collection directly into its type.

Defining Dependent Structs

You define a dependent struct by including value parameters in parentheses () in its declaration.

Syntax

struct TypeName(param_name: ParamType, ...);

Example

Here, the Vect type depends on a length len and a type T.

Using Dependent Types in Functions

Function signatures can use these value dependencies to enforce relationships between parameters, making impossible states unrepresentable.

Example

This function to get the first element of a vector can only be called on a non-empty vector.

This feature allows you to build extremely safe APIs by making the compiler aware of properties that are usually only checked at runtime.

Operators

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

Optionals

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

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

Borrow Checker

Core Entities and Notation

• Place p : An lvalue, i.e. a path to a memory location. Examples: x , arr[i] , s.field . In safe Aela, places are structured paths (no raw pointer deref, pointer arithmetic, or unions).
• Reference &p / &mut p : A borrow of a place, producing a reference value.
• Loan L(p, kind) : The abstract fact that p is borrowed, with kind ∈ {shared, unique} .
• Program Point q : A location in the control-flow graph (CFG).
• Alive(L, q) : Predicate meaning loan L is still valid at point q (lexically-free semantics).
• Operations :
• reads(p, q) : a read of place p at q .
• writes(p, q) : a write to place p at q .
• moves(p, q) : a move from place p at q .
• Aliases(x, p, q) : x holds a reference to p at q (logical predicate, tracked via loan origins).
• Escape(r, q) : Reference r escapes its region at q (returned, stored, captured, etc.).

inter-procedural Region & Effect Summaries

• Each function with references is internally elaborated to carry region variables ρ .
• Example: fn get_first(&[i32]) -> &i32 elaborates to for<ρ> fn(&ρ [i32]) -> &ρ i32 .
• Compiler emits a summary : region params, outlives constraints, and an escape set.
• Call sites instantiate these summaries and unify with argument regions. This provides modular checking without WPO.
• Optional disambiguation syntax for multiple inputs: fn pick(arr: &T as A, other: &T) -> &A T; ties return to param marker A .

Minimal Syntax Escape Hatch (as A)

Keeps everyday code lifetime-less, but allow explicit disambiguation when inference cannot decide.

• Syntax: Parameters may carry labels: fn foo(x: &T as A) -> &A T . Returns may use &A . Struct fields may tie to labels.
• Labels introduce internal region vars (`ρ_A`) that summaries use. Unlabeled references get fresh ρ ’s.
• Elision rules: one input reference → auto-tie; multiple ambiguous inputs → require a label.
• Advanced usage:
• Outlives constraints can be added: fn foo(x: &T as A, y: &U as O) -> &A T where O : A; .
• Methods: self implicitly labeled Self , but can also be explicitly labeled: self: &Self as S .
• Diagnostics: Role-based: “return value tied to param a (label A) but a does not live long enough.” Quick fixes: “Add as A to param.”

Lifetimes in Data Structures

• Reference fields implicitly carry region parameters. struct Node { data: &T } elaborates to struct Node<ρ, T> { data: &ρ T } .
• Construction instantiates ρ from the argument’s region. Error if struct outlives the referenced data.

Place Overlap (I3)

• p overlaps p .
• p overlaps p.f . Distinct fields disjoint.
• arr[i] vs arr[j] : disjoint if indices are distinct compile-time constants; else conservative overlap.
• Library intrinsics like split_at_mut provide disjointness proofs via trusted contracts or runtime checks.

Escape Conditions (E1)

Reference escapes if it flows into a longer-lived region by:

• Returning from a function.
• Assigning to a longer-lived binding.
• Storing in struct/enum/global.
• Capturing by closure/future that outlives scope.
• Passing to FFI (unless contract says non-retaining).
• Storing in concurrent/shared cell accessible later.
• Erasure into longer-lived object/interface.

Asynchronous Code (async/await)

• Phase 1: Forbid loans across await unless the origin outlives the entire future. Practically: locals cannot cross await ; only borrows from captured fields of the async task can.
• Phase 2: Desugar async to state machines and check across suspension points, enabling safe long-lived borrows.

Closures (FunctionExpression)

• Capture classification:

• Read-only → shared.
• Mutate → unique.
• Move → by-value.
• Trait mapping: shared → Fn; unique → FnMut; move → FnOnce.
• Escaping closures require captured regions to outlive closure region.

Refinement Types

• Built-in predicates like initialized(x) , not_escaped(x) are decidable and do not require heavy SMT.
• User-defined predicates and full logical refinement are measured to avoid compile-time blowups and underspecification.

Diagnostics Without Lifetime Names

• Role-based regions: “returned reference must not outlive borrow of arr .”
• Highlight borrow creation, return site, and conflict.
• Optional symbolic labels (r1, r2) in error messages for clarity.

Rule-by-Rule Examples

Rule-by-Rule Examples (Concrete)

R0 — Implicit, Lexically-Free Regions

L1 — Loan Creation

L2 — Loan Propagation

A1 — Unique Exclusivity

A2 — Shared Read‑Only

I1 — Write Invalidates

I2 — Move Invalidates

I3 — Overlap/Fields

U1 — Use Requires Alive

U2 — No After‑Free

RB1 — Shared from Unique

RB2 — Unique from Unique (optional v1)

E1 — No Escaping Borrows

M1 — Binding Mutability

M2 — No Shared Mutability Without Atomics

T1 — Temporaries

T2 — Branches/Loops/Match

F1 — FFI Preconditions

F2 — FFI Postconditions

RFT1 — Refinement Well‑Formedness

RFT2 — Discharge at Use Sites

inter‑Procedural Summary (Elision)

Structs with Reference Fields (Implicit Regions)

Async Phase 1 — No Unique Loans Across Await

Closures — Capture Classification

C/C++ Harmony

Most languages' safty stops at the FFI boundary. But by automating the creation of safe FFI boundaries and embedding more of the C/C++ code's contracts directly into Aela's type system. Instead of just marking a boundary as unsafe and leaving the safety burden entirely on the developer, Aela can actively assist in verifying the C/C++ side of the interaction.

Automatically Generate "Diplomatic" Wrappers

Instead of manually writing write unsafe blocks and wrapper functions (This is tedious and error-prone). Aela can automate this.

Aela Compile can parse C/C++ header files (.h, .hpp) and automatically generatee the FFI bindings and a safe, idiomatic Aela wrapper. It's much more sophisticated than a simple binding generator.

Contract Inference

The tool can analyze C++ code for clues about contracts.

For instance, it can interpret a gsl::not_null or _Nonnull annotation as a non-nullable reference in Aela, automatically adding the necessary runtime checks.

Resource Management

If a C function create_foo() returns a pointer that must be freed with destroy_foo() , the generator can automatically create a smart pointer or RAII object in Aela that calls destroy_foo() on scope exit. This eliminates a huge class of resource leak bugs.

Error Handling

It can translate C-style error codes e.g., return -1; or errno = EINVAL; into Aela's native error-handling mechanism, like Result types or exceptions.

This moves the burden from the developer having to manually ensure safety to the too providing a verifiably safe starting point.

A Type System for C/C++ Interop

Aela's type system can understand C/C++'s quirks better. It encodes invariants about C pointers and memory directly into the types.

Sized Pointers

Instead of a raw pointer, Aela has types like Pointer(T, size_t N), which represent a pointer to a buffer of N elements. This allows the compiler to enforce bounds checking at the FFI boundary.

Nullability and Ownership

Explicitly differentiate between Pointer(T) (nullable) and Reference(T) (non-nullable). And types that encode ownership semantics like OwnedPointer(T) (must be freed) vs. BorrowedPointer(T) (must not be freed).

Tainted Data

Data coming from C/C++ is considered "tainted" by the type system. It needs to be explicitly validated (e.g., checking a string for valid UTF-8, ensuring a value is within an expected range) before it can be used in the safe context.

Integrate Static and Dynamic Analysis

Since Aela is written in C, it can integrate powerful C/C++ analysis tools directly into the build process.

Clang's Analyzers

Aela uses libraries from the Clang/LLVM project to perform static analysis on the C/C++ code. During compilation, it automatically invokes analyzers to check for things like null pointer dereferences, use-after-free, or buffer overflows in the C code being called, and flag a warning or error if a potential issue is found.

Boundary Sanitization

A "debug mode" for FFI that injects runtime checks at the boundary.

When your code calls a C function, it could automatically add canaries or check buffer boundaries. When C code calls back into Aela, it can validate incoming pointers and data. This is similar to running with AddressSanitizer (ASan), but it's focused specifically on the FFI-boundary risks.

By taking these steps, Aela doesn't just stop its safety guarantees at the boundary. It actively polices that boundary, making brownfield integration significantly safer and more robust than the manual, high-discipline approach required by other languages.

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.

Memory & Mutability Model

1. Default Allocation Semantics

• All values start on the stack by default.
• Stack allocations are:
• Fast
• Scoped
• Owned directly by the binding.

2. Heap Allocation

To allocate a value on the heap, use the new keyword with one of the following modifiers:

Syntax

All heap allocatations are reference counted.

Behavior

• new shared :
• Performs a copy of the stack value ( { ...val } )
• Allocates it on the heap
• Wraps it in a reference-counted container (non-atomic)
• Returns a reference: &T

• new shared atomic :
• Same as above, but uses atomic reference counting (thread-safe)

3. Mutability Semantics

Mutability is determined only by the binding keyword :

• There is no `mut` keyword
• Mutability is not encoded in types, structs, or fields

Example

Attempting to mutate a let -bound reference results in a compile-time error .

4. Weak References & Cycle Prevention [NOT IMPLEMENTED]

To solve the problem of reference cycles (e.g., a parent refers to a child, and the child refers back to the parent), Aela will provide weak references. A weak reference is a non-owning pointer that does not prevent an object from being deallocated.

The system is designed to be minimal and explicit, consisting of three parts:

The weak &T Type

A weak reference has a distinct type to ensure compile-time safety. This allows the compiler to enforce correct usage.

The weak() Downgrade Function

To create a weak reference, you must use the explicit, built-in weak() function. This makes the intent clear and avoids implicit "magic".

let strong_ref: &Foo = new shared { ... };

// Explicitly create a weak reference from a strong one. let weak_ref: weak &Foo = weak(strong_ref);

The if let Upgrade Pattern

Accessing the object behind a weak reference is inherently optional, as the object may have been deallocated. Aela enforces safe access through a conditional if let binding.

// Given a variable 'weak_ref' of type 'weak &Foo'

5. Copying Stack Values

• Heap allocation requires copying the stack value:

• This avoids moving ownership from the stack. Moves are not allowed .

5. Reference Types and Behavior

6. Compile-Time Analysis

• Safe aliasing of references
• Proper use of var (exclusive mutation)
• Reference count tracking correctness
• No runtime borrow errors required

The compiler performs static analysis to ensure:

7. No Implicit Moves from Stack

• Stack values cannot be moved to the heap.
• Heap promotion always requires a copy using { ...val } .
• new shared { ...std::move(x) } is on the roadmap

Calling Conventions

How variables are allocated and passed to functions. The 'new' keyword is the explicit signal for heap allocation and reference counting.

Primitives & Simple Structs (Stack Allocated)

• Rule: Variables declared WITHOUT the 'new' keyword live on the stack.
• In Memory: The variable holds the data directly.
• Function Passing: Passed BY VALUE (a full copy is made).
• Lifetime: Automatic (destroyed when the variable goes out of scope).
• Reference Counted: No.

Boxed Values (Heap Allocated via 'new')

• Rule: Variables initialized WITH the 'new' keyword are allocated on the heap.
• In Memory: The variable holds a POINTER to a "box" on the heap.
• Function Passing: Passed BY REFERENCE (a copy of the pointer is made).
• Lifetime: Managed (Reference Counted).
• Reference Counted: Yes.

Closures (Special Case)

• Rule: A closure that captures variables has its environment allocated on the heap.
• In Memory: The closure variable is a {func_ptr, env_ptr} struct. The env_ptr points to a heap-allocated box containing the captured variables.
• Function Passing: The {func_ptr, env_ptr} struct itself is small and is passed BY VALUE.
• Lifetime: The environment's lifetime is managed by Reference Counting.

GUI

Aela provides a cross platform GUI library that works on MacOS, iOS, Windows, Linux, & Android.

Install

Example

Why commercial-source?

Security

Transparency helps, but it’s not enough. Heartbleed, Log4Shell, and the xz backdoor landed in widely used open-source code. The gap isn’t visibility—it’s accountability, resourcing, and execution.

A commercial, closed-source model brings clear responsibility and funded security work:

Formal accountability

Commercial software runs under contracts and SLAs. When a vulnerability appears, a named company is on the hook—legally and financially—to fix it. In decentralized open source, responsibility often sits with volunteers without service commitments.

Dedicated, directed resources

We staff full-time security teams for audits, pen tests, and vulnerability management. Budget and people are assigned to unglamorous but critical maintenance and hardening that many projects lack.

Cohesive vision and focused dev

One organization sets architecture, roadmap, and tradeoffs. Decisions move faster and designs stay consistent. Large open-source efforts juggle many voices, which can slow delivery and blur design.

Choose the assurance model that fits your risk. Community stewardship offers transparency and shared responsibility. Our model adds contractual guarantees, professional assurance, and direct accountability backed by dedicated resources.

Cost

Look past sticker price to total cost of ownership (TCO).

Open source

TCO includes hiring in-house experts who contribute upstream to unblock features and address security issues.

Commercial source

We fold those operational costs into a predictable subscription or license. You get SLAs, legal indemnification, and dedicated support that map cleanly to enterprise procurement and risk frameworks.

In short: invest in internal capability and control, or buy a service-backed solution with predictable costs and clear responsibility.

Formal Grammar Spec