Overview

Aela is a commercial-source language for embedded systems.

Aela is a compiled, memory-safe language with a strong, static type system. It started in 2018 as a fork of Rust, but has diverged significantly to service embedded systems use cases. It has a similar syntax and sticks to many of the same goals such as ownership semantics, memory and concurrency safety, only pay for what you use, and zero-cost abstractions.

Programming Language Landscape

This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.

image.png

Langauge Goals

All language design decisions revolve around determinism and performance for embedded systems.

Aela also focuses on harmony with C and C++. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like write(2) .

Language Goals

All language design decisions revolve around providing absolute determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is eliminated. All excluded features have an ideal alternative (see documentation) or have been simply omitted.

Excluded Feature Justification
Panics Panics are not in the type signature; they violate the principle of abstraction and create a hidden, unrecoverable failure path that bypasses the type system.
Exceptions Exceptions create hidden, non-local control flow paths that are impossible to reason about statically and incur runtime overhead. Error handling must be explicit.
Global State Global variables create hidden dependencies and introduce non-determinism, making concurrency unsafe and program behavior impossible to reason about locally.
Lifetime Annotations Explicit lifetime annotations are a significant source of complexity and syntactic noise. The compiler must be smart enough to infer ownership duration without burdening the programmer.
Macros Macros create non-linear, hard-to-debug code flow ("magic"). Code must be explicit and analyzable; what you see is what the compiler gets, ensuring predictability and toolability.
unsafe keyword The unsafe keyword is an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of unsafe operations rather than entire blocks.
Attributes Attributes are a form of meta-programming that injects non-local behavior and hidden complexity. They modify code in non-obvious ways, violating the principle that code should be explicit.
Pointer Arithmetic Direct pointer manipulation is a primary source of memory safety vulnerabilities (e.g., buffer overflows). Safe, bounds-checked slice operations are the only acceptable alternative.
Advanced Traits Complex trait systems lead to baroque, unreadable type signatures and cryptic compiler errors. Simplicity and clarity are prioritized over abstract expressive power.
Inline Assembly Inline assembly is non-portable, opaque to the optimizer, and breaks static analysis. Low-level routines must be provided via a stable C ABI, ensuring a clean contract.
null keyword Null pointers are the source of countless runtime crashes. The absence of a value must be explicitly represented and handled in the type system (e.g., via Option ).
Operator Overloading Operator overloading makes code ambiguous and hides the cost of operations. Function calls must be explicit to ensure code clarity and predictable performance.
Implicit Conversions Implicit conversions hide potential bugs, such as data truncation or precision loss. All type conversions must be explicit, forcing the programmer to acknowledge the operation.

Feature Comparison

Feature Aela C C++ Rust Ada
Compile-Time Memory Safety √ √ √
Cold Build Speed √ √ √
Reference Counted √ √
Automatic RAII √ √
Formal Verification √ √
Dependent & Refinement Types √
Language-Native Concurrency √
Structured Concurrency √ √
Automatic C/C++ safe binding √

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 won't 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

- /path/to/my-app/index.json
0 {
1 "name" : "my - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae"
4 }

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

- index.json for a project that uses a UI library
0 {
1 "name" : "my - gui - app" ,
2 "version" : "1 . 0 . 0" ,
3 "entry" : "src / app . ae" ,
4 "dependencies" : {
5 "ui" : " . . / libs / aela - ui" ,
6 "database" : " . . / libs / aela - db"
7 }
8 }

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

- ../libs/aela-ui/src/window.ae
0 // This struct can be imported by other modules.
1 export struct WindowOptions {
2 title : string ,
3 width : int ,
4 height : int ,
5 }
6
7 // This function is private to the window.ae module.
8 fn internal_helper ( ) - > void {
9 // ...
10 }

Re-exports

- re-export pattern
0 import { Thing1 , Thing2 } from "things . ae" ;
1
2 export Thing1 ;
3 export Thing2 ;

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

";" lang="" title="Example" id="b68adefb69265">
Example
0 import from " " ;

Example

void { // Access symbols using the `::` namespace operator. let opts: &ui::WindowOptions = new ui::WindowOptions(); helpers::do_something(); }" lang="example" title="- src/app.ae" id="027e17636df19">
- src/app.ae
0 // Import the "ui" package, which was defined in index.json.
1 import ui from "ui" ;
2
3 // Import a local utility file using a relative path.
4 import helpers from " . / helpers . ae" ;
5
6 fn main ( ) - > void {
7 // Access symbols using the `::` namespace operator.
8 let opts : & ui : : WindowOptions = new ui : : WindowOptions ( ) ;
9 helpers : : do_something ( ) ;
10 }

Named Imports

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

Syntax

";" lang="" title="Example" id="9905825be2237">
Example
0 import { , : } from " " ;

Example EXAMPLE

void { // `Window` can be used directly. let win: &Window = new Window(); // `WindowOptions` is available under the alias `Options`. let opts: &Options = new Options(); }" lang="example" title="- src/app.ae" id="3192e955d263e">
- src/app.ae
0 import { Window , WindowOptions : Options } from "ui" ;
1
2 fn main ( ) - > void {
3 // `Window` can be used directly.
4 let win : & Window = new Window ( ) ;
5
6 // `WindowOptions` is available under the alias `Options`.
7 let opts : & Options = new Options ( ) ;
8 }

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

- index.json for an app with native UI code on macOS
0 {
1 "name" : "aela - native - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4 "sources" : {
5 "darwin" : [ "src / native / apple . mm" ]
6 } ,
7 "link" : {
8 "platform" : {
9 "darwin" : [
10 " - framework" , "Foundation" ,
11 " - framework" , "AppKit" ,
12 " - framework" , "ObjectiveC"
13 ]
14 }
15 }
16 }

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.

Failures

A primary cause of software defects, security vulnerabilities, and developer anxiety is the "Trust Gap": the difference between what a function's signature claims it does and what its implementation can actually do. Aela is designed to eliminate this gap. Its error and fault handling system is built on a single, non-negotiable principle: a function's signature must be a complete and honest contract, and the compiler must enforce it.

Don't Try-Catch

Traditional exception systems, common in languages like Java, JavaScript, C++, and Python, introduce a form of hidden control flow. A throw or raise statement is a non-local goto that is often invisible in the function's signature.

Consider a typical function in such a language: function get_user(id: int) -> User

This signature makes a simple promise: "Give me an integer, and I will give you a User." However, the implementation might throw a DatabaseConnectionException, a UserNotFoundException, or a NullPointerException. To understand the function's true behavior, the developer must embark on a research project: reading the documentation (which may be out of date), reading the source code, and reading the source of every function it calls.

This breaks a developer's ability to reason locally about the code.

Don't Panic

Some modern languages, notably Rust, attempt to solve error handling this by creating a two-tiered system:

  • Recoverable Errors ( Result ): For expected failures (e.g., file not found). These are part of the type signature.
  • Unrecoverable Bugs ( panic! ): For programmer errors (e.g., index out of bounds). These are not part of the type signature.

While an improvement, this still creates a hidden side-channel for bugs. More critically, the panic! mechanism creates a deep schism between platforms, especially for embedded systems.

The unwind vs. abort Schism:

On servers, panic! defaults to unwind, a slow and complex process that runs cleanup code (destructors). This adds a significant "tax" to the binary size, which is unacceptable on resource-constrained devices.

On embedded systems, developers are forced to configure panics to abort, which immediately halts the program.

The Broken Promise of abort: When panic = "abort" is used, the language's core safety promise—that resources will be cleaned up on failure (RAII via Drop in Rust)—is broken. Destructors are never called. A MutexGuard will leave a mutex permanently locked. A peripheral that was supposed to be disabled is left in an active state. The very code written to ensure safety on failure becomes useless.

This patched-together model is not a first-principles solution. Aela requires a single, unified system that is safe, deterministic, and efficient on all platforms.

The Fault Model

The Principle of the Honest Contract: Aela avoids ambiguity in failure handling by enforcing that the outcome of a function must be encoded in its signature.

Function Signatures

A function declares its potential to terminate due to an unrecoverable logic bug by using the | operator in its return type. This operator separates the single success type from a list of one or more fault types.

fn get_at(slice: &[u8], index: int) -> u8 | OutOfBounds;

This signature is an honest contract. It tells any caller: "This function will either return a u8 , or it will terminate with an OutOfBounds fault. There are no other possibilities."

The fault and raise Keywords

  • `fault` : A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from struct or enum , which represent data and recoverable errors.
  • fault OutOfBounds(index: int, len: int);
  • `raise` : A keyword that triggers a fault. It immediately stops the current function's execution and propagates the fault to the caller. raise is considered a terminal action.
  • raise OutOfBounds(index: index, len: len);

The Standard match Statement

The match statement is how Aela handles the outcome of functions that may terminate with faults.

Example
0 match ( expression ) {
1 pattern1 = > { . . . } ,
2 pattern2 = > { . . . } , // potentially a fault type!
3 . . .
4 }

Semantic Rules

The safety and special behavior of fault handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:

If the expression being evaluated by a match statement has a fault path in its signature (i.e., contains a | ), then the compiler enforces a "Terminal Arm Rule" on any arm that matches a fault -declared type.

This rule is context-dependent. It is triggered by the signature of the function being called, not just the type of the pattern. This is the key insight that resolves all ambiguity.

The "Terminal Arm Rule" is defined as: The block of the arm must end with a terminal statement. Aela does not have implicit returns, so this is a direct check of the final statement in the block.

Terminal statements are:

  • raise ;
  • std::abort();
  • std::halt();
  • std::reboot();

Note

pure fn ketword must not introduce or handle faults; they cannot have a | in their return type and cannot raise.

Note

Faults must not cross FFI; board/FFI shims must convert faults to domain-appropriate codes or terminals.

Note

AP131 outlines a proposal to have return be the equivalent of raise . Allowing both and specifying that they’re identical.

Note

AP132 outlines a proposal to permit functions to be generic over an open set of faults (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;

Note

AP134 outlines a proposal to add a desugaring operator. let b = get_at(xs, 0)?; // expands to match/raise

Complete Examples: The Rule in Practice

These two examples demonstrate how the context-dependent rule creates a safe and unambiguous system.

Example 1: Handling a Live Fault Event

Example
0 // The compiler sees the '|' in the signature, so it activates the Terminal Arm Rule for this match.
1 match ( create_packet ( user_size ) ) {
2 Some ( packet ) = > { /* This arm is normal. */ } ,
3 None = > { /* This arm is normal. */ } ,
4
5 // The compiler sees that `PacketTooLarge` is a `fault` type and applies the rule.
6 f : PacketTooLarge = > {
7 log : : critical ( "Logic error : Invalid packet size requested . " , f ) ;
8 // The block ends with a known terminal keyword. The code is valid.
9 std : : reboot ( ) ;
10 }
11 }

If reboot; were omitted, the compiler would issue a clear error: "Fault-handling arm must end with a terminal statement."

Example 2: Inspecting a Fault as Data

Example
0 // This function returns a fault object as a value. Its signature has NO '|'.
1 fn inspect_issues ( ) - > PacketTooLarge ;
2
3 // The compiler sees NO '|' in the signature, so it DOES NOT activate the Terminal Arm Rule.
4 match ( inspect_issues ( ) ) {
5
6 // Even though `PacketTooLarge` is a `fault` type, the rule is not active.
7 // This arm is treated as a normal pattern match.
8 f : PacketTooLarge = > {
9 log : : warn ( "A non - critical issue was detected : " , f ) ;
10 // The block is allowed to complete normally. The code is valid.
11 }
12 }

Memory & Mutability

1. Default Allocation Semantics

  • All values start on the stack by default.
  • Stack allocations are:
  • Fast
  • Scoped
  • Owned directly by the binding.
Example
0 let foo : Foo = { num : 0 } ; // Foo is stack-allocated

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.

Example
0 let x : & T = new { . . . val } ; // Allocate on the heap
1 let x : & T = new shared { . . . val } ; // Single-threaded, mutable
2 let x : & T = new shared atomic { . . . val } ; // Thread-safe atomic
3 var x : & T = new weak { . . . val } ; // Mutable weak reference
4 var x : & T = new static { . . . val } ; // New without malloc
5 var x : & T = new static atomic { . . . val } ; // New without malloc, Thread-safe atomic

Behavior of new Modifiers

Modifier Behavior Description
(none) Heap Allocation (OS based allocator). Returns a handle/reference to a freshly allocated object, immutable and can not be loaned.
shared Heap. Shared ownership, single-threaded. Allowed to be loaned; not thread-safe; not Send/Sync-like.
shared atomic Heap. Shared ownership, thread-safe. Reference counts and interior coordination use atomics; Send/Sync if T satisfies the “atomic-safe” requirements you define.
weak Heap, weak handle to a shared object. Does not keep the allocation alive; must be paired with at least one strong shared/shared atomic owner somewhere to be useful.
static Static storage, no OS allocator. Object is placed/constructed in static memory (BSS/RODATA/flash/SECTION), suitable for bare-metal/MCUs. Lifetime: program-long (or until explicitly torn down by system semantics).
static atomic Static storage, thread-safe coordination via atomics. Shared global counters updated in ISR + mainline, Lock-free buffers (ring buffers for UART, DMA, etc.). Configuration/state variables read by multiple cores or ISRs. On a simple single-core MCU with no interrupts, it’s redundant but harmless.
  • 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 :

Keyword Meaning
let Immutable binding (read-only)
var Mutable binding (read-write)
  • The mut keyword is not necesasry here.
  • Mutability is not encoded in types, structs, or fields.
  • let and var are both lexically scoped.

Example

Example
0 let a : & Foo = new shared { . . . foo } ; // Immutable heap reference
1 var b : & Foo = new shared { . . . foo } ; // Mutable heap reference

Note

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

4. Weak References & Cycle Prevention

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'

Example
0 if let strong_ref = weak_ref {
1 // This block only runs if the object is still alive.
2 // 'strong_ref' is a new, temporary strong reference of type &Foo.
3 strong_ref . do_something ( ) ;
4 }

5. Copying Stack Values

  • Heap allocation requires copying the stack value:
Example
0 new shared { . . . foo } // `{ ...foo }` performs a field-wise copy
  • This avoids moving ownership from the stack. Moves are not allowed .

5. Reference Types and Behavior

Kind Syntax RC Type Thread-Safe Mutable
Stack value let x: T = ... None N/A No
Heap reference let x: &T = new shared {...} RC No No
Heap reference (mutable) var x: &T = new shared {...} RC No Yes
Heap reference (atomic) let/var x: &T = new shared atomic {} ARC Yes Depends

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.
a copy of the number 10 is passed. // bar(stack_str); -> a copy of the {ptr, i64} struct is passed." lang="example" title="- Stack Allocated" id="5096a1ef49907">
- Stack Allocated
0 let stack_int : i32 = 10 ; // The variable 'stack_int' IS the number 10.
1 let stack_str : string = "hello" ; // The variable 'stack_str' IS the {ptr, i64} struct.
2
3 // When calling a function:
4 // foo(stack_int); -> a copy of the number 10 is passed.
5 // bar(stack_str); -> a copy of the {ptr, i64} struct is passed.

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.
- Heap allocated via new
0 let heap_int : i32 = new 42 ; // 'heap_int' is a POINTER to a box containing 42.
1 let heap_obj : MyStruct = new { } ; // 'heap_obj' is a POINTER to a box containing a MyStruct.
2 let heap_arr : u8 [ ] = new [ 1 , 2 , 3 ] ; // 'heap_arr' is a POINTER to a box for the array data.
3
4 // When calling a function:
5 // foo(heap_int); -> a copy of the POINTER is passed. The heap data is not touched.

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.
- Special Case
0 let captured_var = new "text" ;
1
2 let my_closure = fn ( ) {
3 print ( captured_var ) ; // Captures the pointer 'captured_var'.
4 } ;
5
6 // 'my_closure' is a {func_ptr, env_ptr} struct.
7 // 'env_ptr' points to a heap box which contains a copy of the 'captured_var' pointer.

Refinement & Dependent Types

TL;DR: Refinement & dependent types are types that embed logical conditions or values themselves, making illegal states unrepresentable by construction.

If you're coming from languages like JavaScript, C++, or Rust, you're used to type systems that check the shape of your data. For example, a type checker ensures you don't use a string where a number is expected.

Aela takes this a step further with refinement types and dependent types . These are features that allow the type system to understand and check the values of your data, not just their shape. It's more rigorous that shape checking, it's a value-aware check that happens entirely at compile time .

Motivation

Most type systems validate shape (ie., "this is an int "). Aela also validates value-level facts : a string is non-empty , an integer is non-zero , a vector’s length matches what your function promises. This turns bugs into compile‑time errors and makes code self-documenting.

  • Earlier feedback: logical mistakes become type errors you see during compilation.
  • Stronger intent: types like NonEmptyString and NonZeroint tell the reader (and the compiler) exactly what you mean.
  • Confidence: fewer defensive checks sprinkled across your code.

Compile-Time VS. Run-Time Arguments

Aela uses a single parameter list for functions, with an optional compile-time section separated from the run-time section by a semicolon ; . Parameters are separated by commas. If a parameter has a type annotation, it will be considered a value parameter. If a value has no type annotation, it will be considered a type.

Example
0 fn f ( T , U ; x : T , y : U ) - > T { return x ; }
1 └┬─┘ └┬───────┘
2 │ └─ Run - Time Parameters
3 └─ Compile - Time Parameters
4
5 fn g ( T ; ) - > T { . . . } // Compile-Time Only (rare but allowed; note trailing `;`)
6 fn h ( x : i32 ) - > i32 { return x ; } // Run Time Only (no `;`)

Rules

  • Tokens before ; are compile-time parameters (type or const/value-level),
  • Type parameters: bare identifiers (ie., T , U ).
  • Const parameters: Name: Type form (ie., N: int ).
  • Tokens after ; are run-time parameters (the usual name: Type , with optional mut / spread, per language rules).
  • If there’s no ; , the entire list is treated as run-time parameters.
  • If the CT part is empty , omit ; (preferred style). If the RT part is empty and CT is present, keep a trailing ; .

Refinement Types: add a where -clause to any base type

A refinement type is a base type with a logical predicate.

Syntax : { id: Type where predicate }

Example
0 // A string that must be non-empty
1 type NonEmptyString = { s : string where std : : length ( s ) > 0 } ;
2
3 let good : NonEmptyString = "Aela" ; // ok
4 let bad : NonEmptyString = "" ; // compile-time error

Use refinements when you want value-aware validation while keeping the underlying representation.

Note

The compiler statically checks predicates where it can (literals, constant expressions, and facts learned from prior code/contracts). When a predicate can’t be decided statically, you’ll provide evidence (see “Proving facts to the compiler”).

Dependent Types: when types mention values

A dependent type is a type that depends on values .

A simple, practical pattern is to refine a function’s return by its inputs :

Example
0 fn add ( a : i32 , b : i32 ) - > { r : i32 where r = = a + b } {
1 return a + b ;
2 }

Here the return type depends on the run-time values a and b . The compiler enforces this contract at compile time wherever it can be proven, and narrows follow-up reasoning.

Another common pattern uses compile-time const parameters to index types:

Example
0 // Conceptual example; CT params appear before `;`
1 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) {
2 // implementation builds a vector whose length is M+N
3 }
  • T is a type parameter .
  • M and N are const parameters (compile-time integers).
  • The result type’s length computes to M + N at the type level .

Proving facts to the compiler

There are three common ways to convince the compiler of a refinement:

  1. Literals and constant expressions — obvious at compile time:
Example
0 let z : NonZeroint = 10 ; // trivially valid
  1. Local reasoning / guards — use a guard to establish a fact for a scope:
Example
0 fn safe_head ( xs : string [ ] ) - > { s : string where std : : length ( s ) > 0 } {
1 if ( std : : length ( xs ) > 0 ) {
2 return xs [ 0 ] ; // compiler knows length(xs) > 0 in this block
3 } else {
4 // handle empty case or return an option/result type
5 }
6 }
  1. Type-level contracts — express properties in the type and let the compiler check uses:
Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }
3 // Callers must provide evidence that `d != 0`.

Note

In more advanced code, system properties and invariants (see KW_REQUIRES , KW_ENSURES , KW_INVARIANT ) can encode broader guarantees, which the compiler uses as facts within the relevant scope.

End‑to‑End: making division-by-zero impossible

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( numer : i32 , denom : NonZeroint ) - > i32 {
3 return numer / denom ;
4 }
5
6 let a : i32 = 100 ;
7 let b : NonZeroint = 10 ; // proven at compile time
8 let ok = safe_divide ( a , b ) ; // compiles
9
10 let c : i32 = 0 ;
11 let err = safe_divide ( a , c ) ; // type error: expected NonZeroint, got i32

Parameter List: full spec (informal)

Example
0 // Declarations
1 fn name ( CT ; RT ) - > Ret { . . . }
2 fn name ( RT ) - > Ret { . . . } // no CT part → omit `;`
3 fn name ( CT ; ) - > Ret { . . . } // CT-only (allowed)
4
5 // CT parameters
6 typeparam : : = IDENTIFIER // ie., T, U
7 constparam : : = IDENTIFIER ':' Type // ie., N: int, K: U64
8 CT : : = typeparam | constparam ( ',' . . . )
9
10 // RT parameters
11 param : : = [ '...' ] [ 'mut' ] IDENTIFIER ':' Type
12 RT : : = param ( ',' . . . )

Validation

  • The CT side only accepts type/const parameters (no mut , no spreads).
  • The RT side accepts ordinary parameters.
  • A single top‑level ; within the parentheses splits CT from RT.
  • Style: omit an empty CT (; ...) — prefer just ( ... ) .

Choosing Refinement vs. Dependent

Use refinement types when:

  • You’re constraining a familiar base type ( i32 , string , a struct) with a predicate ( n != 0 , len(s) > 0 ).
  • You want to reuse existing APIs with stronger safety.

Use dependent types when:

  • The shape of your result depends on inputs (lengths, indices, protocol states).
  • You have natural compile-time parameters (ie., a block size N: int ).

They compose well: dependent function types can return refinement types, and vice versa.

Error messages (ergonomics)

  • CT/RT mixup : “Compile-time parameter list may only contain type/const parameters.”
  • Missing `;` : If the first parameter looks like a type/const param ( T or N: int ), suggest adding the ; .
  • Unproven refinement : Point to the predicate and suggest guards or helper constructors to provide evidence.

FAQ

Q: Do I have to write CT parameters at call sites? A: Typically no — they’re inferred from RT arguments and expected return types. You can guide inference via annotations.

Q: Can I have multiple `;`? A: No. There is at most one top‑level ; per parameter list.

Q: Are const parameters immutable? A: Yes. They are compile-time values; mutability doesn’t apply.

Q: What about async/pure/thread modifiers? A: These work unchanged and apply to the function as a whole; the ; split only affects parameter binding.

Worked examples (with ; )

1) Identity with a type parameter

Example
0 fn id ( T ; x : T ) - > T { return x ; }

2) Map over a vector (type‑level only)

Example
0 fn map ( T , U ; f : fn ( T ) - > U , xs : Vec ( T ) ) - > Vec ( U ) { . . . }

3) Concat with const lengths (conceptual)

Example
0 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) { . . . }

4) Safe division with a refinement type

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }

Function Types

Why functions feel like they have “colors” (and how Aela fixes it)

Many languages split the world into synchronous and asynchronous functions. That split tends to spread—call sites, types, libraries—until everything is “[colored][1].” Aela acknowledges that programs have different execution disciplines (purity, async, thread-safety), then solves the composition pain with first-class types , clear call rules , and built‑in intrinsics so you can cross boundaries intentionally and safely.

At a glance:

  • Three disciplines (colors): pure , thread , async .
  • Simple call rules enforced by the checker.
  • Intrinsic adapters (escape hatches) to cross colors when needed.
  • Contracts ( requires / ensures ) and system blocks to guard risky crossings.

The three disciplines

pure

  • What it means: No observable side effects; referentially transparent.
  • When to use: Deterministic computation, validation, transforms.
  • Gotchas: Cannot call async or impure functions. May be combined with thread if the work is offloaded safely.

thread

  • What it means: Safe to run off the main executor (e.g., in a worker). No ambient event‑loop assumptions; data must be sendable or shared safely.
  • When to use: CPU‑bound work, blocking IO wrapped properly, parallelizable tasks.
  • Combines with: pure (i.e., pure thread fn ).

async

  • What it means: May suspend at await points, returns a future/awaitable.
  • When to use: IO‑bound workflows, coordination with timers, event‑driven code.
  • Note: async is not pure . It stands alone.

Call rules (the short version)

  • pure → may call only pure .
  • thread → may call thread or pure ; invoking a thread fn yields a Task handle.
  • uncolored (impure) → may call thread / pure directly and async via intrinsic.
  • async → may await other async functions or Task handles, and also call pure / thread without suspension.
  • await is legal inside both async fn and thread fn , because awaiting a Task join or future is permitted in either discipline.

Note

The checker gives precise diagnostics and suggests the right intrinsic when you cross a boundary.

Function types are first‑class

Aela’s type system includes function types with their discipline. These are expressed with refinement/dependent types instead of generics:

Example
0 pure fn ( x : u32 ) - > u32
1 thread fn ( bytes : Bytes ) - > Digest
2 async fn ( path : Path ) - > Result ( file : File , err : IoError )

Function parameters can carry refinements on their arguments or return types, e.g.:

Example
0 pure fn ( n : int where n > 0 ) - > Factorial ( n )

This makes intrinsics predictable and type‑safe, without requiring a generic system.

Crossing boundaries: standard intrinsics

To make crossing disciplines predictable and ergonomic, Aela ships intrinsics in the standard library:

Example
0 std : : concurrency : : to_threaded
1 std : : concurrency : : to_async
2 std : : concurrency : : to_blocking
3 std : : concurrency : : detach
4 std : : concurrency : : join

These are typed adapters that the checker understands.

Signatures & typing rules (no generics required)

Aela doesn’t need parametric generics here—these intrinsics are schematic over types and use refinement/dependent predicates to express constraints. We write them informally as “for any types X, Y…”, and the checker discharges the side conditions.

`to_threaded` *

Example
0 // for any types X, Y
1 // Preferred: lift pure/CPU-bound work onto a worker pool
2 fn to_threaded ( f : pure fn ( X ) - > Y ) - > thread fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )
4
5 // Also allowed (impure function), with the same sendability requirements
6 fn to_threaded ( f : fn ( X ) - > Y ) - > thread fn ( X ) - > Y
7 where Sendable ( X ) & & Sendable ( captures ( f ) )

Checks: argument and captured values must be sendable or shared/atomic . No reliance on an ambient event loop.

`to_async` *

Example
0 // for any types X, Y
1 fn to_async ( f : thread fn ( X ) - > Y ) - > async fn ( X ) - > Y
2
3 // Lifts a plain sync function too (discouraged unless necessary)
4 fn to_async ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
5 where Sendable ( X ) & & Sendable ( captures ( f ) )

Runtime model: schedules on the blocking/CPU pool; if the pool is saturated, the returned future suspends until capacity is available.

`to_blocking` * (the common case inside async )

Example
0 // for any types X, Y
1 // Inside async: run synchronous work without stalling the event loop
2 fn to_blocking ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )

This is analogous to Rust Tokio’s `block_in_place`: it yields to the scheduler and executes on the blocking pool.

`block_on` * (drive async to completion from a worker thread)

Example
0 // for any type T
1 fn block_on ( fut : async fn ( ) - > T ) - > thread fn ( ) - > T

Policy: Forbidden on the event‑loop thread; prefer to_async / to_blocking when in async contexts.

`detach` / `join` *

Example
0 type Handle ( T )
1 fn detach ( fut : async fn ( ) - > T ) - > Handle ( T )
2 fn join ( h : Handle ( T ) ) - > async fn ( ) - > T

Diagnostics you’ll see

  • “Argument to `to_threaded` captures non‑sendable state Rc(T).”
  • “`to_blocking` called from non‑async context.”
  • “Pool saturated: `to_async` may suspend until space frees up.”

Examples

CPU work from async (don’t block the loop):

Example
0 async fn load_and_hash ( path : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( path ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 return digest ;
4 }

Submit a threaded task and await the handle:

Example
0 let t : Task ( Digest ) = to_threaded ( compute_hash ) ( bytes ) ;
1 let d : Digest = await t ; // structured join

Drive async to completion from a worker thread:

Example
0 thread fn load_cfg_sync ( ) - > Config {
1 std : : concurrency : : block_on ( load_cfg_async ) ( )
2 }

Lift pure compute to workers:

Example
0 pure fn sum ( xs : & [ i32 ] ) - > i32 { /* ... */ }
1 let task : Task ( i32 ) = std : : concurrency : : to_threaded ( sum ) ( nums ) ;
2 let result : i32 = await task ;

Use blocking work from async:

Example
0 async fn hash_file ( p : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( p ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 digest
4 }

Use `to_async` to present sync/threaded as async:

Example
0 thread fn compress ( data : Bytes ) - > Bytes { /* CPU intensive */ }
1
2 async fn upload ( path : string ) - > Result ( Url , IoError ) {
3 let compressed = await std : : concurrency : : to_async ( compress ) ( await read_file ( path ) ) ;
4 return await send_to_server ( compressed ) ;
5 }

Detached background task:

Example
0 let h = std : : concurrency : : detach ( expensive_build ( ) ) ;
1 await std : : concurrency : : join ( h ) ;

Idioms and examples

  • Keep core transforms pure , wrap with intrinsics at the edges.
  • Use thread { ... } blocks for structured parallelism; all tasks inside must complete before exit.
  • Use std::select to race multiple async sources and cancel losers automatically.

FFI without foot‑guns

Declare foreign functions with explicit disciplines and refinements:

Example
0 ffi read_file = async fn ( path : string where exists ( path ) ) - > Result ( string , IoError )

Then wrap with system policies to guard where they are allowed:

parse_config } }" lang="aela" title="Example" id="8c9dff8f39f5b">
Example
0 system IO {
1 action ReadConfigAllowed ( ) - > Config
2 requires io_capability ( )
3 { await read_file ( " / etc / app . json" ) . ? | > parse_config }
4 }

Concurrency & mutability

  • Use shared / atomic types for cross‑thread data.
  • thread functions may operate on shared safely.
  • pure functions must not mutate shared state.

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.”
&Self T { return &self.0; } fn other(self: &Self as S, other: &Self as O) -> &O T { return &other.0; } } fn demo_methods() { let p1: Pair(int) = (1, 2); let p2: Pair(int) = (3, 4); let r1 = p1.first(); let r2 = p1.other(&p2); print(r1); print(r2); } // 4) Higher-order function: label flows through function type fn map_head(xs: &Vec(T) as A, f: Fn(&A T) -> U) -> &A U { return f(&xs[0]); } fn demo_hof() { let nums: Vec(int) = [1, 2, 3]; let head_ref = map_head(&nums, fn(x: &int) -> &int { return x; }); print(head_ref); } // 5) Multiple inputs require label: `as A` disambiguates the return fn pick(a: &T as A, b: &T) -> &A T { // body could choose either; label tells the checker the result is tied to `a` return a; } // 6) Optional: Outlives relation (advanced) fn choose_longer(a: &T as X, b: &T as Y) -> &X T where Y : X { return a; } // 7) Struct constructor with label reuse struct Window(T) { head: &A T, tail: &B T } fn mk_window(xs: &Vec(T) as A, ys: &Vec(T) as B) -> Window(T) { return Window { head: &xs[0], tail: &ys[0] }; } fn demo_window() { let xs: Vec(int) = [1,2,3]; let ys: Vec(int) = [4,5,6]; let w = mk_window(&xs, &ys); print(w.head); print(w.tail); } // 8) Diagnostics-friendly failure (commented): // fn bad_pick(a: &T, b: &T) -> &T { // if cond { return a; } else { return b; } // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`. // }" lang="aela" title="Example" id="afc4d82ee77ff">
Example
0 // 1) Disambiguate which input a returned reference is tied to
1 fn first_of_two ( a : & T as A , b : & T ) - > & A T {
2 return a ;
3 }
4
5 fn demo_first_of_two ( ) {
6 let x : int = 10 ;
7 let y : int = 20 ;
8 let rx = & x ;
9 let ry = & y ;
10
11 let r = first_of_two ( rx , ry ) ;
12 print ( r ) ;
13 }
14
15 // 2) Struct field referencing an argument via label
16 struct View ( T ) { data : & A T }
17
18 fn make_view ( x : & T as A ) - > View ( T ) {
19 return View { data : x } ;
20 }
21
22 fn demo_view ( ) {
23 let s : string = "hello" ;
24 let v = make_view ( & s ) ;
25 print ( v . data ) ;
26 }
27
28 // 3) Methods: implicit Self label + explicit labels to disambiguate
29 impl Pair ( T ) {
30 fn first ( self : & Self ) - > & Self T {
31 return & self . 0 ;
32 }
33
34 fn other ( self : & Self as S , other : & Self as O ) - > & O T {
35 return & other . 0 ;
36 }
37 }
38
39 fn demo_methods ( ) {
40 let p1 : Pair ( int ) = ( 1 , 2 ) ;
41 let p2 : Pair ( int ) = ( 3 , 4 ) ;
42
43 let r1 = p1 . first ( ) ;
44 let r2 = p1 . other ( & p2 ) ;
45 print ( r1 ) ;
46 print ( r2 ) ;
47 }
48
49 // 4) Higher-order function: label flows through function type
50 fn map_head ( xs : & Vec ( T ) as A , f : Fn ( & A T ) - > U ) - > & A U {
51 return f ( & xs [ 0 ] ) ;
52 }
53
54 fn demo_hof ( ) {
55 let nums : Vec ( int ) = [ 1 , 2 , 3 ] ;
56 let head_ref = map_head ( & nums , fn ( x : & int ) - > & int { return x ; } ) ;
57 print ( head_ref ) ;
58 }
59
60 // 5) Multiple inputs require label: `as A` disambiguates the return
61 fn pick ( a : & T as A , b : & T ) - > & A T {
62 // body could choose either; label tells the checker the result is tied to `a`
63 return a ;
64 }
65
66 // 6) Optional: Outlives relation (advanced)
67 fn choose_longer ( a : & T as X , b : & T as Y ) - > & X T where Y : X {
68 return a ;
69 }
70
71 // 7) Struct constructor with label reuse
72 struct Window ( T ) { head : & A T , tail : & B T }
73
74 fn mk_window ( xs : & Vec ( T ) as A , ys : & Vec ( T ) as B ) - > Window ( T ) {
75 return Window { head : & xs [ 0 ] , tail : & ys [ 0 ] } ;
76 }
77
78 fn demo_window ( ) {
79 let xs : Vec ( int ) = [ 1 , 2 , 3 ] ;
80 let ys : Vec ( int ) = [ 4 , 5 , 6 ] ;
81 let w = mk_window ( & xs , & ys ) ;
82 print ( w . head ) ;
83 print ( w . tail ) ;
84 }
85
86 // 8) Diagnostics-friendly failure (commented):
87 // fn bad_pick(a: &T, b: &T) -> &T {
88 // if cond { return a; } else { return b; }
89 // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`.
90 // }

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

Example
0 let s : string = "hi" ;
1 let r = & s ; // borrow starts
2 print ( r ) ; // last use of r
3 var t = s ; // OK allowed: r’s region ended at last use (lexically-free)

L1 — Loan Creation

Example
0 var x : int = 0 ;
1 let r = & x ; // L(x, shared)
2 let m = & mut x ; // Not OK conflict later under A1, but creation itself establishes L(x, unique)

L2 — Loan Propagation

Example
0 fn id_ref ( p : & int ) - > & int { p }
1 let x : int = 1 ;
2 let r1 = & x ; // L(x, shared)
3 let r2 = id_ref ( r1 ) ; // loan propagates to r2 until last use
4 print ( r2 ) ; // OK!

A1 — Unique Exclusivity

Example
0 var v : int = 0 ;
1 let m = & mut v ; // L(v, unique)
2 let r = & v ; // Not OK! A1: unique excludes any concurrent shared borrow

A2 — Shared Read‑Only

Example
0 var n : int = 0 ;
1 let a = & n ; // L(n, shared)
2 let b = & n ; // another shared loan
3 print ( * a + * b ) ; // OK! reads allowed
4 n = 5 ; // Not OK! A2: write while shared loans alive

I1 — Write Invalidates

Example
0 var s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ;
3 s . push ( " ! " ) ; // Not OK! I1: write to s while shared loan alive (if r not yet last‑used)

I2 — Move Invalidates

Example
0 var s : string = "a" ;
1 let r = & s ; // L(s, shared)
2 var t = s ; // Not OK! I2: move invalidates loans; r would dangle

I3 — Overlap/Fields

Example
0 struct P { x : int , y : int }
1 var p : P = P { x : 1 , y : 2 } ;
2 let mx = & mut p . x ; // L(p.x, unique)
3 let my = & mut p . y ; // OK, disjoint fields: allowed
4
5 var arr : [ int ; 3 ] = [ 0 , 1 , 2 ] ;
6 let a = & mut arr [ 0 ] ;
7 let b = & mut arr [ 1 ] ; // not OK, if indices distinct constants
8 let i = 0 ; let j = read_index ( ) ;
9 let c = & mut arr [ i ] ;
10 let d = & mut arr [ j ] ; // Not OK conservatively, may overlap unless proven disjoint (use split helpers)

U1 — Use Requires Alive

Example
0 let s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ; // OK! use while alive
3 // after last use r ends; any further use would be not OK (dead borrow)

U2 — No After‑Free

Example
0 fn bad ( ) {
1 let s : string = "x" ;
2 let r = & s ;
3 drop ( s ) ; // base place dead
4 print ( r ) ; // Not OK: U2: use after base death
5 }

RB1 — Shared from Unique

Example
0 var v : int = 0 ;
1 let mu = & mut v ; // L(v, unique)
2
3 // Shared reborrow of the same place (auto-deref from &mut int to int)
4 let rs : & int = & mu ; // creates L(v, shared)
5
6 print ( rs ) ;
7
8 // Write through the unique borrow (auto-deref on assignment)
9 mu = 3 ; // must end shared loan before writing via `mu`

RB2 — Unique from Unique (optional v1)

Example
0 var v : int = 0 ;
1 let mu1 = & mut v ;
2 let mu2 = & mut mu1 ; // unique reborrow of v; allowed only if no overlapping use via mu1

E1 — No Escaping Borrows

Example
0 fn leak_ref ( ) - > & int {
1 let x : int = 1 ;
2 return & x ; // Not OK! Escapes to caller; Not OK, dies at function end
3 }
4
5 fn head ( s : & string ) - > & char {
6 return & s [ 0 ] ;
7 } // OK! Summary ties return to arg

M1 — Binding Mutability

Example
0 let x : int = 0 ;
1 let rx = & mut x ; // Not OK: M1: &mut requires mutable base
2 var y : int = 0 ;
3 let ry = & mut y ; // OK

M2 — No Shared Mutability Without Atomics

Example
0 shared var n : int = 0 ; // shared location
1 let r1 = & n ; let r2 = & n ; // shared borrows
2 n = n + 1 ; // Not OK concurrent write without atomic discipline
3 atomic var a : int = 0 ; // with atomic, writes are allowed by policy

T1 — Temporaries

Example
0 print ( & ( make_string ( ) ) ) ; // OK temporary lives through call; reference dies at last use
1 let r = & ( make_string ( ) ) ;
2 print ( r ) ; // Not OK if r would outlive the temporary’s last use

T2 — Branches/Loops/Match

Example
0 let s : string = "x" ;
1 let r = & s ;
2 if cond { print ( r ) ; } else { print ( r ) ; }
3 // r is used on both paths; live set at join = intersection ⇒ still alive until after the if
4 var t = s ; // not OK must occur after r’s last use on all paths

F1 — FFI Preconditions

Example
0 ffi puts : ( & char ) - > int = . . . ;
1 let s : string = "hi" ;
2 let r = & s [ 0 ] ;
3 puts ( r ) ; // OK if FFI summary: does not retain; Not OK if it may retain (escape)

F2 — FFI Postconditions

Example
0 ffi c_strchr : ( & char , int ) - > & char = . . . ; // trusted: result aliases input
1
2 fn first_a ( s : & string ) - > & char {
3 c_strchr ( & s [ 0 ] , 'a' ) // OK allowed only because summary ties result to arg region
4 }

RFT1 — Refinement Well‑Formedness

Example
0 let x : int = 5 ;
1 let y : { z : & int where initialized ( z ) } = { z : & x } ; // OK predicate references lifetime‑relevant property

RFT2 — Discharge at Use Sites

Example
0 fn show ( p : { z : & int where not_escaped ( z ) } ) - > void {
1 print ( p . z ) ; // OK! checker discharges `not_escaped` from current loan facts
2 }

inter‑Procedural Summary (Elision)

Example
0 fn get_first ( a : & [ int ] ) - > & int {
1 return & a [ 0 ] ;
2 }
3
4 // elaborated internally: for<ρ> fn(&ρ [int]) -> &ρ int
5 // caller instantiates ρ from its argument; return tied to same ρ

Structs with Reference Fields (Implicit Regions)

Example
0 struct Node ( T ) { data : & T } // elaborates to Node<ρ, T>
1
2 fn demo ( ) - > void {
3 let x : int = 1 ;
4 var n : Node ( int ) = Node { data : & x } ; // OK n: Node<ρx, int>
5 }
6
7 fn bad ( ) - > void {
8 var n : Node ( int ) ;
9
10 {
11 let x : int = 1 ;
12 n = Node { data : & x } ; // Not OK n outlives x ⇒ region check fails
13 }
14 }

Async Phase 1 — No Unique Loans Across Await

Example
0 async fn step ( mut v : & int ) - > void {
1 let m = v ; // borrow unique via parameter
2 await tick ( ) ; // Not OK, unique loan across await in phase 1
3 }

Closures — Capture Classification

void { move x }; // by‑value move ⇒ FnOnce" lang="aela" title="Example" id="e459ee693aab5">
Example
0 var n : int = 0 ;
1 let c1 = fn ( ) - > void { print ( & n ) ; } ; // shared borrow capture ⇒ Fn
2 let c2 = fn ( ) - > void { n = n + 1 ; } ; // unique borrow capture ⇒ FnMut
3 let x : string = "hi" ;
4 let c3 = fn ( ) - > void { move x } ; // by‑value move ⇒ FnOnce

RTOS Harmony

Linux Setup

You most likely need to edit your udev rules

Example
0 sudo curl - L - o / etc / udev / rules . d / 50 - cmsis - dap . rules \
1 https : / / raw . githubusercontent . com / pyocd / pyOCD / main / udev / 50 - cmsis - dap . rules

If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.

Example
0 lsusb | grep - iE 'arduino|cmsis|dap|renesas'
1 Bus 001 Device 005 : ID 2341 : 1002 Arduino SA . . .

Replace ID VVVV:PPPP

Example
0 # Arduino UNO R4 WiFi (CMSIS-DAP) — custom rule
1 SUBSYSTEM = = "usb" , ATTR { idVendor } = = "VVVV" , ATTR { idProduct } = = "PPPP" , MODE : = "0666"
2 SUBSYSTEM = = "hidraw" , ATTRS { idVendor } = = "VVVV" , ATTRS { idProduct } = = "PPPP" , MODE : = "0666"

Reload, re-enumerate

Example
0 sudo udevadm control - - reload - rules
1 sudo udevadm trigger

Unplug & Replug, press the reset button & then check:

Example
0 pyocd list

Zephyr

Install

Example
0 git cmake ninja python python - pip dtc wget

Install the Zephyr CLI tool

Example
0 pip install west

Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.

Example
0 sudo usermod - a - G dialout $USER

Create a project directory. Create a python environment in the project directory. Initialize it as a new zephyr project. Run the update command to get all the sub-repos.

Example
0 mkdir ~ / projects / z
1 python - m venv ~ / projects / z / . venv
2 west init ~ / projects / z
3 west update

Go back to your projects root and get the minimal SDK for cross compiling.

Example
0 cd ~ / projects
1 wget https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz

Calculate the SHA sum if you want

Example
0 wget - O - https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / sha256 . sum | shasum - - check - - ignore - missing

Extract the SDK and run the setup

Example
0 tar xvf zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz
1 cd ~ / projects / zephyr - sdk - 0 . 17 . 4
2 . / setup . sh

Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)

Example
0 # 1. Navigate to your project directory
1 cd ~ / projects / z
2
3 # 2. Activate the Python virtual environment for 'west'
4 source . / . venv / bin / activate
5
6 # 3. Manually export the SDK path to ensure it's found
7 export ZEPHYR_SDK_INSTALL_DIR = ~ / projects / zephyr - sdk - 0 . 17 . 4
8
9 # 4. Source the Zephyr environment to link everything together
10 source . / zephyr / zephyr - env . sh
11
12 # 5. Install a shit ton of dependencies
13 pip - 3 install - r zephyr / scripts / requirements . txt

Compile & Flash Test

Finally, build an Arduino image. I use Blinky here because its super simple and makes sense to start with as a sanity test.

Example
0 west build - p auto - b arduino_uno_r4 zephyr / samples / blinky
1 west flash

Integrating with Aela

Aela can output object files, so it's very simple to create a Zephyr project with Aela by just adding CMakeLists.txt and prj.conf files.

Example
0 myapp /
1 ├─ CMakeLists . txt
2 ├─ prj . conf
3 ├─ index . json
4 └─ index . ae

Example prj.conf

Example
0 # Prefer minimal libc over newlib (if you don’t need full POSIX/locale/etc.)
1 CONFIG_NEWLIB_LIBC = n
2 CONFIG_MINIMAL_LIBC = y
3 # If you must use newlib, at least disable float printf/scanf:
4 # CONFIG_NEWLIB_LIBC_FLOAT_PRINTF=n
5 # CONFIG_NEWLIB_LIBC_FLOAT_SCANF=n
6
7 # Logging/printk/console (turn off what you don't need)
8 CONFIG_PRINTK = n
9 CONFIG_LOG = n
10 # or, if you need logs:
11 # CONFIG_LOG=y
12 # CONFIG_LOG_MODE_MINIMAL=y
13 # CONFIG_LOG_DEFAULT_LEVEL=0
14
15 # Shell/console features often sneak in via defaults
16 CONFIG_CONSOLE = n
17 CONFIG_UART_CONSOLE = n
18 CONFIG_SHELL = n
19
20 # Link-time optimization can trim more
21 CONFIG_LTO = y
22 CONFIG_SIZE_OPTIMIZATIONS = y
23
24 # Assertions & debug
25 CONFIG_ASSERT = n
26 CONFIG_DEBUG = n
27 CONFIG_DEBUG_INFO = n # (debug symbols only affect .elf, not .bin size)
28
29 # Heap & stacks
30 CONFIG_HEAP_MEM_POOL_SIZE = 0 # if you don’t malloc at all
31 CONFIG_MAIN_STACK_SIZE = 1024 # tune as low as your app can tolerate

Example CMakeLists.txt

${AELA_OBJ}" VERBATIM ) add_library(aela_objects OBJECT ${AELA_OBJ}) set_source_files_properties(${AELA_OBJ} PROPERTIES GENERATED TRUE) # Link your Aela object (contains `main`) into the Zephyr app target_link_libraries(app PRIVATE aela_objects)" lang="cmake" title="Example" id="2051be01a6894">
Example
0 cmake_minimum_required ( VERSION 3 . 20 )
1 find_package ( Zephyr REQUIRED HINTS $ENV { ZEPHYR_BASE } )
2 project ( myapp )
3
4 # You can also pass these with: -DAEC=/path/aec -DAEC_FLAGS="..."
5 set ( AEC "aec" CACHE FILEPATH "Path to Aela compiler" )
6 set ( AEC_FLAGS "" CACHE STRING "Extra flags for Aela" )
7
8 # Optional: mirror Zephyr’s CPU/FPU flags so the .o matches the board ABI
9 # (We read what Zephyr passes to the C toolchain and reuse the ARM-related bits.)
10 get_property ( _Z_OPTS TARGET zephyr_interface PROPERTY INTERFACE_COMPILE_OPTIONS )
11 set ( _AE_ARM_OPTS "" )
12 foreach ( opt IN LISTS _Z_OPTS )
13 if ( opt MATCHES " ^ - m ( cpu | thumb | float - abi | fpu ) " ) ; list ( APPEND _AE_ARM_OPTS "$ { opt } " ) ; endif ( )
14 endforeach ( )
15
16 set ( AELA_SRC $ { CMAKE_CURRENT_SOURCE_DIR } / myprog . ae )
17 set ( AELA_OBJ $ { CMAKE_CURRENT_BINARY_DIR } / aela / myprog . obj . o )
18
19 add_custom_command (
20 OUTPUT $ { AELA_OBJ }
21 COMMAND $ { CMAKE_COMMAND } - E make_directory $ { CMAKE_CURRENT_BINARY_DIR } / aela
22 COMMAND $ { AEC } $ { AEC_FLAGS } $ { _AE_ARM_OPTS } - c $ { AELA_SRC } - o $ { AELA_OBJ }
23 DEPENDS $ { AELA_SRC }
24 COMMENT "Aela : $ { AELA_SRC } - > $ { AELA_OBJ } "
25 VERBATIM
26 )
27
28 add_library ( aela_objects OBJECT $ { AELA_OBJ } )
29 set_source_files_properties ( $ { AELA_OBJ } PROPERTIES GENERATED TRUE )
30
31 # Link your Aela object (contains `main`) into the Zephyr app
32 target_link_libraries ( app PRIVATE aela_objects )

Compiling

Example
0 west build - b arduino_uno_r4_wifi myapp - p \
1 - DCMAKE_EXPORT_COMPILE_COMMANDS = ON \
2 - DAEC = $ ( command - v aec )
3 west flash

Note

The _AE_ARM_OPTS trick copies exactly the -mcpu/-mfpu/-mfloat-abi/-mthumb flags Zephyr uses for this board, so your Aela object links ABI-cleanly without you guessing the right combo. (UNO R4 WiFi is a Cortex-M4; Zephyr’s board page confirms the arch.)

FreeRTOS

Discover Platform Build Flags

Lets assume an Arduino R4 here as an example.

We need to "spy" on the Arduino CLI to get the exact compiler and linker flags required for the R4 WiFi. The Aela build system will pass these directly to its underlyng C compiler. Arduino code files are called "sketches".

  1. Create a dummy sketch:
temp_sketch/temp_sketch.ino" lang="bash" title="Example" id="2274fcd531ebc">
Example
0 mkdir temp_sketch
1 echo " void setup ( ) { } void loop ( ) { } " > temp_sketch / temp_sketch . ino
  1. Run a verbose compile:
Example
0 arduino - cli compile - - fqbn arduino : renesas_uno : unor4wifi - - verbose temp_sketch
  1. Find and copy the linker command. Scroll through the output and find the longest command, which will start with something like .../arm-none-eabi-g++ ... . It will be a very long line that links all the object files and libraries together. Copy this entire command into a text editor. We're going to use its flags.

It will look something like this (shortened for clarity): .../arm-none-eabi-g++ -Os -Wl,--gc-sections -mcpu=cortex-m4 ... -L/path/to/build -Wl,--start-group -lArduinoCore -lrtos -lm -Wl,--end-group ...

We will now transfer the important parts of that command into your index.json .

Step 2: Project Structure

Organize your project with your source code inside a src directory.

Example
0 aela_freertos_blinky /
1 ├── index . json # The project manifest (our main focus)
2 └── src /
3 ├── main . ae # Your Aela application logic
4 └── shim . c # The C entry-point shim

Step 3: The index.json Manifest

This is the control center. We'll define a custom platform target called "arduino_r4" and place all the flags we discovered into the link section.

Create the file `index.json` (unless it was created via aec init ):

Example
0 {
1 "name" : "aela - freertos - blinky" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4
5 "sources" : {
6 "shared" : [
7 "src / shim . c"
8 ]
9 } ,
10
11 "link" : {
12 "platform" : {
13 "arduino_r4" : [
14 " - mcpu = cortex - m4" ,
15 " - mthumb" ,
16 " - mfloat - abi = hard" ,
17 " - mfpu = fpv4 - sp - d16" ,
18
19 " - Os" ,
20 " - Wl , - - gc - sections" ,
21 " - Wl , - - script = / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI / linker_script . ld" ,
22
23 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / cores / arduino" ,
24 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI" ,
25 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / libraries / Arduino_FreeRTOS / src" ,
26
27 " - L / tmp / arduino / build - 123456789 . . . " ,
28
29 " - Wl , - - start - group" ,
30 " - lArduinoCore" ,
31 " - lrtos" ,
32 " - lm" ,
33 " - Wl , - - end - group"
34 ]
35 }
36 }
37 }

Note

You must replace the placeholder paths ( /home/user/... , /tmp/arduino/... ) with the full, absolute paths you copied from your verbose compiler output in Step 1.

Step 4: The Source Code

The source code is the same as before, but now it lives in the src/ directory.

src/main.ae

src/main.ae
0 // FFI Declarations for C functions
1 struct TaskHandle_t ;
2 type TaskFunction_t = fn ( & void ) - > void ;
3
4 ffi pinMode = fn ( u32 , u32 ) - > void ;
5 ffi digitalWrite = fn ( u32 , u32 ) - > void ;
6 ffi xTaskCreate = fn ( TaskFunction_t , string , u32 , & void , u32 , & TaskHandle_t ) - > i32 ;
7 ffi vTaskStartScheduler = fn ( ) - > void ;
8 ffi vTaskDelay = fn ( u32 ) - > void ;
9
10 // Constants
11 let LED_BUILTIN : u32 = 13 ;
12 let OUTPUT : u32 = 1 ;
13 let HIGH : u32 = 1 ;
14 let LOW : u32 = 0 ;
15
16 // The task that will blink the LED.
17 fn blinkTask ( params : & void ) - > void {
18 pinMode ( LED_BUILTIN , OUTPUT ) ;
19 while ( true ) {
20 digitalWrite ( LED_BUILTIN , HIGH ) ;
21 vTaskDelay ( 500 ) ;
22 digitalWrite ( LED_BUILTIN , LOW ) ;
23 vTaskDelay ( 500 ) ;
24 }
25 }
26
27 // Main entry point called from our C shim.
28 export fn aela_rtos ( ) - > void {
29 xTaskCreate ( blinkTask , "Blinker" , 128 , null , 1 , null ) ;
30 vTaskStartScheduler ( ) ;
31 }

src/shim.c

src/shim.c
0 #include
1
2 // Declare the external function defined in our Aela code.
3 extern void aela_rtos ( ) ;
4
5 // Standard Arduino entry point.
6 void setup ( ) {
7 aela_rtos ( ) ;
8 }
9
10 // loop() will never be reached, but must exist to link correctly.
11 void loop ( ) { }

Step 5: Build and Flash

You tell the Aela compiler what you're targeting, and it uses the manifest to set the correct build flags.

Build the project for the target triple:

Example
0 # This command tells Aela to cross-compile for the specified target.
1 # It will then find the "thumbv7em-none-eabihf" key in your index.json.
2 aec build - - platform = "arduino_r4" - - target thumbv7em - none - eabihf

Flash the output. The build process should still result in a .uf2 file in a build directory. You can then flash it with the Arduino CLI as before.

Example
0 arduino - cli upload - - fqbn arduino : renesas_uno : unor4wifi - - input - file build / aela - freertos - blinky . uf2

FAQ

Why is Aela 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.

Overview

Aela is a commercial-source language for embedded systems.

Aela is a compiled, memory-safe language with a strong, static type system. It started in 2018 as a fork of Rust, but has diverged significantly to service embedded systems use cases. It has a similar syntax and sticks to many of the same goals such as ownership semantics, memory and concurrency safety, only pay for what you use, and zero-cost abstractions.

Programming Language Landscape

This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.

image.png

Langauge Goals

All language design decisions revolve around determinism and performance for embedded systems.

Aela also focuses on harmony with C and C++. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like write(2) .

Language Goals

All language design decisions revolve around providing absolute determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is eliminated. All excluded features have an ideal alternative (see documentation) or have been simply omitted.

Excluded Feature Justification
Panics Panics are not in the type signature; they violate the principle of abstraction and create a hidden, unrecoverable failure path that bypasses the type system.
Exceptions Exceptions create hidden, non-local control flow paths that are impossible to reason about statically and incur runtime overhead. Error handling must be explicit.
Global State Global variables create hidden dependencies and introduce non-determinism, making concurrency unsafe and program behavior impossible to reason about locally.
Lifetime Annotations Explicit lifetime annotations are a significant source of complexity and syntactic noise. The compiler must be smart enough to infer ownership duration without burdening the programmer.
Macros Macros create non-linear, hard-to-debug code flow ("magic"). Code must be explicit and analyzable; what you see is what the compiler gets, ensuring predictability and toolability.
unsafe keyword The unsafe keyword is an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of unsafe operations rather than entire blocks.
Attributes Attributes are a form of meta-programming that injects non-local behavior and hidden complexity. They modify code in non-obvious ways, violating the principle that code should be explicit.
Pointer Arithmetic Direct pointer manipulation is a primary source of memory safety vulnerabilities (e.g., buffer overflows). Safe, bounds-checked slice operations are the only acceptable alternative.
Advanced Traits Complex trait systems lead to baroque, unreadable type signatures and cryptic compiler errors. Simplicity and clarity are prioritized over abstract expressive power.
Inline Assembly Inline assembly is non-portable, opaque to the optimizer, and breaks static analysis. Low-level routines must be provided via a stable C ABI, ensuring a clean contract.
null keyword Null pointers are the source of countless runtime crashes. The absence of a value must be explicitly represented and handled in the type system (e.g., via Option ).
Operator Overloading Operator overloading makes code ambiguous and hides the cost of operations. Function calls must be explicit to ensure code clarity and predictable performance.
Implicit Conversions Implicit conversions hide potential bugs, such as data truncation or precision loss. All type conversions must be explicit, forcing the programmer to acknowledge the operation.

Feature Comparison

Feature Aela C C++ Rust Ada
Compile-Time Memory Safety √ √ √
Cold Build Speed √ √ √
Reference Counted √ √
Automatic RAII √ √
Formal Verification √ √
Dependent & Refinement Types √
Language-Native Concurrency √
Structured Concurrency √ √
Automatic C/C++ safe binding √

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 won't 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

- /path/to/my-app/index.json
0 {
1 "name" : "my - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae"
4 }

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

- index.json for a project that uses a UI library
0 {
1 "name" : "my - gui - app" ,
2 "version" : "1 . 0 . 0" ,
3 "entry" : "src / app . ae" ,
4 "dependencies" : {
5 "ui" : " . . / libs / aela - ui" ,
6 "database" : " . . / libs / aela - db"
7 }
8 }

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

- ../libs/aela-ui/src/window.ae
0 // This struct can be imported by other modules.
1 export struct WindowOptions {
2 title : string ,
3 width : int ,
4 height : int ,
5 }
6
7 // This function is private to the window.ae module.
8 fn internal_helper ( ) - > void {
9 // ...
10 }

Re-exports

- re-export pattern
0 import { Thing1 , Thing2 } from "things . ae" ;
1
2 export Thing1 ;
3 export Thing2 ;

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

";" lang="" title="Example" id="b68adefb69265">
Example
0 import from " " ;

Example

void { // Access symbols using the `::` namespace operator. let opts: &ui::WindowOptions = new ui::WindowOptions(); helpers::do_something(); }" lang="example" title="- src/app.ae" id="027e17636df19">
- src/app.ae
0 // Import the "ui" package, which was defined in index.json.
1 import ui from "ui" ;
2
3 // Import a local utility file using a relative path.
4 import helpers from " . / helpers . ae" ;
5
6 fn main ( ) - > void {
7 // Access symbols using the `::` namespace operator.
8 let opts : & ui : : WindowOptions = new ui : : WindowOptions ( ) ;
9 helpers : : do_something ( ) ;
10 }

Named Imports

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

Syntax

";" lang="" title="Example" id="9905825be2237">
Example
0 import { , : } from " " ;

Example EXAMPLE

void { // `Window` can be used directly. let win: &Window = new Window(); // `WindowOptions` is available under the alias `Options`. let opts: &Options = new Options(); }" lang="example" title="- src/app.ae" id="3192e955d263e">
- src/app.ae
0 import { Window , WindowOptions : Options } from "ui" ;
1
2 fn main ( ) - > void {
3 // `Window` can be used directly.
4 let win : & Window = new Window ( ) ;
5
6 // `WindowOptions` is available under the alias `Options`.
7 let opts : & Options = new Options ( ) ;
8 }

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

- index.json for an app with native UI code on macOS
0 {
1 "name" : "aela - native - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4 "sources" : {
5 "darwin" : [ "src / native / apple . mm" ]
6 } ,
7 "link" : {
8 "platform" : {
9 "darwin" : [
10 " - framework" , "Foundation" ,
11 " - framework" , "AppKit" ,
12 " - framework" , "ObjectiveC"
13 ]
14 }
15 }
16 }

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.

Failures

A primary cause of software defects, security vulnerabilities, and developer anxiety is the "Trust Gap": the difference between what a function's signature claims it does and what its implementation can actually do. Aela is designed to eliminate this gap. Its error and fault handling system is built on a single, non-negotiable principle: a function's signature must be a complete and honest contract, and the compiler must enforce it.

Don't Try-Catch

Traditional exception systems, common in languages like Java, JavaScript, C++, and Python, introduce a form of hidden control flow. A throw or raise statement is a non-local goto that is often invisible in the function's signature.

Consider a typical function in such a language: function get_user(id: int) -> User

This signature makes a simple promise: "Give me an integer, and I will give you a User." However, the implementation might throw a DatabaseConnectionException, a UserNotFoundException, or a NullPointerException. To understand the function's true behavior, the developer must embark on a research project: reading the documentation (which may be out of date), reading the source code, and reading the source of every function it calls.

This breaks a developer's ability to reason locally about the code.

Don't Panic

Some modern languages, notably Rust, attempt to solve error handling this by creating a two-tiered system:

  • Recoverable Errors ( Result ): For expected failures (e.g., file not found). These are part of the type signature.
  • Unrecoverable Bugs ( panic! ): For programmer errors (e.g., index out of bounds). These are not part of the type signature.

While an improvement, this still creates a hidden side-channel for bugs. More critically, the panic! mechanism creates a deep schism between platforms, especially for embedded systems.

The unwind vs. abort Schism:

On servers, panic! defaults to unwind, a slow and complex process that runs cleanup code (destructors). This adds a significant "tax" to the binary size, which is unacceptable on resource-constrained devices.

On embedded systems, developers are forced to configure panics to abort, which immediately halts the program.

The Broken Promise of abort: When panic = "abort" is used, the language's core safety promise—that resources will be cleaned up on failure (RAII via Drop in Rust)—is broken. Destructors are never called. A MutexGuard will leave a mutex permanently locked. A peripheral that was supposed to be disabled is left in an active state. The very code written to ensure safety on failure becomes useless.

This patched-together model is not a first-principles solution. Aela requires a single, unified system that is safe, deterministic, and efficient on all platforms.

The Fault Model

The Principle of the Honest Contract: Aela avoids ambiguity in failure handling by enforcing that the outcome of a function must be encoded in its signature.

Function Signatures

A function declares its potential to terminate due to an unrecoverable logic bug by using the | operator in its return type. This operator separates the single success type from a list of one or more fault types.

fn get_at(slice: &[u8], index: int) -> u8 | OutOfBounds;

This signature is an honest contract. It tells any caller: "This function will either return a u8 , or it will terminate with an OutOfBounds fault. There are no other possibilities."

The fault and raise Keywords

  • `fault` : A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from struct or enum , which represent data and recoverable errors.
  • fault OutOfBounds(index: int, len: int);
  • `raise` : A keyword that triggers a fault. It immediately stops the current function's execution and propagates the fault to the caller. raise is considered a terminal action.
  • raise OutOfBounds(index: index, len: len);

The Standard match Statement

The match statement is how Aela handles the outcome of functions that may terminate with faults.

Example
0 match ( expression ) {
1 pattern1 = > { . . . } ,
2 pattern2 = > { . . . } , // potentially a fault type!
3 . . .
4 }

Semantic Rules

The safety and special behavior of fault handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:

If the expression being evaluated by a match statement has a fault path in its signature (i.e., contains a | ), then the compiler enforces a "Terminal Arm Rule" on any arm that matches a fault -declared type.

This rule is context-dependent. It is triggered by the signature of the function being called, not just the type of the pattern. This is the key insight that resolves all ambiguity.

The "Terminal Arm Rule" is defined as: The block of the arm must end with a terminal statement. Aela does not have implicit returns, so this is a direct check of the final statement in the block.

Terminal statements are:

  • raise ;
  • std::abort();
  • std::halt();
  • std::reboot();

Note

pure fn ketword must not introduce or handle faults; they cannot have a | in their return type and cannot raise.

Note

Faults must not cross FFI; board/FFI shims must convert faults to domain-appropriate codes or terminals.

Note

AP131 outlines a proposal to have return be the equivalent of raise . Allowing both and specifying that they’re identical.

Note

AP132 outlines a proposal to permit functions to be generic over an open set of faults (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;

Note

AP134 outlines a proposal to add a desugaring operator. let b = get_at(xs, 0)?; // expands to match/raise

Complete Examples: The Rule in Practice

These two examples demonstrate how the context-dependent rule creates a safe and unambiguous system.

Example 1: Handling a Live Fault Event

Example
0 // The compiler sees the '|' in the signature, so it activates the Terminal Arm Rule for this match.
1 match ( create_packet ( user_size ) ) {
2 Some ( packet ) = > { /* This arm is normal. */ } ,
3 None = > { /* This arm is normal. */ } ,
4
5 // The compiler sees that `PacketTooLarge` is a `fault` type and applies the rule.
6 f : PacketTooLarge = > {
7 log : : critical ( "Logic error : Invalid packet size requested . " , f ) ;
8 // The block ends with a known terminal keyword. The code is valid.
9 std : : reboot ( ) ;
10 }
11 }

If reboot; were omitted, the compiler would issue a clear error: "Fault-handling arm must end with a terminal statement."

Example 2: Inspecting a Fault as Data

Example
0 // This function returns a fault object as a value. Its signature has NO '|'.
1 fn inspect_issues ( ) - > PacketTooLarge ;
2
3 // The compiler sees NO '|' in the signature, so it DOES NOT activate the Terminal Arm Rule.
4 match ( inspect_issues ( ) ) {
5
6 // Even though `PacketTooLarge` is a `fault` type, the rule is not active.
7 // This arm is treated as a normal pattern match.
8 f : PacketTooLarge = > {
9 log : : warn ( "A non - critical issue was detected : " , f ) ;
10 // The block is allowed to complete normally. The code is valid.
11 }
12 }

Memory & Mutability

1. Default Allocation Semantics

  • All values start on the stack by default.
  • Stack allocations are:
  • Fast
  • Scoped
  • Owned directly by the binding.
Example
0 let foo : Foo = { num : 0 } ; // Foo is stack-allocated

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.

Example
0 let x : & T = new { . . . val } ; // Allocate on the heap
1 let x : & T = new shared { . . . val } ; // Single-threaded, mutable
2 let x : & T = new shared atomic { . . . val } ; // Thread-safe atomic
3 var x : & T = new weak { . . . val } ; // Mutable weak reference
4 var x : & T = new static { . . . val } ; // New without malloc
5 var x : & T = new static atomic { . . . val } ; // New without malloc, Thread-safe atomic

Behavior of new Modifiers

Modifier Behavior Description
(none) Heap Allocation (OS based allocator). Returns a handle/reference to a freshly allocated object, immutable and can not be loaned.
shared Heap. Shared ownership, single-threaded. Allowed to be loaned; not thread-safe; not Send/Sync-like.
shared atomic Heap. Shared ownership, thread-safe. Reference counts and interior coordination use atomics; Send/Sync if T satisfies the “atomic-safe” requirements you define.
weak Heap, weak handle to a shared object. Does not keep the allocation alive; must be paired with at least one strong shared/shared atomic owner somewhere to be useful.
static Static storage, no OS allocator. Object is placed/constructed in static memory (BSS/RODATA/flash/SECTION), suitable for bare-metal/MCUs. Lifetime: program-long (or until explicitly torn down by system semantics).
static atomic Static storage, thread-safe coordination via atomics. Shared global counters updated in ISR + mainline, Lock-free buffers (ring buffers for UART, DMA, etc.). Configuration/state variables read by multiple cores or ISRs. On a simple single-core MCU with no interrupts, it’s redundant but harmless.
  • 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 :

Keyword Meaning
let Immutable binding (read-only)
var Mutable binding (read-write)
  • The mut keyword is not necesasry here.
  • Mutability is not encoded in types, structs, or fields.
  • let and var are both lexically scoped.

Example

Example
0 let a : & Foo = new shared { . . . foo } ; // Immutable heap reference
1 var b : & Foo = new shared { . . . foo } ; // Mutable heap reference

Note

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

4. Weak References & Cycle Prevention

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'

Example
0 if let strong_ref = weak_ref {
1 // This block only runs if the object is still alive.
2 // 'strong_ref' is a new, temporary strong reference of type &Foo.
3 strong_ref . do_something ( ) ;
4 }

5. Copying Stack Values

  • Heap allocation requires copying the stack value:
Example
0 new shared { . . . foo } // `{ ...foo }` performs a field-wise copy
  • This avoids moving ownership from the stack. Moves are not allowed .

5. Reference Types and Behavior

Kind Syntax RC Type Thread-Safe Mutable
Stack value let x: T = ... None N/A No
Heap reference let x: &T = new shared {...} RC No No
Heap reference (mutable) var x: &T = new shared {...} RC No Yes
Heap reference (atomic) let/var x: &T = new shared atomic {} ARC Yes Depends

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.
a copy of the number 10 is passed. // bar(stack_str); -> a copy of the {ptr, i64} struct is passed." lang="example" title="- Stack Allocated" id="5096a1ef49907">
- Stack Allocated
0 let stack_int : i32 = 10 ; // The variable 'stack_int' IS the number 10.
1 let stack_str : string = "hello" ; // The variable 'stack_str' IS the {ptr, i64} struct.
2
3 // When calling a function:
4 // foo(stack_int); -> a copy of the number 10 is passed.
5 // bar(stack_str); -> a copy of the {ptr, i64} struct is passed.

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.
- Heap allocated via new
0 let heap_int : i32 = new 42 ; // 'heap_int' is a POINTER to a box containing 42.
1 let heap_obj : MyStruct = new { } ; // 'heap_obj' is a POINTER to a box containing a MyStruct.
2 let heap_arr : u8 [ ] = new [ 1 , 2 , 3 ] ; // 'heap_arr' is a POINTER to a box for the array data.
3
4 // When calling a function:
5 // foo(heap_int); -> a copy of the POINTER is passed. The heap data is not touched.

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.
- Special Case
0 let captured_var = new "text" ;
1
2 let my_closure = fn ( ) {
3 print ( captured_var ) ; // Captures the pointer 'captured_var'.
4 } ;
5
6 // 'my_closure' is a {func_ptr, env_ptr} struct.
7 // 'env_ptr' points to a heap box which contains a copy of the 'captured_var' pointer.

Refinement & Dependent Types

TL;DR: Refinement & dependent types are types that embed logical conditions or values themselves, making illegal states unrepresentable by construction.

If you're coming from languages like JavaScript, C++, or Rust, you're used to type systems that check the shape of your data. For example, a type checker ensures you don't use a string where a number is expected.

Aela takes this a step further with refinement types and dependent types . These are features that allow the type system to understand and check the values of your data, not just their shape. It's more rigorous that shape checking, it's a value-aware check that happens entirely at compile time .

Motivation

Most type systems validate shape (ie., "this is an int "). Aela also validates value-level facts : a string is non-empty , an integer is non-zero , a vector’s length matches what your function promises. This turns bugs into compile‑time errors and makes code self-documenting.

  • Earlier feedback: logical mistakes become type errors you see during compilation.
  • Stronger intent: types like NonEmptyString and NonZeroint tell the reader (and the compiler) exactly what you mean.
  • Confidence: fewer defensive checks sprinkled across your code.

Compile-Time VS. Run-Time Arguments

Aela uses a single parameter list for functions, with an optional compile-time section separated from the run-time section by a semicolon ; . Parameters are separated by commas. If a parameter has a type annotation, it will be considered a value parameter. If a value has no type annotation, it will be considered a type.

Example
0 fn f ( T , U ; x : T , y : U ) - > T { return x ; }
1 └┬─┘ └┬───────┘
2 │ └─ Run - Time Parameters
3 └─ Compile - Time Parameters
4
5 fn g ( T ; ) - > T { . . . } // Compile-Time Only (rare but allowed; note trailing `;`)
6 fn h ( x : i32 ) - > i32 { return x ; } // Run Time Only (no `;`)

Rules

  • Tokens before ; are compile-time parameters (type or const/value-level),
  • Type parameters: bare identifiers (ie., T , U ).
  • Const parameters: Name: Type form (ie., N: int ).
  • Tokens after ; are run-time parameters (the usual name: Type , with optional mut / spread, per language rules).
  • If there’s no ; , the entire list is treated as run-time parameters.
  • If the CT part is empty , omit ; (preferred style). If the RT part is empty and CT is present, keep a trailing ; .

Refinement Types: add a where -clause to any base type

A refinement type is a base type with a logical predicate.

Syntax : { id: Type where predicate }

Example
0 // A string that must be non-empty
1 type NonEmptyString = { s : string where std : : length ( s ) > 0 } ;
2
3 let good : NonEmptyString = "Aela" ; // ok
4 let bad : NonEmptyString = "" ; // compile-time error

Use refinements when you want value-aware validation while keeping the underlying representation.

Note

The compiler statically checks predicates where it can (literals, constant expressions, and facts learned from prior code/contracts). When a predicate can’t be decided statically, you’ll provide evidence (see “Proving facts to the compiler”).

Dependent Types: when types mention values

A dependent type is a type that depends on values .

A simple, practical pattern is to refine a function’s return by its inputs :

Example
0 fn add ( a : i32 , b : i32 ) - > { r : i32 where r = = a + b } {
1 return a + b ;
2 }

Here the return type depends on the run-time values a and b . The compiler enforces this contract at compile time wherever it can be proven, and narrows follow-up reasoning.

Another common pattern uses compile-time const parameters to index types:

Example
0 // Conceptual example; CT params appear before `;`
1 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) {
2 // implementation builds a vector whose length is M+N
3 }
  • T is a type parameter .
  • M and N are const parameters (compile-time integers).
  • The result type’s length computes to M + N at the type level .

Proving facts to the compiler

There are three common ways to convince the compiler of a refinement:

  1. Literals and constant expressions — obvious at compile time:
Example
0 let z : NonZeroint = 10 ; // trivially valid
  1. Local reasoning / guards — use a guard to establish a fact for a scope:
Example
0 fn safe_head ( xs : string [ ] ) - > { s : string where std : : length ( s ) > 0 } {
1 if ( std : : length ( xs ) > 0 ) {
2 return xs [ 0 ] ; // compiler knows length(xs) > 0 in this block
3 } else {
4 // handle empty case or return an option/result type
5 }
6 }
  1. Type-level contracts — express properties in the type and let the compiler check uses:
Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }
3 // Callers must provide evidence that `d != 0`.

Note

In more advanced code, system properties and invariants (see KW_REQUIRES , KW_ENSURES , KW_INVARIANT ) can encode broader guarantees, which the compiler uses as facts within the relevant scope.

End‑to‑End: making division-by-zero impossible

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( numer : i32 , denom : NonZeroint ) - > i32 {
3 return numer / denom ;
4 }
5
6 let a : i32 = 100 ;
7 let b : NonZeroint = 10 ; // proven at compile time
8 let ok = safe_divide ( a , b ) ; // compiles
9
10 let c : i32 = 0 ;
11 let err = safe_divide ( a , c ) ; // type error: expected NonZeroint, got i32

Parameter List: full spec (informal)

Example
0 // Declarations
1 fn name ( CT ; RT ) - > Ret { . . . }
2 fn name ( RT ) - > Ret { . . . } // no CT part → omit `;`
3 fn name ( CT ; ) - > Ret { . . . } // CT-only (allowed)
4
5 // CT parameters
6 typeparam : : = IDENTIFIER // ie., T, U
7 constparam : : = IDENTIFIER ':' Type // ie., N: int, K: U64
8 CT : : = typeparam | constparam ( ',' . . . )
9
10 // RT parameters
11 param : : = [ '...' ] [ 'mut' ] IDENTIFIER ':' Type
12 RT : : = param ( ',' . . . )

Validation

  • The CT side only accepts type/const parameters (no mut , no spreads).
  • The RT side accepts ordinary parameters.
  • A single top‑level ; within the parentheses splits CT from RT.
  • Style: omit an empty CT (; ...) — prefer just ( ... ) .

Choosing Refinement vs. Dependent

Use refinement types when:

  • You’re constraining a familiar base type ( i32 , string , a struct) with a predicate ( n != 0 , len(s) > 0 ).
  • You want to reuse existing APIs with stronger safety.

Use dependent types when:

  • The shape of your result depends on inputs (lengths, indices, protocol states).
  • You have natural compile-time parameters (ie., a block size N: int ).

They compose well: dependent function types can return refinement types, and vice versa.

Error messages (ergonomics)

  • CT/RT mixup : “Compile-time parameter list may only contain type/const parameters.”
  • Missing `;` : If the first parameter looks like a type/const param ( T or N: int ), suggest adding the ; .
  • Unproven refinement : Point to the predicate and suggest guards or helper constructors to provide evidence.

FAQ

Q: Do I have to write CT parameters at call sites? A: Typically no — they’re inferred from RT arguments and expected return types. You can guide inference via annotations.

Q: Can I have multiple `;`? A: No. There is at most one top‑level ; per parameter list.

Q: Are const parameters immutable? A: Yes. They are compile-time values; mutability doesn’t apply.

Q: What about async/pure/thread modifiers? A: These work unchanged and apply to the function as a whole; the ; split only affects parameter binding.

Worked examples (with ; )

1) Identity with a type parameter

Example
0 fn id ( T ; x : T ) - > T { return x ; }

2) Map over a vector (type‑level only)

Example
0 fn map ( T , U ; f : fn ( T ) - > U , xs : Vec ( T ) ) - > Vec ( U ) { . . . }

3) Concat with const lengths (conceptual)

Example
0 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) { . . . }

4) Safe division with a refinement type

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }

Function Types

Why functions feel like they have “colors” (and how Aela fixes it)

Many languages split the world into synchronous and asynchronous functions. That split tends to spread—call sites, types, libraries—until everything is “[colored][1].” Aela acknowledges that programs have different execution disciplines (purity, async, thread-safety), then solves the composition pain with first-class types , clear call rules , and built‑in intrinsics so you can cross boundaries intentionally and safely.

At a glance:

  • Three disciplines (colors): pure , thread , async .
  • Simple call rules enforced by the checker.
  • Intrinsic adapters (escape hatches) to cross colors when needed.
  • Contracts ( requires / ensures ) and system blocks to guard risky crossings.

The three disciplines

pure

  • What it means: No observable side effects; referentially transparent.
  • When to use: Deterministic computation, validation, transforms.
  • Gotchas: Cannot call async or impure functions. May be combined with thread if the work is offloaded safely.

thread

  • What it means: Safe to run off the main executor (e.g., in a worker). No ambient event‑loop assumptions; data must be sendable or shared safely.
  • When to use: CPU‑bound work, blocking IO wrapped properly, parallelizable tasks.
  • Combines with: pure (i.e., pure thread fn ).

async

  • What it means: May suspend at await points, returns a future/awaitable.
  • When to use: IO‑bound workflows, coordination with timers, event‑driven code.
  • Note: async is not pure . It stands alone.

Call rules (the short version)

  • pure → may call only pure .
  • thread → may call thread or pure ; invoking a thread fn yields a Task handle.
  • uncolored (impure) → may call thread / pure directly and async via intrinsic.
  • async → may await other async functions or Task handles, and also call pure / thread without suspension.
  • await is legal inside both async fn and thread fn , because awaiting a Task join or future is permitted in either discipline.

Note

The checker gives precise diagnostics and suggests the right intrinsic when you cross a boundary.

Function types are first‑class

Aela’s type system includes function types with their discipline. These are expressed with refinement/dependent types instead of generics:

Example
0 pure fn ( x : u32 ) - > u32
1 thread fn ( bytes : Bytes ) - > Digest
2 async fn ( path : Path ) - > Result ( file : File , err : IoError )

Function parameters can carry refinements on their arguments or return types, e.g.:

Example
0 pure fn ( n : int where n > 0 ) - > Factorial ( n )

This makes intrinsics predictable and type‑safe, without requiring a generic system.

Crossing boundaries: standard intrinsics

To make crossing disciplines predictable and ergonomic, Aela ships intrinsics in the standard library:

Example
0 std : : concurrency : : to_threaded
1 std : : concurrency : : to_async
2 std : : concurrency : : to_blocking
3 std : : concurrency : : detach
4 std : : concurrency : : join

These are typed adapters that the checker understands.

Signatures & typing rules (no generics required)

Aela doesn’t need parametric generics here—these intrinsics are schematic over types and use refinement/dependent predicates to express constraints. We write them informally as “for any types X, Y…”, and the checker discharges the side conditions.

`to_threaded` *

Example
0 // for any types X, Y
1 // Preferred: lift pure/CPU-bound work onto a worker pool
2 fn to_threaded ( f : pure fn ( X ) - > Y ) - > thread fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )
4
5 // Also allowed (impure function), with the same sendability requirements
6 fn to_threaded ( f : fn ( X ) - > Y ) - > thread fn ( X ) - > Y
7 where Sendable ( X ) & & Sendable ( captures ( f ) )

Checks: argument and captured values must be sendable or shared/atomic . No reliance on an ambient event loop.

`to_async` *

Example
0 // for any types X, Y
1 fn to_async ( f : thread fn ( X ) - > Y ) - > async fn ( X ) - > Y
2
3 // Lifts a plain sync function too (discouraged unless necessary)
4 fn to_async ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
5 where Sendable ( X ) & & Sendable ( captures ( f ) )

Runtime model: schedules on the blocking/CPU pool; if the pool is saturated, the returned future suspends until capacity is available.

`to_blocking` * (the common case inside async )

Example
0 // for any types X, Y
1 // Inside async: run synchronous work without stalling the event loop
2 fn to_blocking ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )

This is analogous to Rust Tokio’s `block_in_place`: it yields to the scheduler and executes on the blocking pool.

`block_on` * (drive async to completion from a worker thread)

Example
0 // for any type T
1 fn block_on ( fut : async fn ( ) - > T ) - > thread fn ( ) - > T

Policy: Forbidden on the event‑loop thread; prefer to_async / to_blocking when in async contexts.

`detach` / `join` *

Example
0 type Handle ( T )
1 fn detach ( fut : async fn ( ) - > T ) - > Handle ( T )
2 fn join ( h : Handle ( T ) ) - > async fn ( ) - > T

Diagnostics you’ll see

  • “Argument to `to_threaded` captures non‑sendable state Rc(T).”
  • “`to_blocking` called from non‑async context.”
  • “Pool saturated: `to_async` may suspend until space frees up.”

Examples

CPU work from async (don’t block the loop):

Example
0 async fn load_and_hash ( path : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( path ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 return digest ;
4 }

Submit a threaded task and await the handle:

Example
0 let t : Task ( Digest ) = to_threaded ( compute_hash ) ( bytes ) ;
1 let d : Digest = await t ; // structured join

Drive async to completion from a worker thread:

Example
0 thread fn load_cfg_sync ( ) - > Config {
1 std : : concurrency : : block_on ( load_cfg_async ) ( )
2 }

Lift pure compute to workers:

Example
0 pure fn sum ( xs : & [ i32 ] ) - > i32 { /* ... */ }
1 let task : Task ( i32 ) = std : : concurrency : : to_threaded ( sum ) ( nums ) ;
2 let result : i32 = await task ;

Use blocking work from async:

Example
0 async fn hash_file ( p : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( p ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 digest
4 }

Use `to_async` to present sync/threaded as async:

Example
0 thread fn compress ( data : Bytes ) - > Bytes { /* CPU intensive */ }
1
2 async fn upload ( path : string ) - > Result ( Url , IoError ) {
3 let compressed = await std : : concurrency : : to_async ( compress ) ( await read_file ( path ) ) ;
4 return await send_to_server ( compressed ) ;
5 }

Detached background task:

Example
0 let h = std : : concurrency : : detach ( expensive_build ( ) ) ;
1 await std : : concurrency : : join ( h ) ;

Idioms and examples

  • Keep core transforms pure , wrap with intrinsics at the edges.
  • Use thread { ... } blocks for structured parallelism; all tasks inside must complete before exit.
  • Use std::select to race multiple async sources and cancel losers automatically.

FFI without foot‑guns

Declare foreign functions with explicit disciplines and refinements:

Example
0 ffi read_file = async fn ( path : string where exists ( path ) ) - > Result ( string , IoError )

Then wrap with system policies to guard where they are allowed:

parse_config } }" lang="aela" title="Example" id="8c9dff8f39f5b">
Example
0 system IO {
1 action ReadConfigAllowed ( ) - > Config
2 requires io_capability ( )
3 { await read_file ( " / etc / app . json" ) . ? | > parse_config }
4 }

Concurrency & mutability

  • Use shared / atomic types for cross‑thread data.
  • thread functions may operate on shared safely.
  • pure functions must not mutate shared state.

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.”
&Self T { return &self.0; } fn other(self: &Self as S, other: &Self as O) -> &O T { return &other.0; } } fn demo_methods() { let p1: Pair(int) = (1, 2); let p2: Pair(int) = (3, 4); let r1 = p1.first(); let r2 = p1.other(&p2); print(r1); print(r2); } // 4) Higher-order function: label flows through function type fn map_head(xs: &Vec(T) as A, f: Fn(&A T) -> U) -> &A U { return f(&xs[0]); } fn demo_hof() { let nums: Vec(int) = [1, 2, 3]; let head_ref = map_head(&nums, fn(x: &int) -> &int { return x; }); print(head_ref); } // 5) Multiple inputs require label: `as A` disambiguates the return fn pick(a: &T as A, b: &T) -> &A T { // body could choose either; label tells the checker the result is tied to `a` return a; } // 6) Optional: Outlives relation (advanced) fn choose_longer(a: &T as X, b: &T as Y) -> &X T where Y : X { return a; } // 7) Struct constructor with label reuse struct Window(T) { head: &A T, tail: &B T } fn mk_window(xs: &Vec(T) as A, ys: &Vec(T) as B) -> Window(T) { return Window { head: &xs[0], tail: &ys[0] }; } fn demo_window() { let xs: Vec(int) = [1,2,3]; let ys: Vec(int) = [4,5,6]; let w = mk_window(&xs, &ys); print(w.head); print(w.tail); } // 8) Diagnostics-friendly failure (commented): // fn bad_pick(a: &T, b: &T) -> &T { // if cond { return a; } else { return b; } // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`. // }" lang="aela" title="Example" id="afc4d82ee77ff">
Example
0 // 1) Disambiguate which input a returned reference is tied to
1 fn first_of_two ( a : & T as A , b : & T ) - > & A T {
2 return a ;
3 }
4
5 fn demo_first_of_two ( ) {
6 let x : int = 10 ;
7 let y : int = 20 ;
8 let rx = & x ;
9 let ry = & y ;
10
11 let r = first_of_two ( rx , ry ) ;
12 print ( r ) ;
13 }
14
15 // 2) Struct field referencing an argument via label
16 struct View ( T ) { data : & A T }
17
18 fn make_view ( x : & T as A ) - > View ( T ) {
19 return View { data : x } ;
20 }
21
22 fn demo_view ( ) {
23 let s : string = "hello" ;
24 let v = make_view ( & s ) ;
25 print ( v . data ) ;
26 }
27
28 // 3) Methods: implicit Self label + explicit labels to disambiguate
29 impl Pair ( T ) {
30 fn first ( self : & Self ) - > & Self T {
31 return & self . 0 ;
32 }
33
34 fn other ( self : & Self as S , other : & Self as O ) - > & O T {
35 return & other . 0 ;
36 }
37 }
38
39 fn demo_methods ( ) {
40 let p1 : Pair ( int ) = ( 1 , 2 ) ;
41 let p2 : Pair ( int ) = ( 3 , 4 ) ;
42
43 let r1 = p1 . first ( ) ;
44 let r2 = p1 . other ( & p2 ) ;
45 print ( r1 ) ;
46 print ( r2 ) ;
47 }
48
49 // 4) Higher-order function: label flows through function type
50 fn map_head ( xs : & Vec ( T ) as A , f : Fn ( & A T ) - > U ) - > & A U {
51 return f ( & xs [ 0 ] ) ;
52 }
53
54 fn demo_hof ( ) {
55 let nums : Vec ( int ) = [ 1 , 2 , 3 ] ;
56 let head_ref = map_head ( & nums , fn ( x : & int ) - > & int { return x ; } ) ;
57 print ( head_ref ) ;
58 }
59
60 // 5) Multiple inputs require label: `as A` disambiguates the return
61 fn pick ( a : & T as A , b : & T ) - > & A T {
62 // body could choose either; label tells the checker the result is tied to `a`
63 return a ;
64 }
65
66 // 6) Optional: Outlives relation (advanced)
67 fn choose_longer ( a : & T as X , b : & T as Y ) - > & X T where Y : X {
68 return a ;
69 }
70
71 // 7) Struct constructor with label reuse
72 struct Window ( T ) { head : & A T , tail : & B T }
73
74 fn mk_window ( xs : & Vec ( T ) as A , ys : & Vec ( T ) as B ) - > Window ( T ) {
75 return Window { head : & xs [ 0 ] , tail : & ys [ 0 ] } ;
76 }
77
78 fn demo_window ( ) {
79 let xs : Vec ( int ) = [ 1 , 2 , 3 ] ;
80 let ys : Vec ( int ) = [ 4 , 5 , 6 ] ;
81 let w = mk_window ( & xs , & ys ) ;
82 print ( w . head ) ;
83 print ( w . tail ) ;
84 }
85
86 // 8) Diagnostics-friendly failure (commented):
87 // fn bad_pick(a: &T, b: &T) -> &T {
88 // if cond { return a; } else { return b; }
89 // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`.
90 // }

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

Example
0 let s : string = "hi" ;
1 let r = & s ; // borrow starts
2 print ( r ) ; // last use of r
3 var t = s ; // OK allowed: r’s region ended at last use (lexically-free)

L1 — Loan Creation

Example
0 var x : int = 0 ;
1 let r = & x ; // L(x, shared)
2 let m = & mut x ; // Not OK conflict later under A1, but creation itself establishes L(x, unique)

L2 — Loan Propagation

Example
0 fn id_ref ( p : & int ) - > & int { p }
1 let x : int = 1 ;
2 let r1 = & x ; // L(x, shared)
3 let r2 = id_ref ( r1 ) ; // loan propagates to r2 until last use
4 print ( r2 ) ; // OK!

A1 — Unique Exclusivity

Example
0 var v : int = 0 ;
1 let m = & mut v ; // L(v, unique)
2 let r = & v ; // Not OK! A1: unique excludes any concurrent shared borrow

A2 — Shared Read‑Only

Example
0 var n : int = 0 ;
1 let a = & n ; // L(n, shared)
2 let b = & n ; // another shared loan
3 print ( * a + * b ) ; // OK! reads allowed
4 n = 5 ; // Not OK! A2: write while shared loans alive

I1 — Write Invalidates

Example
0 var s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ;
3 s . push ( " ! " ) ; // Not OK! I1: write to s while shared loan alive (if r not yet last‑used)

I2 — Move Invalidates

Example
0 var s : string = "a" ;
1 let r = & s ; // L(s, shared)
2 var t = s ; // Not OK! I2: move invalidates loans; r would dangle

I3 — Overlap/Fields

Example
0 struct P { x : int , y : int }
1 var p : P = P { x : 1 , y : 2 } ;
2 let mx = & mut p . x ; // L(p.x, unique)
3 let my = & mut p . y ; // OK, disjoint fields: allowed
4
5 var arr : [ int ; 3 ] = [ 0 , 1 , 2 ] ;
6 let a = & mut arr [ 0 ] ;
7 let b = & mut arr [ 1 ] ; // not OK, if indices distinct constants
8 let i = 0 ; let j = read_index ( ) ;
9 let c = & mut arr [ i ] ;
10 let d = & mut arr [ j ] ; // Not OK conservatively, may overlap unless proven disjoint (use split helpers)

U1 — Use Requires Alive

Example
0 let s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ; // OK! use while alive
3 // after last use r ends; any further use would be not OK (dead borrow)

U2 — No After‑Free

Example
0 fn bad ( ) {
1 let s : string = "x" ;
2 let r = & s ;
3 drop ( s ) ; // base place dead
4 print ( r ) ; // Not OK: U2: use after base death
5 }

RB1 — Shared from Unique

Example
0 var v : int = 0 ;
1 let mu = & mut v ; // L(v, unique)
2
3 // Shared reborrow of the same place (auto-deref from &mut int to int)
4 let rs : & int = & mu ; // creates L(v, shared)
5
6 print ( rs ) ;
7
8 // Write through the unique borrow (auto-deref on assignment)
9 mu = 3 ; // must end shared loan before writing via `mu`

RB2 — Unique from Unique (optional v1)

Example
0 var v : int = 0 ;
1 let mu1 = & mut v ;
2 let mu2 = & mut mu1 ; // unique reborrow of v; allowed only if no overlapping use via mu1

E1 — No Escaping Borrows

Example
0 fn leak_ref ( ) - > & int {
1 let x : int = 1 ;
2 return & x ; // Not OK! Escapes to caller; Not OK, dies at function end
3 }
4
5 fn head ( s : & string ) - > & char {
6 return & s [ 0 ] ;
7 } // OK! Summary ties return to arg

M1 — Binding Mutability

Example
0 let x : int = 0 ;
1 let rx = & mut x ; // Not OK: M1: &mut requires mutable base
2 var y : int = 0 ;
3 let ry = & mut y ; // OK

M2 — No Shared Mutability Without Atomics

Example
0 shared var n : int = 0 ; // shared location
1 let r1 = & n ; let r2 = & n ; // shared borrows
2 n = n + 1 ; // Not OK concurrent write without atomic discipline
3 atomic var a : int = 0 ; // with atomic, writes are allowed by policy

T1 — Temporaries

Example
0 print ( & ( make_string ( ) ) ) ; // OK temporary lives through call; reference dies at last use
1 let r = & ( make_string ( ) ) ;
2 print ( r ) ; // Not OK if r would outlive the temporary’s last use

T2 — Branches/Loops/Match

Example
0 let s : string = "x" ;
1 let r = & s ;
2 if cond { print ( r ) ; } else { print ( r ) ; }
3 // r is used on both paths; live set at join = intersection ⇒ still alive until after the if
4 var t = s ; // not OK must occur after r’s last use on all paths

F1 — FFI Preconditions

Example
0 ffi puts : ( & char ) - > int = . . . ;
1 let s : string = "hi" ;
2 let r = & s [ 0 ] ;
3 puts ( r ) ; // OK if FFI summary: does not retain; Not OK if it may retain (escape)

F2 — FFI Postconditions

Example
0 ffi c_strchr : ( & char , int ) - > & char = . . . ; // trusted: result aliases input
1
2 fn first_a ( s : & string ) - > & char {
3 c_strchr ( & s [ 0 ] , 'a' ) // OK allowed only because summary ties result to arg region
4 }

RFT1 — Refinement Well‑Formedness

Example
0 let x : int = 5 ;
1 let y : { z : & int where initialized ( z ) } = { z : & x } ; // OK predicate references lifetime‑relevant property

RFT2 — Discharge at Use Sites

Example
0 fn show ( p : { z : & int where not_escaped ( z ) } ) - > void {
1 print ( p . z ) ; // OK! checker discharges `not_escaped` from current loan facts
2 }

inter‑Procedural Summary (Elision)

Example
0 fn get_first ( a : & [ int ] ) - > & int {
1 return & a [ 0 ] ;
2 }
3
4 // elaborated internally: for<ρ> fn(&ρ [int]) -> &ρ int
5 // caller instantiates ρ from its argument; return tied to same ρ

Structs with Reference Fields (Implicit Regions)

Example
0 struct Node ( T ) { data : & T } // elaborates to Node<ρ, T>
1
2 fn demo ( ) - > void {
3 let x : int = 1 ;
4 var n : Node ( int ) = Node { data : & x } ; // OK n: Node<ρx, int>
5 }
6
7 fn bad ( ) - > void {
8 var n : Node ( int ) ;
9
10 {
11 let x : int = 1 ;
12 n = Node { data : & x } ; // Not OK n outlives x ⇒ region check fails
13 }
14 }

Async Phase 1 — No Unique Loans Across Await

Example
0 async fn step ( mut v : & int ) - > void {
1 let m = v ; // borrow unique via parameter
2 await tick ( ) ; // Not OK, unique loan across await in phase 1
3 }

Closures — Capture Classification

void { move x }; // by‑value move ⇒ FnOnce" lang="aela" title="Example" id="e459ee693aab5">
Example
0 var n : int = 0 ;
1 let c1 = fn ( ) - > void { print ( & n ) ; } ; // shared borrow capture ⇒ Fn
2 let c2 = fn ( ) - > void { n = n + 1 ; } ; // unique borrow capture ⇒ FnMut
3 let x : string = "hi" ;
4 let c3 = fn ( ) - > void { move x } ; // by‑value move ⇒ FnOnce

RTOS Harmony

Linux Setup

You most likely need to edit your udev rules

Example
0 sudo curl - L - o / etc / udev / rules . d / 50 - cmsis - dap . rules \
1 https : / / raw . githubusercontent . com / pyocd / pyOCD / main / udev / 50 - cmsis - dap . rules

If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.

Example
0 lsusb | grep - iE 'arduino|cmsis|dap|renesas'
1 Bus 001 Device 005 : ID 2341 : 1002 Arduino SA . . .

Replace ID VVVV:PPPP

Example
0 # Arduino UNO R4 WiFi (CMSIS-DAP) — custom rule
1 SUBSYSTEM = = "usb" , ATTR { idVendor } = = "VVVV" , ATTR { idProduct } = = "PPPP" , MODE : = "0666"
2 SUBSYSTEM = = "hidraw" , ATTRS { idVendor } = = "VVVV" , ATTRS { idProduct } = = "PPPP" , MODE : = "0666"

Reload, re-enumerate

Example
0 sudo udevadm control - - reload - rules
1 sudo udevadm trigger

Unplug & Replug, press the reset button & then check:

Example
0 pyocd list

Zephyr

Install

Example
0 git cmake ninja python python - pip dtc wget

Install the Zephyr CLI tool

Example
0 pip install west

Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.

Example
0 sudo usermod - a - G dialout $USER

Create a project directory. Create a python environment in the project directory. Initialize it as a new zephyr project. Run the update command to get all the sub-repos.

Example
0 mkdir ~ / projects / z
1 python - m venv ~ / projects / z / . venv
2 west init ~ / projects / z
3 west update

Go back to your projects root and get the minimal SDK for cross compiling.

Example
0 cd ~ / projects
1 wget https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz

Calculate the SHA sum if you want

Example
0 wget - O - https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / sha256 . sum | shasum - - check - - ignore - missing

Extract the SDK and run the setup

Example
0 tar xvf zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz
1 cd ~ / projects / zephyr - sdk - 0 . 17 . 4
2 . / setup . sh

Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)

Example
0 # 1. Navigate to your project directory
1 cd ~ / projects / z
2
3 # 2. Activate the Python virtual environment for 'west'
4 source . / . venv / bin / activate
5
6 # 3. Manually export the SDK path to ensure it's found
7 export ZEPHYR_SDK_INSTALL_DIR = ~ / projects / zephyr - sdk - 0 . 17 . 4
8
9 # 4. Source the Zephyr environment to link everything together
10 source . / zephyr / zephyr - env . sh
11
12 # 5. Install a shit ton of dependencies
13 pip - 3 install - r zephyr / scripts / requirements . txt

Compile & Flash Test

Finally, build an Arduino image. I use Blinky here because its super simple and makes sense to start with as a sanity test.

Example
0 west build - p auto - b arduino_uno_r4 zephyr / samples / blinky
1 west flash

Integrating with Aela

Aela can output object files, so it's very simple to create a Zephyr project with Aela by just adding CMakeLists.txt and prj.conf files.

Example
0 myapp /
1 ├─ CMakeLists . txt
2 ├─ prj . conf
3 ├─ index . json
4 └─ index . ae

Example prj.conf

Example
0 # Prefer minimal libc over newlib (if you don’t need full POSIX/locale/etc.)
1 CONFIG_NEWLIB_LIBC = n
2 CONFIG_MINIMAL_LIBC = y
3 # If you must use newlib, at least disable float printf/scanf:
4 # CONFIG_NEWLIB_LIBC_FLOAT_PRINTF=n
5 # CONFIG_NEWLIB_LIBC_FLOAT_SCANF=n
6
7 # Logging/printk/console (turn off what you don't need)
8 CONFIG_PRINTK = n
9 CONFIG_LOG = n
10 # or, if you need logs:
11 # CONFIG_LOG=y
12 # CONFIG_LOG_MODE_MINIMAL=y
13 # CONFIG_LOG_DEFAULT_LEVEL=0
14
15 # Shell/console features often sneak in via defaults
16 CONFIG_CONSOLE = n
17 CONFIG_UART_CONSOLE = n
18 CONFIG_SHELL = n
19
20 # Link-time optimization can trim more
21 CONFIG_LTO = y
22 CONFIG_SIZE_OPTIMIZATIONS = y
23
24 # Assertions & debug
25 CONFIG_ASSERT = n
26 CONFIG_DEBUG = n
27 CONFIG_DEBUG_INFO = n # (debug symbols only affect .elf, not .bin size)
28
29 # Heap & stacks
30 CONFIG_HEAP_MEM_POOL_SIZE = 0 # if you don’t malloc at all
31 CONFIG_MAIN_STACK_SIZE = 1024 # tune as low as your app can tolerate

Example CMakeLists.txt

${AELA_OBJ}" VERBATIM ) add_library(aela_objects OBJECT ${AELA_OBJ}) set_source_files_properties(${AELA_OBJ} PROPERTIES GENERATED TRUE) # Link your Aela object (contains `main`) into the Zephyr app target_link_libraries(app PRIVATE aela_objects)" lang="cmake" title="Example" id="2051be01a6894">
Example
0 cmake_minimum_required ( VERSION 3 . 20 )
1 find_package ( Zephyr REQUIRED HINTS $ENV { ZEPHYR_BASE } )
2 project ( myapp )
3
4 # You can also pass these with: -DAEC=/path/aec -DAEC_FLAGS="..."
5 set ( AEC "aec" CACHE FILEPATH "Path to Aela compiler" )
6 set ( AEC_FLAGS "" CACHE STRING "Extra flags for Aela" )
7
8 # Optional: mirror Zephyr’s CPU/FPU flags so the .o matches the board ABI
9 # (We read what Zephyr passes to the C toolchain and reuse the ARM-related bits.)
10 get_property ( _Z_OPTS TARGET zephyr_interface PROPERTY INTERFACE_COMPILE_OPTIONS )
11 set ( _AE_ARM_OPTS "" )
12 foreach ( opt IN LISTS _Z_OPTS )
13 if ( opt MATCHES " ^ - m ( cpu | thumb | float - abi | fpu ) " ) ; list ( APPEND _AE_ARM_OPTS "$ { opt } " ) ; endif ( )
14 endforeach ( )
15
16 set ( AELA_SRC $ { CMAKE_CURRENT_SOURCE_DIR } / myprog . ae )
17 set ( AELA_OBJ $ { CMAKE_CURRENT_BINARY_DIR } / aela / myprog . obj . o )
18
19 add_custom_command (
20 OUTPUT $ { AELA_OBJ }
21 COMMAND $ { CMAKE_COMMAND } - E make_directory $ { CMAKE_CURRENT_BINARY_DIR } / aela
22 COMMAND $ { AEC } $ { AEC_FLAGS } $ { _AE_ARM_OPTS } - c $ { AELA_SRC } - o $ { AELA_OBJ }
23 DEPENDS $ { AELA_SRC }
24 COMMENT "Aela : $ { AELA_SRC } - > $ { AELA_OBJ } "
25 VERBATIM
26 )
27
28 add_library ( aela_objects OBJECT $ { AELA_OBJ } )
29 set_source_files_properties ( $ { AELA_OBJ } PROPERTIES GENERATED TRUE )
30
31 # Link your Aela object (contains `main`) into the Zephyr app
32 target_link_libraries ( app PRIVATE aela_objects )

Compiling

Example
0 west build - b arduino_uno_r4_wifi myapp - p \
1 - DCMAKE_EXPORT_COMPILE_COMMANDS = ON \
2 - DAEC = $ ( command - v aec )
3 west flash

Note

The _AE_ARM_OPTS trick copies exactly the -mcpu/-mfpu/-mfloat-abi/-mthumb flags Zephyr uses for this board, so your Aela object links ABI-cleanly without you guessing the right combo. (UNO R4 WiFi is a Cortex-M4; Zephyr’s board page confirms the arch.)

FreeRTOS

Discover Platform Build Flags

Lets assume an Arduino R4 here as an example.

We need to "spy" on the Arduino CLI to get the exact compiler and linker flags required for the R4 WiFi. The Aela build system will pass these directly to its underlyng C compiler. Arduino code files are called "sketches".

  1. Create a dummy sketch:
temp_sketch/temp_sketch.ino" lang="bash" title="Example" id="2274fcd531ebc">
Example
0 mkdir temp_sketch
1 echo " void setup ( ) { } void loop ( ) { } " > temp_sketch / temp_sketch . ino
  1. Run a verbose compile:
Example
0 arduino - cli compile - - fqbn arduino : renesas_uno : unor4wifi - - verbose temp_sketch
  1. Find and copy the linker command. Scroll through the output and find the longest command, which will start with something like .../arm-none-eabi-g++ ... . It will be a very long line that links all the object files and libraries together. Copy this entire command into a text editor. We're going to use its flags.

It will look something like this (shortened for clarity): .../arm-none-eabi-g++ -Os -Wl,--gc-sections -mcpu=cortex-m4 ... -L/path/to/build -Wl,--start-group -lArduinoCore -lrtos -lm -Wl,--end-group ...

We will now transfer the important parts of that command into your index.json .

Step 2: Project Structure

Organize your project with your source code inside a src directory.

Example
0 aela_freertos_blinky /
1 ├── index . json # The project manifest (our main focus)
2 └── src /
3 ├── main . ae # Your Aela application logic
4 └── shim . c # The C entry-point shim

Step 3: The index.json Manifest

This is the control center. We'll define a custom platform target called "arduino_r4" and place all the flags we discovered into the link section.

Create the file `index.json` (unless it was created via aec init ):

Example
0 {
1 "name" : "aela - freertos - blinky" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4
5 "sources" : {
6 "shared" : [
7 "src / shim . c"
8 ]
9 } ,
10
11 "link" : {
12 "platform" : {
13 "arduino_r4" : [
14 " - mcpu = cortex - m4" ,
15 " - mthumb" ,
16 " - mfloat - abi = hard" ,
17 " - mfpu = fpv4 - sp - d16" ,
18
19 " - Os" ,
20 " - Wl , - - gc - sections" ,
21 " - Wl , - - script = / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI / linker_script . ld" ,
22
23 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / cores / arduino" ,
24 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI" ,
25 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / libraries / Arduino_FreeRTOS / src" ,
26
27 " - L / tmp / arduino / build - 123456789 . . . " ,
28
29 " - Wl , - - start - group" ,
30 " - lArduinoCore" ,
31 " - lrtos" ,
32 " - lm" ,
33 " - Wl , - - end - group"
34 ]
35 }
36 }
37 }

Note

You must replace the placeholder paths ( /home/user/... , /tmp/arduino/... ) with the full, absolute paths you copied from your verbose compiler output in Step 1.

Step 4: The Source Code

The source code is the same as before, but now it lives in the src/ directory.

src/main.ae

src/main.ae
0 // FFI Declarations for C functions
1 struct TaskHandle_t ;
2 type TaskFunction_t = fn ( & void ) - > void ;
3
4 ffi pinMode = fn ( u32 , u32 ) - > void ;
5 ffi digitalWrite = fn ( u32 , u32 ) - > void ;
6 ffi xTaskCreate = fn ( TaskFunction_t , string , u32 , & void , u32 , & TaskHandle_t ) - > i32 ;
7 ffi vTaskStartScheduler = fn ( ) - > void ;
8 ffi vTaskDelay = fn ( u32 ) - > void ;
9
10 // Constants
11 let LED_BUILTIN : u32 = 13 ;
12 let OUTPUT : u32 = 1 ;
13 let HIGH : u32 = 1 ;
14 let LOW : u32 = 0 ;
15
16 // The task that will blink the LED.
17 fn blinkTask ( params : & void ) - > void {
18 pinMode ( LED_BUILTIN , OUTPUT ) ;
19 while ( true ) {
20 digitalWrite ( LED_BUILTIN , HIGH ) ;
21 vTaskDelay ( 500 ) ;
22 digitalWrite ( LED_BUILTIN , LOW ) ;
23 vTaskDelay ( 500 ) ;
24 }
25 }
26
27 // Main entry point called from our C shim.
28 export fn aela_rtos ( ) - > void {
29 xTaskCreate ( blinkTask , "Blinker" , 128 , null , 1 , null ) ;
30 vTaskStartScheduler ( ) ;
31 }

src/shim.c

src/shim.c
0 #include
1
2 // Declare the external function defined in our Aela code.
3 extern void aela_rtos ( ) ;
4
5 // Standard Arduino entry point.
6 void setup ( ) {
7 aela_rtos ( ) ;
8 }
9
10 // loop() will never be reached, but must exist to link correctly.
11 void loop ( ) { }

Step 5: Build and Flash

You tell the Aela compiler what you're targeting, and it uses the manifest to set the correct build flags.

Build the project for the target triple:

Example
0 # This command tells Aela to cross-compile for the specified target.
1 # It will then find the "thumbv7em-none-eabihf" key in your index.json.
2 aec build - - platform = "arduino_r4" - - target thumbv7em - none - eabihf

Flash the output. The build process should still result in a .uf2 file in a build directory. You can then flash it with the Arduino CLI as before.

Example
0 arduino - cli upload - - fqbn arduino : renesas_uno : unor4wifi - - input - file build / aela - freertos - blinky . uf2

FAQ

Why is Aela 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.

Overview

Aela is a commercial-source language for embedded systems.

Aela is a compiled, memory-safe language with a strong, static type system. It started in 2018 as a fork of Rust, but has diverged significantly to service embedded systems use cases. It has a similar syntax and sticks to many of the same goals such as ownership semantics, memory and concurrency safety, only pay for what you use, and zero-cost abstractions.

Programming Language Landscape

This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.

image.png

Langauge Goals

All language design decisions revolve around determinism and performance for embedded systems.

Aela also focuses on harmony with C and C++. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like write(2) .

Language Goals

All language design decisions revolve around providing absolute determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is eliminated. All excluded features have an ideal alternative (see documentation) or have been simply omitted.

Excluded Feature Justification
Panics Panics are not in the type signature; they violate the principle of abstraction and create a hidden, unrecoverable failure path that bypasses the type system.
Exceptions Exceptions create hidden, non-local control flow paths that are impossible to reason about statically and incur runtime overhead. Error handling must be explicit.
Global State Global variables create hidden dependencies and introduce non-determinism, making concurrency unsafe and program behavior impossible to reason about locally.
Lifetime Annotations Explicit lifetime annotations are a significant source of complexity and syntactic noise. The compiler must be smart enough to infer ownership duration without burdening the programmer.
Macros Macros create non-linear, hard-to-debug code flow ("magic"). Code must be explicit and analyzable; what you see is what the compiler gets, ensuring predictability and toolability.
unsafe keyword The unsafe keyword is an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of unsafe operations rather than entire blocks.
Attributes Attributes are a form of meta-programming that injects non-local behavior and hidden complexity. They modify code in non-obvious ways, violating the principle that code should be explicit.
Pointer Arithmetic Direct pointer manipulation is a primary source of memory safety vulnerabilities (e.g., buffer overflows). Safe, bounds-checked slice operations are the only acceptable alternative.
Advanced Traits Complex trait systems lead to baroque, unreadable type signatures and cryptic compiler errors. Simplicity and clarity are prioritized over abstract expressive power.
Inline Assembly Inline assembly is non-portable, opaque to the optimizer, and breaks static analysis. Low-level routines must be provided via a stable C ABI, ensuring a clean contract.
null keyword Null pointers are the source of countless runtime crashes. The absence of a value must be explicitly represented and handled in the type system (e.g., via Option ).
Operator Overloading Operator overloading makes code ambiguous and hides the cost of operations. Function calls must be explicit to ensure code clarity and predictable performance.
Implicit Conversions Implicit conversions hide potential bugs, such as data truncation or precision loss. All type conversions must be explicit, forcing the programmer to acknowledge the operation.

Feature Comparison

Feature Aela C C++ Rust Ada
Compile-Time Memory Safety √ √ √
Cold Build Speed √ √ √
Reference Counted √ √
Automatic RAII √ √
Formal Verification √ √
Dependent & Refinement Types √
Language-Native Concurrency √
Structured Concurrency √ √
Automatic C/C++ safe binding √

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 won't 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

- /path/to/my-app/index.json
0 {
1 "name" : "my - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae"
4 }

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

- index.json for a project that uses a UI library
0 {
1 "name" : "my - gui - app" ,
2 "version" : "1 . 0 . 0" ,
3 "entry" : "src / app . ae" ,
4 "dependencies" : {
5 "ui" : " . . / libs / aela - ui" ,
6 "database" : " . . / libs / aela - db"
7 }
8 }

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

- ../libs/aela-ui/src/window.ae
0 // This struct can be imported by other modules.
1 export struct WindowOptions {
2 title : string ,
3 width : int ,
4 height : int ,
5 }
6
7 // This function is private to the window.ae module.
8 fn internal_helper ( ) - > void {
9 // ...
10 }

Re-exports

- re-export pattern
0 import { Thing1 , Thing2 } from "things . ae" ;
1
2 export Thing1 ;
3 export Thing2 ;

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

";" lang="" title="Example" id="b68adefb69265">
Example
0 import from " " ;

Example

void { // Access symbols using the `::` namespace operator. let opts: &ui::WindowOptions = new ui::WindowOptions(); helpers::do_something(); }" lang="example" title="- src/app.ae" id="027e17636df19">
- src/app.ae
0 // Import the "ui" package, which was defined in index.json.
1 import ui from "ui" ;
2
3 // Import a local utility file using a relative path.
4 import helpers from " . / helpers . ae" ;
5
6 fn main ( ) - > void {
7 // Access symbols using the `::` namespace operator.
8 let opts : & ui : : WindowOptions = new ui : : WindowOptions ( ) ;
9 helpers : : do_something ( ) ;
10 }

Named Imports

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

Syntax

";" lang="" title="Example" id="9905825be2237">
Example
0 import { , : } from " " ;

Example EXAMPLE

void { // `Window` can be used directly. let win: &Window = new Window(); // `WindowOptions` is available under the alias `Options`. let opts: &Options = new Options(); }" lang="example" title="- src/app.ae" id="3192e955d263e">
- src/app.ae
0 import { Window , WindowOptions : Options } from "ui" ;
1
2 fn main ( ) - > void {
3 // `Window` can be used directly.
4 let win : & Window = new Window ( ) ;
5
6 // `WindowOptions` is available under the alias `Options`.
7 let opts : & Options = new Options ( ) ;
8 }

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

- index.json for an app with native UI code on macOS
0 {
1 "name" : "aela - native - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4 "sources" : {
5 "darwin" : [ "src / native / apple . mm" ]
6 } ,
7 "link" : {
8 "platform" : {
9 "darwin" : [
10 " - framework" , "Foundation" ,
11 " - framework" , "AppKit" ,
12 " - framework" , "ObjectiveC"
13 ]
14 }
15 }
16 }

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.

Failures

A primary cause of software defects, security vulnerabilities, and developer anxiety is the "Trust Gap": the difference between what a function's signature claims it does and what its implementation can actually do. Aela is designed to eliminate this gap. Its error and fault handling system is built on a single, non-negotiable principle: a function's signature must be a complete and honest contract, and the compiler must enforce it.

Don't Try-Catch

Traditional exception systems, common in languages like Java, JavaScript, C++, and Python, introduce a form of hidden control flow. A throw or raise statement is a non-local goto that is often invisible in the function's signature.

Consider a typical function in such a language: function get_user(id: int) -> User

This signature makes a simple promise: "Give me an integer, and I will give you a User." However, the implementation might throw a DatabaseConnectionException, a UserNotFoundException, or a NullPointerException. To understand the function's true behavior, the developer must embark on a research project: reading the documentation (which may be out of date), reading the source code, and reading the source of every function it calls.

This breaks a developer's ability to reason locally about the code.

Don't Panic

Some modern languages, notably Rust, attempt to solve error handling this by creating a two-tiered system:

  • Recoverable Errors ( Result ): For expected failures (e.g., file not found). These are part of the type signature.
  • Unrecoverable Bugs ( panic! ): For programmer errors (e.g., index out of bounds). These are not part of the type signature.

While an improvement, this still creates a hidden side-channel for bugs. More critically, the panic! mechanism creates a deep schism between platforms, especially for embedded systems.

The unwind vs. abort Schism:

On servers, panic! defaults to unwind, a slow and complex process that runs cleanup code (destructors). This adds a significant "tax" to the binary size, which is unacceptable on resource-constrained devices.

On embedded systems, developers are forced to configure panics to abort, which immediately halts the program.

The Broken Promise of abort: When panic = "abort" is used, the language's core safety promise—that resources will be cleaned up on failure (RAII via Drop in Rust)—is broken. Destructors are never called. A MutexGuard will leave a mutex permanently locked. A peripheral that was supposed to be disabled is left in an active state. The very code written to ensure safety on failure becomes useless.

This patched-together model is not a first-principles solution. Aela requires a single, unified system that is safe, deterministic, and efficient on all platforms.

The Fault Model

The Principle of the Honest Contract: Aela avoids ambiguity in failure handling by enforcing that the outcome of a function must be encoded in its signature.

Function Signatures

A function declares its potential to terminate due to an unrecoverable logic bug by using the | operator in its return type. This operator separates the single success type from a list of one or more fault types.

fn get_at(slice: &[u8], index: int) -> u8 | OutOfBounds;

This signature is an honest contract. It tells any caller: "This function will either return a u8 , or it will terminate with an OutOfBounds fault. There are no other possibilities."

The fault and raise Keywords

  • `fault` : A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from struct or enum , which represent data and recoverable errors.
  • fault OutOfBounds(index: int, len: int);
  • `raise` : A keyword that triggers a fault. It immediately stops the current function's execution and propagates the fault to the caller. raise is considered a terminal action.
  • raise OutOfBounds(index: index, len: len);

The Standard match Statement

The match statement is how Aela handles the outcome of functions that may terminate with faults.

Example
0 match ( expression ) {
1 pattern1 = > { . . . } ,
2 pattern2 = > { . . . } , // potentially a fault type!
3 . . .
4 }

Semantic Rules

The safety and special behavior of fault handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:

If the expression being evaluated by a match statement has a fault path in its signature (i.e., contains a | ), then the compiler enforces a "Terminal Arm Rule" on any arm that matches a fault -declared type.

This rule is context-dependent. It is triggered by the signature of the function being called, not just the type of the pattern. This is the key insight that resolves all ambiguity.

The "Terminal Arm Rule" is defined as: The block of the arm must end with a terminal statement. Aela does not have implicit returns, so this is a direct check of the final statement in the block.

Terminal statements are:

  • raise ;
  • std::abort();
  • std::halt();
  • std::reboot();

Note

pure fn ketword must not introduce or handle faults; they cannot have a | in their return type and cannot raise.

Note

Faults must not cross FFI; board/FFI shims must convert faults to domain-appropriate codes or terminals.

Note

AP131 outlines a proposal to have return be the equivalent of raise . Allowing both and specifying that they’re identical.

Note

AP132 outlines a proposal to permit functions to be generic over an open set of faults (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;

Note

AP134 outlines a proposal to add a desugaring operator. let b = get_at(xs, 0)?; // expands to match/raise

Complete Examples: The Rule in Practice

These two examples demonstrate how the context-dependent rule creates a safe and unambiguous system.

Example 1: Handling a Live Fault Event

Example
0 // The compiler sees the '|' in the signature, so it activates the Terminal Arm Rule for this match.
1 match ( create_packet ( user_size ) ) {
2 Some ( packet ) = > { /* This arm is normal. */ } ,
3 None = > { /* This arm is normal. */ } ,
4
5 // The compiler sees that `PacketTooLarge` is a `fault` type and applies the rule.
6 f : PacketTooLarge = > {
7 log : : critical ( "Logic error : Invalid packet size requested . " , f ) ;
8 // The block ends with a known terminal keyword. The code is valid.
9 std : : reboot ( ) ;
10 }
11 }

If reboot; were omitted, the compiler would issue a clear error: "Fault-handling arm must end with a terminal statement."

Example 2: Inspecting a Fault as Data

Example
0 // This function returns a fault object as a value. Its signature has NO '|'.
1 fn inspect_issues ( ) - > PacketTooLarge ;
2
3 // The compiler sees NO '|' in the signature, so it DOES NOT activate the Terminal Arm Rule.
4 match ( inspect_issues ( ) ) {
5
6 // Even though `PacketTooLarge` is a `fault` type, the rule is not active.
7 // This arm is treated as a normal pattern match.
8 f : PacketTooLarge = > {
9 log : : warn ( "A non - critical issue was detected : " , f ) ;
10 // The block is allowed to complete normally. The code is valid.
11 }
12 }

Memory & Mutability

1. Default Allocation Semantics

  • All values start on the stack by default.
  • Stack allocations are:
  • Fast
  • Scoped
  • Owned directly by the binding.
Example
0 let foo : Foo = { num : 0 } ; // Foo is stack-allocated

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.

Example
0 let x : & T = new { . . . val } ; // Allocate on the heap
1 let x : & T = new shared { . . . val } ; // Single-threaded, mutable
2 let x : & T = new shared atomic { . . . val } ; // Thread-safe atomic
3 var x : & T = new weak { . . . val } ; // Mutable weak reference
4 var x : & T = new static { . . . val } ; // New without malloc
5 var x : & T = new static atomic { . . . val } ; // New without malloc, Thread-safe atomic

Behavior of new Modifiers

Modifier Behavior Description
(none) Heap Allocation (OS based allocator). Returns a handle/reference to a freshly allocated object, immutable and can not be loaned.
shared Heap. Shared ownership, single-threaded. Allowed to be loaned; not thread-safe; not Send/Sync-like.
shared atomic Heap. Shared ownership, thread-safe. Reference counts and interior coordination use atomics; Send/Sync if T satisfies the “atomic-safe” requirements you define.
weak Heap, weak handle to a shared object. Does not keep the allocation alive; must be paired with at least one strong shared/shared atomic owner somewhere to be useful.
static Static storage, no OS allocator. Object is placed/constructed in static memory (BSS/RODATA/flash/SECTION), suitable for bare-metal/MCUs. Lifetime: program-long (or until explicitly torn down by system semantics).
static atomic Static storage, thread-safe coordination via atomics. Shared global counters updated in ISR + mainline, Lock-free buffers (ring buffers for UART, DMA, etc.). Configuration/state variables read by multiple cores or ISRs. On a simple single-core MCU with no interrupts, it’s redundant but harmless.
  • 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 :

Keyword Meaning
let Immutable binding (read-only)
var Mutable binding (read-write)
  • The mut keyword is not necesasry here.
  • Mutability is not encoded in types, structs, or fields.
  • let and var are both lexically scoped.

Example

Example
0 let a : & Foo = new shared { . . . foo } ; // Immutable heap reference
1 var b : & Foo = new shared { . . . foo } ; // Mutable heap reference

Note

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

4. Weak References & Cycle Prevention

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'

Example
0 if let strong_ref = weak_ref {
1 // This block only runs if the object is still alive.
2 // 'strong_ref' is a new, temporary strong reference of type &Foo.
3 strong_ref . do_something ( ) ;
4 }

5. Copying Stack Values

  • Heap allocation requires copying the stack value:
Example
0 new shared { . . . foo } // `{ ...foo }` performs a field-wise copy
  • This avoids moving ownership from the stack. Moves are not allowed .

5. Reference Types and Behavior

Kind Syntax RC Type Thread-Safe Mutable
Stack value let x: T = ... None N/A No
Heap reference let x: &T = new shared {...} RC No No
Heap reference (mutable) var x: &T = new shared {...} RC No Yes
Heap reference (atomic) let/var x: &T = new shared atomic {} ARC Yes Depends

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.
a copy of the number 10 is passed. // bar(stack_str); -> a copy of the {ptr, i64} struct is passed." lang="example" title="- Stack Allocated" id="5096a1ef49907">
- Stack Allocated
0 let stack_int : i32 = 10 ; // The variable 'stack_int' IS the number 10.
1 let stack_str : string = "hello" ; // The variable 'stack_str' IS the {ptr, i64} struct.
2
3 // When calling a function:
4 // foo(stack_int); -> a copy of the number 10 is passed.
5 // bar(stack_str); -> a copy of the {ptr, i64} struct is passed.

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.
- Heap allocated via new
0 let heap_int : i32 = new 42 ; // 'heap_int' is a POINTER to a box containing 42.
1 let heap_obj : MyStruct = new { } ; // 'heap_obj' is a POINTER to a box containing a MyStruct.
2 let heap_arr : u8 [ ] = new [ 1 , 2 , 3 ] ; // 'heap_arr' is a POINTER to a box for the array data.
3
4 // When calling a function:
5 // foo(heap_int); -> a copy of the POINTER is passed. The heap data is not touched.

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.
- Special Case
0 let captured_var = new "text" ;
1
2 let my_closure = fn ( ) {
3 print ( captured_var ) ; // Captures the pointer 'captured_var'.
4 } ;
5
6 // 'my_closure' is a {func_ptr, env_ptr} struct.
7 // 'env_ptr' points to a heap box which contains a copy of the 'captured_var' pointer.

Refinement & Dependent Types

TL;DR: Refinement & dependent types are types that embed logical conditions or values themselves, making illegal states unrepresentable by construction.

If you're coming from languages like JavaScript, C++, or Rust, you're used to type systems that check the shape of your data. For example, a type checker ensures you don't use a string where a number is expected.

Aela takes this a step further with refinement types and dependent types . These are features that allow the type system to understand and check the values of your data, not just their shape. It's more rigorous that shape checking, it's a value-aware check that happens entirely at compile time .

Motivation

Most type systems validate shape (ie., "this is an int "). Aela also validates value-level facts : a string is non-empty , an integer is non-zero , a vector’s length matches what your function promises. This turns bugs into compile‑time errors and makes code self-documenting.

  • Earlier feedback: logical mistakes become type errors you see during compilation.
  • Stronger intent: types like NonEmptyString and NonZeroint tell the reader (and the compiler) exactly what you mean.
  • Confidence: fewer defensive checks sprinkled across your code.

Compile-Time VS. Run-Time Arguments

Aela uses a single parameter list for functions, with an optional compile-time section separated from the run-time section by a semicolon ; . Parameters are separated by commas. If a parameter has a type annotation, it will be considered a value parameter. If a value has no type annotation, it will be considered a type.

Example
0 fn f ( T , U ; x : T , y : U ) - > T { return x ; }
1 └┬─┘ └┬───────┘
2 │ └─ Run - Time Parameters
3 └─ Compile - Time Parameters
4
5 fn g ( T ; ) - > T { . . . } // Compile-Time Only (rare but allowed; note trailing `;`)
6 fn h ( x : i32 ) - > i32 { return x ; } // Run Time Only (no `;`)

Rules

  • Tokens before ; are compile-time parameters (type or const/value-level),
  • Type parameters: bare identifiers (ie., T , U ).
  • Const parameters: Name: Type form (ie., N: int ).
  • Tokens after ; are run-time parameters (the usual name: Type , with optional mut / spread, per language rules).
  • If there’s no ; , the entire list is treated as run-time parameters.
  • If the CT part is empty , omit ; (preferred style). If the RT part is empty and CT is present, keep a trailing ; .

Refinement Types: add a where -clause to any base type

A refinement type is a base type with a logical predicate.

Syntax : { id: Type where predicate }

Example
0 // A string that must be non-empty
1 type NonEmptyString = { s : string where std : : length ( s ) > 0 } ;
2
3 let good : NonEmptyString = "Aela" ; // ok
4 let bad : NonEmptyString = "" ; // compile-time error

Use refinements when you want value-aware validation while keeping the underlying representation.

Note

The compiler statically checks predicates where it can (literals, constant expressions, and facts learned from prior code/contracts). When a predicate can’t be decided statically, you’ll provide evidence (see “Proving facts to the compiler”).

Dependent Types: when types mention values

A dependent type is a type that depends on values .

A simple, practical pattern is to refine a function’s return by its inputs :

Example
0 fn add ( a : i32 , b : i32 ) - > { r : i32 where r = = a + b } {
1 return a + b ;
2 }

Here the return type depends on the run-time values a and b . The compiler enforces this contract at compile time wherever it can be proven, and narrows follow-up reasoning.

Another common pattern uses compile-time const parameters to index types:

Example
0 // Conceptual example; CT params appear before `;`
1 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) {
2 // implementation builds a vector whose length is M+N
3 }
  • T is a type parameter .
  • M and N are const parameters (compile-time integers).
  • The result type’s length computes to M + N at the type level .

Proving facts to the compiler

There are three common ways to convince the compiler of a refinement:

  1. Literals and constant expressions — obvious at compile time:
Example
0 let z : NonZeroint = 10 ; // trivially valid
  1. Local reasoning / guards — use a guard to establish a fact for a scope:
Example
0 fn safe_head ( xs : string [ ] ) - > { s : string where std : : length ( s ) > 0 } {
1 if ( std : : length ( xs ) > 0 ) {
2 return xs [ 0 ] ; // compiler knows length(xs) > 0 in this block
3 } else {
4 // handle empty case or return an option/result type
5 }
6 }
  1. Type-level contracts — express properties in the type and let the compiler check uses:
Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }
3 // Callers must provide evidence that `d != 0`.

Note

In more advanced code, system properties and invariants (see KW_REQUIRES , KW_ENSURES , KW_INVARIANT ) can encode broader guarantees, which the compiler uses as facts within the relevant scope.

End‑to‑End: making division-by-zero impossible

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( numer : i32 , denom : NonZeroint ) - > i32 {
3 return numer / denom ;
4 }
5
6 let a : i32 = 100 ;
7 let b : NonZeroint = 10 ; // proven at compile time
8 let ok = safe_divide ( a , b ) ; // compiles
9
10 let c : i32 = 0 ;
11 let err = safe_divide ( a , c ) ; // type error: expected NonZeroint, got i32

Parameter List: full spec (informal)

Example
0 // Declarations
1 fn name ( CT ; RT ) - > Ret { . . . }
2 fn name ( RT ) - > Ret { . . . } // no CT part → omit `;`
3 fn name ( CT ; ) - > Ret { . . . } // CT-only (allowed)
4
5 // CT parameters
6 typeparam : : = IDENTIFIER // ie., T, U
7 constparam : : = IDENTIFIER ':' Type // ie., N: int, K: U64
8 CT : : = typeparam | constparam ( ',' . . . )
9
10 // RT parameters
11 param : : = [ '...' ] [ 'mut' ] IDENTIFIER ':' Type
12 RT : : = param ( ',' . . . )

Validation

  • The CT side only accepts type/const parameters (no mut , no spreads).
  • The RT side accepts ordinary parameters.
  • A single top‑level ; within the parentheses splits CT from RT.
  • Style: omit an empty CT (; ...) — prefer just ( ... ) .

Choosing Refinement vs. Dependent

Use refinement types when:

  • You’re constraining a familiar base type ( i32 , string , a struct) with a predicate ( n != 0 , len(s) > 0 ).
  • You want to reuse existing APIs with stronger safety.

Use dependent types when:

  • The shape of your result depends on inputs (lengths, indices, protocol states).
  • You have natural compile-time parameters (ie., a block size N: int ).

They compose well: dependent function types can return refinement types, and vice versa.

Error messages (ergonomics)

  • CT/RT mixup : “Compile-time parameter list may only contain type/const parameters.”
  • Missing `;` : If the first parameter looks like a type/const param ( T or N: int ), suggest adding the ; .
  • Unproven refinement : Point to the predicate and suggest guards or helper constructors to provide evidence.

FAQ

Q: Do I have to write CT parameters at call sites? A: Typically no — they’re inferred from RT arguments and expected return types. You can guide inference via annotations.

Q: Can I have multiple `;`? A: No. There is at most one top‑level ; per parameter list.

Q: Are const parameters immutable? A: Yes. They are compile-time values; mutability doesn’t apply.

Q: What about async/pure/thread modifiers? A: These work unchanged and apply to the function as a whole; the ; split only affects parameter binding.

Worked examples (with ; )

1) Identity with a type parameter

Example
0 fn id ( T ; x : T ) - > T { return x ; }

2) Map over a vector (type‑level only)

Example
0 fn map ( T , U ; f : fn ( T ) - > U , xs : Vec ( T ) ) - > Vec ( U ) { . . . }

3) Concat with const lengths (conceptual)

Example
0 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) { . . . }

4) Safe division with a refinement type

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }

Function Types

Why functions feel like they have “colors” (and how Aela fixes it)

Many languages split the world into synchronous and asynchronous functions. That split tends to spread—call sites, types, libraries—until everything is “[colored][1].” Aela acknowledges that programs have different execution disciplines (purity, async, thread-safety), then solves the composition pain with first-class types , clear call rules , and built‑in intrinsics so you can cross boundaries intentionally and safely.

At a glance:

  • Three disciplines (colors): pure , thread , async .
  • Simple call rules enforced by the checker.
  • Intrinsic adapters (escape hatches) to cross colors when needed.
  • Contracts ( requires / ensures ) and system blocks to guard risky crossings.

The three disciplines

pure

  • What it means: No observable side effects; referentially transparent.
  • When to use: Deterministic computation, validation, transforms.
  • Gotchas: Cannot call async or impure functions. May be combined with thread if the work is offloaded safely.

thread

  • What it means: Safe to run off the main executor (e.g., in a worker). No ambient event‑loop assumptions; data must be sendable or shared safely.
  • When to use: CPU‑bound work, blocking IO wrapped properly, parallelizable tasks.
  • Combines with: pure (i.e., pure thread fn ).

async

  • What it means: May suspend at await points, returns a future/awaitable.
  • When to use: IO‑bound workflows, coordination with timers, event‑driven code.
  • Note: async is not pure . It stands alone.

Call rules (the short version)

  • pure → may call only pure .
  • thread → may call thread or pure ; invoking a thread fn yields a Task handle.
  • uncolored (impure) → may call thread / pure directly and async via intrinsic.
  • async → may await other async functions or Task handles, and also call pure / thread without suspension.
  • await is legal inside both async fn and thread fn , because awaiting a Task join or future is permitted in either discipline.

Note

The checker gives precise diagnostics and suggests the right intrinsic when you cross a boundary.

Function types are first‑class

Aela’s type system includes function types with their discipline. These are expressed with refinement/dependent types instead of generics:

Example
0 pure fn ( x : u32 ) - > u32
1 thread fn ( bytes : Bytes ) - > Digest
2 async fn ( path : Path ) - > Result ( file : File , err : IoError )

Function parameters can carry refinements on their arguments or return types, e.g.:

Example
0 pure fn ( n : int where n > 0 ) - > Factorial ( n )

This makes intrinsics predictable and type‑safe, without requiring a generic system.

Crossing boundaries: standard intrinsics

To make crossing disciplines predictable and ergonomic, Aela ships intrinsics in the standard library:

Example
0 std : : concurrency : : to_threaded
1 std : : concurrency : : to_async
2 std : : concurrency : : to_blocking
3 std : : concurrency : : detach
4 std : : concurrency : : join

These are typed adapters that the checker understands.

Signatures & typing rules (no generics required)

Aela doesn’t need parametric generics here—these intrinsics are schematic over types and use refinement/dependent predicates to express constraints. We write them informally as “for any types X, Y…”, and the checker discharges the side conditions.

`to_threaded` *

Example
0 // for any types X, Y
1 // Preferred: lift pure/CPU-bound work onto a worker pool
2 fn to_threaded ( f : pure fn ( X ) - > Y ) - > thread fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )
4
5 // Also allowed (impure function), with the same sendability requirements
6 fn to_threaded ( f : fn ( X ) - > Y ) - > thread fn ( X ) - > Y
7 where Sendable ( X ) & & Sendable ( captures ( f ) )

Checks: argument and captured values must be sendable or shared/atomic . No reliance on an ambient event loop.

`to_async` *

Example
0 // for any types X, Y
1 fn to_async ( f : thread fn ( X ) - > Y ) - > async fn ( X ) - > Y
2
3 // Lifts a plain sync function too (discouraged unless necessary)
4 fn to_async ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
5 where Sendable ( X ) & & Sendable ( captures ( f ) )

Runtime model: schedules on the blocking/CPU pool; if the pool is saturated, the returned future suspends until capacity is available.

`to_blocking` * (the common case inside async )

Example
0 // for any types X, Y
1 // Inside async: run synchronous work without stalling the event loop
2 fn to_blocking ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )

This is analogous to Rust Tokio’s `block_in_place`: it yields to the scheduler and executes on the blocking pool.

`block_on` * (drive async to completion from a worker thread)

Example
0 // for any type T
1 fn block_on ( fut : async fn ( ) - > T ) - > thread fn ( ) - > T

Policy: Forbidden on the event‑loop thread; prefer to_async / to_blocking when in async contexts.

`detach` / `join` *

Example
0 type Handle ( T )
1 fn detach ( fut : async fn ( ) - > T ) - > Handle ( T )
2 fn join ( h : Handle ( T ) ) - > async fn ( ) - > T

Diagnostics you’ll see

  • “Argument to `to_threaded` captures non‑sendable state Rc(T).”
  • “`to_blocking` called from non‑async context.”
  • “Pool saturated: `to_async` may suspend until space frees up.”

Examples

CPU work from async (don’t block the loop):

Example
0 async fn load_and_hash ( path : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( path ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 return digest ;
4 }

Submit a threaded task and await the handle:

Example
0 let t : Task ( Digest ) = to_threaded ( compute_hash ) ( bytes ) ;
1 let d : Digest = await t ; // structured join

Drive async to completion from a worker thread:

Example
0 thread fn load_cfg_sync ( ) - > Config {
1 std : : concurrency : : block_on ( load_cfg_async ) ( )
2 }

Lift pure compute to workers:

Example
0 pure fn sum ( xs : & [ i32 ] ) - > i32 { /* ... */ }
1 let task : Task ( i32 ) = std : : concurrency : : to_threaded ( sum ) ( nums ) ;
2 let result : i32 = await task ;

Use blocking work from async:

Example
0 async fn hash_file ( p : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( p ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 digest
4 }

Use `to_async` to present sync/threaded as async:

Example
0 thread fn compress ( data : Bytes ) - > Bytes { /* CPU intensive */ }
1
2 async fn upload ( path : string ) - > Result ( Url , IoError ) {
3 let compressed = await std : : concurrency : : to_async ( compress ) ( await read_file ( path ) ) ;
4 return await send_to_server ( compressed ) ;
5 }

Detached background task:

Example
0 let h = std : : concurrency : : detach ( expensive_build ( ) ) ;
1 await std : : concurrency : : join ( h ) ;

Idioms and examples

  • Keep core transforms pure , wrap with intrinsics at the edges.
  • Use thread { ... } blocks for structured parallelism; all tasks inside must complete before exit.
  • Use std::select to race multiple async sources and cancel losers automatically.

FFI without foot‑guns

Declare foreign functions with explicit disciplines and refinements:

Example
0 ffi read_file = async fn ( path : string where exists ( path ) ) - > Result ( string , IoError )

Then wrap with system policies to guard where they are allowed:

parse_config } }" lang="aela" title="Example" id="8c9dff8f39f5b">
Example
0 system IO {
1 action ReadConfigAllowed ( ) - > Config
2 requires io_capability ( )
3 { await read_file ( " / etc / app . json" ) . ? | > parse_config }
4 }

Concurrency & mutability

  • Use shared / atomic types for cross‑thread data.
  • thread functions may operate on shared safely.
  • pure functions must not mutate shared state.

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.”
&Self T { return &self.0; } fn other(self: &Self as S, other: &Self as O) -> &O T { return &other.0; } } fn demo_methods() { let p1: Pair(int) = (1, 2); let p2: Pair(int) = (3, 4); let r1 = p1.first(); let r2 = p1.other(&p2); print(r1); print(r2); } // 4) Higher-order function: label flows through function type fn map_head(xs: &Vec(T) as A, f: Fn(&A T) -> U) -> &A U { return f(&xs[0]); } fn demo_hof() { let nums: Vec(int) = [1, 2, 3]; let head_ref = map_head(&nums, fn(x: &int) -> &int { return x; }); print(head_ref); } // 5) Multiple inputs require label: `as A` disambiguates the return fn pick(a: &T as A, b: &T) -> &A T { // body could choose either; label tells the checker the result is tied to `a` return a; } // 6) Optional: Outlives relation (advanced) fn choose_longer(a: &T as X, b: &T as Y) -> &X T where Y : X { return a; } // 7) Struct constructor with label reuse struct Window(T) { head: &A T, tail: &B T } fn mk_window(xs: &Vec(T) as A, ys: &Vec(T) as B) -> Window(T) { return Window { head: &xs[0], tail: &ys[0] }; } fn demo_window() { let xs: Vec(int) = [1,2,3]; let ys: Vec(int) = [4,5,6]; let w = mk_window(&xs, &ys); print(w.head); print(w.tail); } // 8) Diagnostics-friendly failure (commented): // fn bad_pick(a: &T, b: &T) -> &T { // if cond { return a; } else { return b; } // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`. // }" lang="aela" title="Example" id="afc4d82ee77ff">
Example
0 // 1) Disambiguate which input a returned reference is tied to
1 fn first_of_two ( a : & T as A , b : & T ) - > & A T {
2 return a ;
3 }
4
5 fn demo_first_of_two ( ) {
6 let x : int = 10 ;
7 let y : int = 20 ;
8 let rx = & x ;
9 let ry = & y ;
10
11 let r = first_of_two ( rx , ry ) ;
12 print ( r ) ;
13 }
14
15 // 2) Struct field referencing an argument via label
16 struct View ( T ) { data : & A T }
17
18 fn make_view ( x : & T as A ) - > View ( T ) {
19 return View { data : x } ;
20 }
21
22 fn demo_view ( ) {
23 let s : string = "hello" ;
24 let v = make_view ( & s ) ;
25 print ( v . data ) ;
26 }
27
28 // 3) Methods: implicit Self label + explicit labels to disambiguate
29 impl Pair ( T ) {
30 fn first ( self : & Self ) - > & Self T {
31 return & self . 0 ;
32 }
33
34 fn other ( self : & Self as S , other : & Self as O ) - > & O T {
35 return & other . 0 ;
36 }
37 }
38
39 fn demo_methods ( ) {
40 let p1 : Pair ( int ) = ( 1 , 2 ) ;
41 let p2 : Pair ( int ) = ( 3 , 4 ) ;
42
43 let r1 = p1 . first ( ) ;
44 let r2 = p1 . other ( & p2 ) ;
45 print ( r1 ) ;
46 print ( r2 ) ;
47 }
48
49 // 4) Higher-order function: label flows through function type
50 fn map_head ( xs : & Vec ( T ) as A , f : Fn ( & A T ) - > U ) - > & A U {
51 return f ( & xs [ 0 ] ) ;
52 }
53
54 fn demo_hof ( ) {
55 let nums : Vec ( int ) = [ 1 , 2 , 3 ] ;
56 let head_ref = map_head ( & nums , fn ( x : & int ) - > & int { return x ; } ) ;
57 print ( head_ref ) ;
58 }
59
60 // 5) Multiple inputs require label: `as A` disambiguates the return
61 fn pick ( a : & T as A , b : & T ) - > & A T {
62 // body could choose either; label tells the checker the result is tied to `a`
63 return a ;
64 }
65
66 // 6) Optional: Outlives relation (advanced)
67 fn choose_longer ( a : & T as X , b : & T as Y ) - > & X T where Y : X {
68 return a ;
69 }
70
71 // 7) Struct constructor with label reuse
72 struct Window ( T ) { head : & A T , tail : & B T }
73
74 fn mk_window ( xs : & Vec ( T ) as A , ys : & Vec ( T ) as B ) - > Window ( T ) {
75 return Window { head : & xs [ 0 ] , tail : & ys [ 0 ] } ;
76 }
77
78 fn demo_window ( ) {
79 let xs : Vec ( int ) = [ 1 , 2 , 3 ] ;
80 let ys : Vec ( int ) = [ 4 , 5 , 6 ] ;
81 let w = mk_window ( & xs , & ys ) ;
82 print ( w . head ) ;
83 print ( w . tail ) ;
84 }
85
86 // 8) Diagnostics-friendly failure (commented):
87 // fn bad_pick(a: &T, b: &T) -> &T {
88 // if cond { return a; } else { return b; }
89 // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`.
90 // }

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

Example
0 let s : string = "hi" ;
1 let r = & s ; // borrow starts
2 print ( r ) ; // last use of r
3 var t = s ; // OK allowed: r’s region ended at last use (lexically-free)

L1 — Loan Creation

Example
0 var x : int = 0 ;
1 let r = & x ; // L(x, shared)
2 let m = & mut x ; // Not OK conflict later under A1, but creation itself establishes L(x, unique)

L2 — Loan Propagation

Example
0 fn id_ref ( p : & int ) - > & int { p }
1 let x : int = 1 ;
2 let r1 = & x ; // L(x, shared)
3 let r2 = id_ref ( r1 ) ; // loan propagates to r2 until last use
4 print ( r2 ) ; // OK!

A1 — Unique Exclusivity

Example
0 var v : int = 0 ;
1 let m = & mut v ; // L(v, unique)
2 let r = & v ; // Not OK! A1: unique excludes any concurrent shared borrow

A2 — Shared Read‑Only

Example
0 var n : int = 0 ;
1 let a = & n ; // L(n, shared)
2 let b = & n ; // another shared loan
3 print ( * a + * b ) ; // OK! reads allowed
4 n = 5 ; // Not OK! A2: write while shared loans alive

I1 — Write Invalidates

Example
0 var s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ;
3 s . push ( " ! " ) ; // Not OK! I1: write to s while shared loan alive (if r not yet last‑used)

I2 — Move Invalidates

Example
0 var s : string = "a" ;
1 let r = & s ; // L(s, shared)
2 var t = s ; // Not OK! I2: move invalidates loans; r would dangle

I3 — Overlap/Fields

Example
0 struct P { x : int , y : int }
1 var p : P = P { x : 1 , y : 2 } ;
2 let mx = & mut p . x ; // L(p.x, unique)
3 let my = & mut p . y ; // OK, disjoint fields: allowed
4
5 var arr : [ int ; 3 ] = [ 0 , 1 , 2 ] ;
6 let a = & mut arr [ 0 ] ;
7 let b = & mut arr [ 1 ] ; // not OK, if indices distinct constants
8 let i = 0 ; let j = read_index ( ) ;
9 let c = & mut arr [ i ] ;
10 let d = & mut arr [ j ] ; // Not OK conservatively, may overlap unless proven disjoint (use split helpers)

U1 — Use Requires Alive

Example
0 let s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ; // OK! use while alive
3 // after last use r ends; any further use would be not OK (dead borrow)

U2 — No After‑Free

Example
0 fn bad ( ) {
1 let s : string = "x" ;
2 let r = & s ;
3 drop ( s ) ; // base place dead
4 print ( r ) ; // Not OK: U2: use after base death
5 }

RB1 — Shared from Unique

Example
0 var v : int = 0 ;
1 let mu = & mut v ; // L(v, unique)
2
3 // Shared reborrow of the same place (auto-deref from &mut int to int)
4 let rs : & int = & mu ; // creates L(v, shared)
5
6 print ( rs ) ;
7
8 // Write through the unique borrow (auto-deref on assignment)
9 mu = 3 ; // must end shared loan before writing via `mu`

RB2 — Unique from Unique (optional v1)

Example
0 var v : int = 0 ;
1 let mu1 = & mut v ;
2 let mu2 = & mut mu1 ; // unique reborrow of v; allowed only if no overlapping use via mu1

E1 — No Escaping Borrows

Example
0 fn leak_ref ( ) - > & int {
1 let x : int = 1 ;
2 return & x ; // Not OK! Escapes to caller; Not OK, dies at function end
3 }
4
5 fn head ( s : & string ) - > & char {
6 return & s [ 0 ] ;
7 } // OK! Summary ties return to arg

M1 — Binding Mutability

Example
0 let x : int = 0 ;
1 let rx = & mut x ; // Not OK: M1: &mut requires mutable base
2 var y : int = 0 ;
3 let ry = & mut y ; // OK

M2 — No Shared Mutability Without Atomics

Example
0 shared var n : int = 0 ; // shared location
1 let r1 = & n ; let r2 = & n ; // shared borrows
2 n = n + 1 ; // Not OK concurrent write without atomic discipline
3 atomic var a : int = 0 ; // with atomic, writes are allowed by policy

T1 — Temporaries

Example
0 print ( & ( make_string ( ) ) ) ; // OK temporary lives through call; reference dies at last use
1 let r = & ( make_string ( ) ) ;
2 print ( r ) ; // Not OK if r would outlive the temporary’s last use

T2 — Branches/Loops/Match

Example
0 let s : string = "x" ;
1 let r = & s ;
2 if cond { print ( r ) ; } else { print ( r ) ; }
3 // r is used on both paths; live set at join = intersection ⇒ still alive until after the if
4 var t = s ; // not OK must occur after r’s last use on all paths

F1 — FFI Preconditions

Example
0 ffi puts : ( & char ) - > int = . . . ;
1 let s : string = "hi" ;
2 let r = & s [ 0 ] ;
3 puts ( r ) ; // OK if FFI summary: does not retain; Not OK if it may retain (escape)

F2 — FFI Postconditions

Example
0 ffi c_strchr : ( & char , int ) - > & char = . . . ; // trusted: result aliases input
1
2 fn first_a ( s : & string ) - > & char {
3 c_strchr ( & s [ 0 ] , 'a' ) // OK allowed only because summary ties result to arg region
4 }

RFT1 — Refinement Well‑Formedness

Example
0 let x : int = 5 ;
1 let y : { z : & int where initialized ( z ) } = { z : & x } ; // OK predicate references lifetime‑relevant property

RFT2 — Discharge at Use Sites

Example
0 fn show ( p : { z : & int where not_escaped ( z ) } ) - > void {
1 print ( p . z ) ; // OK! checker discharges `not_escaped` from current loan facts
2 }

inter‑Procedural Summary (Elision)

Example
0 fn get_first ( a : & [ int ] ) - > & int {
1 return & a [ 0 ] ;
2 }
3
4 // elaborated internally: for<ρ> fn(&ρ [int]) -> &ρ int
5 // caller instantiates ρ from its argument; return tied to same ρ

Structs with Reference Fields (Implicit Regions)

Example
0 struct Node ( T ) { data : & T } // elaborates to Node<ρ, T>
1
2 fn demo ( ) - > void {
3 let x : int = 1 ;
4 var n : Node ( int ) = Node { data : & x } ; // OK n: Node<ρx, int>
5 }
6
7 fn bad ( ) - > void {
8 var n : Node ( int ) ;
9
10 {
11 let x : int = 1 ;
12 n = Node { data : & x } ; // Not OK n outlives x ⇒ region check fails
13 }
14 }

Async Phase 1 — No Unique Loans Across Await

Example
0 async fn step ( mut v : & int ) - > void {
1 let m = v ; // borrow unique via parameter
2 await tick ( ) ; // Not OK, unique loan across await in phase 1
3 }

Closures — Capture Classification

void { move x }; // by‑value move ⇒ FnOnce" lang="aela" title="Example" id="e459ee693aab5">
Example
0 var n : int = 0 ;
1 let c1 = fn ( ) - > void { print ( & n ) ; } ; // shared borrow capture ⇒ Fn
2 let c2 = fn ( ) - > void { n = n + 1 ; } ; // unique borrow capture ⇒ FnMut
3 let x : string = "hi" ;
4 let c3 = fn ( ) - > void { move x } ; // by‑value move ⇒ FnOnce

RTOS Harmony

Linux Setup

You most likely need to edit your udev rules

Example
0 sudo curl - L - o / etc / udev / rules . d / 50 - cmsis - dap . rules \
1 https : / / raw . githubusercontent . com / pyocd / pyOCD / main / udev / 50 - cmsis - dap . rules

If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.

Example
0 lsusb | grep - iE 'arduino|cmsis|dap|renesas'
1 Bus 001 Device 005 : ID 2341 : 1002 Arduino SA . . .

Replace ID VVVV:PPPP

Example
0 # Arduino UNO R4 WiFi (CMSIS-DAP) — custom rule
1 SUBSYSTEM = = "usb" , ATTR { idVendor } = = "VVVV" , ATTR { idProduct } = = "PPPP" , MODE : = "0666"
2 SUBSYSTEM = = "hidraw" , ATTRS { idVendor } = = "VVVV" , ATTRS { idProduct } = = "PPPP" , MODE : = "0666"

Reload, re-enumerate

Example
0 sudo udevadm control - - reload - rules
1 sudo udevadm trigger

Unplug & Replug, press the reset button & then check:

Example
0 pyocd list

Zephyr

Install

Example
0 git cmake ninja python python - pip dtc wget

Install the Zephyr CLI tool

Example
0 pip install west

Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.

Example
0 sudo usermod - a - G dialout $USER

Create a project directory. Create a python environment in the project directory. Initialize it as a new zephyr project. Run the update command to get all the sub-repos.

Example
0 mkdir ~ / projects / z
1 python - m venv ~ / projects / z / . venv
2 west init ~ / projects / z
3 west update

Go back to your projects root and get the minimal SDK for cross compiling.

Example
0 cd ~ / projects
1 wget https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz

Calculate the SHA sum if you want

Example
0 wget - O - https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / sha256 . sum | shasum - - check - - ignore - missing

Extract the SDK and run the setup

Example
0 tar xvf zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz
1 cd ~ / projects / zephyr - sdk - 0 . 17 . 4
2 . / setup . sh

Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)

Example
0 # 1. Navigate to your project directory
1 cd ~ / projects / z
2
3 # 2. Activate the Python virtual environment for 'west'
4 source . / . venv / bin / activate
5
6 # 3. Manually export the SDK path to ensure it's found
7 export ZEPHYR_SDK_INSTALL_DIR = ~ / projects / zephyr - sdk - 0 . 17 . 4
8
9 # 4. Source the Zephyr environment to link everything together
10 source . / zephyr / zephyr - env . sh
11
12 # 5. Install a shit ton of dependencies
13 pip - 3 install - r zephyr / scripts / requirements . txt

Compile & Flash Test

Finally, build an Arduino image. I use Blinky here because its super simple and makes sense to start with as a sanity test.

Example
0 west build - p auto - b arduino_uno_r4 zephyr / samples / blinky
1 west flash

Integrating with Aela

Aela can output object files, so it's very simple to create a Zephyr project with Aela by just adding CMakeLists.txt and prj.conf files.

Example
0 myapp /
1 ├─ CMakeLists . txt
2 ├─ prj . conf
3 ├─ index . json
4 └─ index . ae

Example prj.conf

Example
0 # Prefer minimal libc over newlib (if you don’t need full POSIX/locale/etc.)
1 CONFIG_NEWLIB_LIBC = n
2 CONFIG_MINIMAL_LIBC = y
3 # If you must use newlib, at least disable float printf/scanf:
4 # CONFIG_NEWLIB_LIBC_FLOAT_PRINTF=n
5 # CONFIG_NEWLIB_LIBC_FLOAT_SCANF=n
6
7 # Logging/printk/console (turn off what you don't need)
8 CONFIG_PRINTK = n
9 CONFIG_LOG = n
10 # or, if you need logs:
11 # CONFIG_LOG=y
12 # CONFIG_LOG_MODE_MINIMAL=y
13 # CONFIG_LOG_DEFAULT_LEVEL=0
14
15 # Shell/console features often sneak in via defaults
16 CONFIG_CONSOLE = n
17 CONFIG_UART_CONSOLE = n
18 CONFIG_SHELL = n
19
20 # Link-time optimization can trim more
21 CONFIG_LTO = y
22 CONFIG_SIZE_OPTIMIZATIONS = y
23
24 # Assertions & debug
25 CONFIG_ASSERT = n
26 CONFIG_DEBUG = n
27 CONFIG_DEBUG_INFO = n # (debug symbols only affect .elf, not .bin size)
28
29 # Heap & stacks
30 CONFIG_HEAP_MEM_POOL_SIZE = 0 # if you don’t malloc at all
31 CONFIG_MAIN_STACK_SIZE = 1024 # tune as low as your app can tolerate

Example CMakeLists.txt

${AELA_OBJ}" VERBATIM ) add_library(aela_objects OBJECT ${AELA_OBJ}) set_source_files_properties(${AELA_OBJ} PROPERTIES GENERATED TRUE) # Link your Aela object (contains `main`) into the Zephyr app target_link_libraries(app PRIVATE aela_objects)" lang="cmake" title="Example" id="2051be01a6894">
Example
0 cmake_minimum_required ( VERSION 3 . 20 )
1 find_package ( Zephyr REQUIRED HINTS $ENV { ZEPHYR_BASE } )
2 project ( myapp )
3
4 # You can also pass these with: -DAEC=/path/aec -DAEC_FLAGS="..."
5 set ( AEC "aec" CACHE FILEPATH "Path to Aela compiler" )
6 set ( AEC_FLAGS "" CACHE STRING "Extra flags for Aela" )
7
8 # Optional: mirror Zephyr’s CPU/FPU flags so the .o matches the board ABI
9 # (We read what Zephyr passes to the C toolchain and reuse the ARM-related bits.)
10 get_property ( _Z_OPTS TARGET zephyr_interface PROPERTY INTERFACE_COMPILE_OPTIONS )
11 set ( _AE_ARM_OPTS "" )
12 foreach ( opt IN LISTS _Z_OPTS )
13 if ( opt MATCHES " ^ - m ( cpu | thumb | float - abi | fpu ) " ) ; list ( APPEND _AE_ARM_OPTS "$ { opt } " ) ; endif ( )
14 endforeach ( )
15
16 set ( AELA_SRC $ { CMAKE_CURRENT_SOURCE_DIR } / myprog . ae )
17 set ( AELA_OBJ $ { CMAKE_CURRENT_BINARY_DIR } / aela / myprog . obj . o )
18
19 add_custom_command (
20 OUTPUT $ { AELA_OBJ }
21 COMMAND $ { CMAKE_COMMAND } - E make_directory $ { CMAKE_CURRENT_BINARY_DIR } / aela
22 COMMAND $ { AEC } $ { AEC_FLAGS } $ { _AE_ARM_OPTS } - c $ { AELA_SRC } - o $ { AELA_OBJ }
23 DEPENDS $ { AELA_SRC }
24 COMMENT "Aela : $ { AELA_SRC } - > $ { AELA_OBJ } "
25 VERBATIM
26 )
27
28 add_library ( aela_objects OBJECT $ { AELA_OBJ } )
29 set_source_files_properties ( $ { AELA_OBJ } PROPERTIES GENERATED TRUE )
30
31 # Link your Aela object (contains `main`) into the Zephyr app
32 target_link_libraries ( app PRIVATE aela_objects )

Compiling

Example
0 west build - b arduino_uno_r4_wifi myapp - p \
1 - DCMAKE_EXPORT_COMPILE_COMMANDS = ON \
2 - DAEC = $ ( command - v aec )
3 west flash

Note

The _AE_ARM_OPTS trick copies exactly the -mcpu/-mfpu/-mfloat-abi/-mthumb flags Zephyr uses for this board, so your Aela object links ABI-cleanly without you guessing the right combo. (UNO R4 WiFi is a Cortex-M4; Zephyr’s board page confirms the arch.)

FreeRTOS

Discover Platform Build Flags

Lets assume an Arduino R4 here as an example.

We need to "spy" on the Arduino CLI to get the exact compiler and linker flags required for the R4 WiFi. The Aela build system will pass these directly to its underlyng C compiler. Arduino code files are called "sketches".

  1. Create a dummy sketch:
temp_sketch/temp_sketch.ino" lang="bash" title="Example" id="2274fcd531ebc">
Example
0 mkdir temp_sketch
1 echo " void setup ( ) { } void loop ( ) { } " > temp_sketch / temp_sketch . ino
  1. Run a verbose compile:
Example
0 arduino - cli compile - - fqbn arduino : renesas_uno : unor4wifi - - verbose temp_sketch
  1. Find and copy the linker command. Scroll through the output and find the longest command, which will start with something like .../arm-none-eabi-g++ ... . It will be a very long line that links all the object files and libraries together. Copy this entire command into a text editor. We're going to use its flags.

It will look something like this (shortened for clarity): .../arm-none-eabi-g++ -Os -Wl,--gc-sections -mcpu=cortex-m4 ... -L/path/to/build -Wl,--start-group -lArduinoCore -lrtos -lm -Wl,--end-group ...

We will now transfer the important parts of that command into your index.json .

Step 2: Project Structure

Organize your project with your source code inside a src directory.

Example
0 aela_freertos_blinky /
1 ├── index . json # The project manifest (our main focus)
2 └── src /
3 ├── main . ae # Your Aela application logic
4 └── shim . c # The C entry-point shim

Step 3: The index.json Manifest

This is the control center. We'll define a custom platform target called "arduino_r4" and place all the flags we discovered into the link section.

Create the file `index.json` (unless it was created via aec init ):

Example
0 {
1 "name" : "aela - freertos - blinky" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4
5 "sources" : {
6 "shared" : [
7 "src / shim . c"
8 ]
9 } ,
10
11 "link" : {
12 "platform" : {
13 "arduino_r4" : [
14 " - mcpu = cortex - m4" ,
15 " - mthumb" ,
16 " - mfloat - abi = hard" ,
17 " - mfpu = fpv4 - sp - d16" ,
18
19 " - Os" ,
20 " - Wl , - - gc - sections" ,
21 " - Wl , - - script = / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI / linker_script . ld" ,
22
23 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / cores / arduino" ,
24 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI" ,
25 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / libraries / Arduino_FreeRTOS / src" ,
26
27 " - L / tmp / arduino / build - 123456789 . . . " ,
28
29 " - Wl , - - start - group" ,
30 " - lArduinoCore" ,
31 " - lrtos" ,
32 " - lm" ,
33 " - Wl , - - end - group"
34 ]
35 }
36 }
37 }

Note

You must replace the placeholder paths ( /home/user/... , /tmp/arduino/... ) with the full, absolute paths you copied from your verbose compiler output in Step 1.

Step 4: The Source Code

The source code is the same as before, but now it lives in the src/ directory.

src/main.ae

src/main.ae
0 // FFI Declarations for C functions
1 struct TaskHandle_t ;
2 type TaskFunction_t = fn ( & void ) - > void ;
3
4 ffi pinMode = fn ( u32 , u32 ) - > void ;
5 ffi digitalWrite = fn ( u32 , u32 ) - > void ;
6 ffi xTaskCreate = fn ( TaskFunction_t , string , u32 , & void , u32 , & TaskHandle_t ) - > i32 ;
7 ffi vTaskStartScheduler = fn ( ) - > void ;
8 ffi vTaskDelay = fn ( u32 ) - > void ;
9
10 // Constants
11 let LED_BUILTIN : u32 = 13 ;
12 let OUTPUT : u32 = 1 ;
13 let HIGH : u32 = 1 ;
14 let LOW : u32 = 0 ;
15
16 // The task that will blink the LED.
17 fn blinkTask ( params : & void ) - > void {
18 pinMode ( LED_BUILTIN , OUTPUT ) ;
19 while ( true ) {
20 digitalWrite ( LED_BUILTIN , HIGH ) ;
21 vTaskDelay ( 500 ) ;
22 digitalWrite ( LED_BUILTIN , LOW ) ;
23 vTaskDelay ( 500 ) ;
24 }
25 }
26
27 // Main entry point called from our C shim.
28 export fn aela_rtos ( ) - > void {
29 xTaskCreate ( blinkTask , "Blinker" , 128 , null , 1 , null ) ;
30 vTaskStartScheduler ( ) ;
31 }

src/shim.c

src/shim.c
0 #include
1
2 // Declare the external function defined in our Aela code.
3 extern void aela_rtos ( ) ;
4
5 // Standard Arduino entry point.
6 void setup ( ) {
7 aela_rtos ( ) ;
8 }
9
10 // loop() will never be reached, but must exist to link correctly.
11 void loop ( ) { }

Step 5: Build and Flash

You tell the Aela compiler what you're targeting, and it uses the manifest to set the correct build flags.

Build the project for the target triple:

Example
0 # This command tells Aela to cross-compile for the specified target.
1 # It will then find the "thumbv7em-none-eabihf" key in your index.json.
2 aec build - - platform = "arduino_r4" - - target thumbv7em - none - eabihf

Flash the output. The build process should still result in a .uf2 file in a build directory. You can then flash it with the Arduino CLI as before.

Example
0 arduino - cli upload - - fqbn arduino : renesas_uno : unor4wifi - - input - file build / aela - freertos - blinky . uf2

FAQ

Why is Aela 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.

Overview

Aela is a commercial-source language for embedded systems.

Aela is a compiled, memory-safe language with a strong, static type system. It started in 2018 as a fork of Rust, but has diverged significantly to service embedded systems use cases. It has a similar syntax and sticks to many of the same goals such as ownership semantics, memory and concurrency safety, only pay for what you use, and zero-cost abstractions.

Programming Language Landscape

This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.

image.png

Langauge Goals

All language design decisions revolve around determinism and performance for embedded systems.

Aela also focuses on harmony with C and C++. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like write(2) .

Language Goals

All language design decisions revolve around providing absolute determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is eliminated. All excluded features have an ideal alternative (see documentation) or have been simply omitted.

Excluded Feature Justification
Panics Panics are not in the type signature; they violate the principle of abstraction and create a hidden, unrecoverable failure path that bypasses the type system.
Exceptions Exceptions create hidden, non-local control flow paths that are impossible to reason about statically and incur runtime overhead. Error handling must be explicit.
Global State Global variables create hidden dependencies and introduce non-determinism, making concurrency unsafe and program behavior impossible to reason about locally.
Lifetime Annotations Explicit lifetime annotations are a significant source of complexity and syntactic noise. The compiler must be smart enough to infer ownership duration without burdening the programmer.
Macros Macros create non-linear, hard-to-debug code flow ("magic"). Code must be explicit and analyzable; what you see is what the compiler gets, ensuring predictability and toolability.
unsafe keyword The unsafe keyword is an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of unsafe operations rather than entire blocks.
Attributes Attributes are a form of meta-programming that injects non-local behavior and hidden complexity. They modify code in non-obvious ways, violating the principle that code should be explicit.
Pointer Arithmetic Direct pointer manipulation is a primary source of memory safety vulnerabilities (e.g., buffer overflows). Safe, bounds-checked slice operations are the only acceptable alternative.
Advanced Traits Complex trait systems lead to baroque, unreadable type signatures and cryptic compiler errors. Simplicity and clarity are prioritized over abstract expressive power.
Inline Assembly Inline assembly is non-portable, opaque to the optimizer, and breaks static analysis. Low-level routines must be provided via a stable C ABI, ensuring a clean contract.
null keyword Null pointers are the source of countless runtime crashes. The absence of a value must be explicitly represented and handled in the type system (e.g., via Option ).
Operator Overloading Operator overloading makes code ambiguous and hides the cost of operations. Function calls must be explicit to ensure code clarity and predictable performance.
Implicit Conversions Implicit conversions hide potential bugs, such as data truncation or precision loss. All type conversions must be explicit, forcing the programmer to acknowledge the operation.

Feature Comparison

Feature Aela C C++ Rust Ada
Compile-Time Memory Safety √ √ √
Cold Build Speed √ √ √
Reference Counted √ √
Automatic RAII √ √
Formal Verification √ √
Dependent & Refinement Types √
Language-Native Concurrency √
Structured Concurrency √ √
Automatic C/C++ safe binding √

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 won't 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

- /path/to/my-app/index.json
0 {
1 "name" : "my - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae"
4 }

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

- index.json for a project that uses a UI library
0 {
1 "name" : "my - gui - app" ,
2 "version" : "1 . 0 . 0" ,
3 "entry" : "src / app . ae" ,
4 "dependencies" : {
5 "ui" : " . . / libs / aela - ui" ,
6 "database" : " . . / libs / aela - db"
7 }
8 }

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

- ../libs/aela-ui/src/window.ae
0 // This struct can be imported by other modules.
1 export struct WindowOptions {
2 title : string ,
3 width : int ,
4 height : int ,
5 }
6
7 // This function is private to the window.ae module.
8 fn internal_helper ( ) - > void {
9 // ...
10 }

Re-exports

- re-export pattern
0 import { Thing1 , Thing2 } from "things . ae" ;
1
2 export Thing1 ;
3 export Thing2 ;

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

";" lang="" title="Example" id="b68adefb69265">
Example
0 import from " " ;

Example

void { // Access symbols using the `::` namespace operator. let opts: &ui::WindowOptions = new ui::WindowOptions(); helpers::do_something(); }" lang="example" title="- src/app.ae" id="027e17636df19">
- src/app.ae
0 // Import the "ui" package, which was defined in index.json.
1 import ui from "ui" ;
2
3 // Import a local utility file using a relative path.
4 import helpers from " . / helpers . ae" ;
5
6 fn main ( ) - > void {
7 // Access symbols using the `::` namespace operator.
8 let opts : & ui : : WindowOptions = new ui : : WindowOptions ( ) ;
9 helpers : : do_something ( ) ;
10 }

Named Imports

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

Syntax

";" lang="" title="Example" id="9905825be2237">
Example
0 import { , : } from " " ;

Example EXAMPLE

void { // `Window` can be used directly. let win: &Window = new Window(); // `WindowOptions` is available under the alias `Options`. let opts: &Options = new Options(); }" lang="example" title="- src/app.ae" id="3192e955d263e">
- src/app.ae
0 import { Window , WindowOptions : Options } from "ui" ;
1
2 fn main ( ) - > void {
3 // `Window` can be used directly.
4 let win : & Window = new Window ( ) ;
5
6 // `WindowOptions` is available under the alias `Options`.
7 let opts : & Options = new Options ( ) ;
8 }

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

- index.json for an app with native UI code on macOS
0 {
1 "name" : "aela - native - app" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4 "sources" : {
5 "darwin" : [ "src / native / apple . mm" ]
6 } ,
7 "link" : {
8 "platform" : {
9 "darwin" : [
10 " - framework" , "Foundation" ,
11 " - framework" , "AppKit" ,
12 " - framework" , "ObjectiveC"
13 ]
14 }
15 }
16 }

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.

Failures

A primary cause of software defects, security vulnerabilities, and developer anxiety is the "Trust Gap": the difference between what a function's signature claims it does and what its implementation can actually do. Aela is designed to eliminate this gap. Its error and fault handling system is built on a single, non-negotiable principle: a function's signature must be a complete and honest contract, and the compiler must enforce it.

Don't Try-Catch

Traditional exception systems, common in languages like Java, JavaScript, C++, and Python, introduce a form of hidden control flow. A throw or raise statement is a non-local goto that is often invisible in the function's signature.

Consider a typical function in such a language: function get_user(id: int) -> User

This signature makes a simple promise: "Give me an integer, and I will give you a User." However, the implementation might throw a DatabaseConnectionException, a UserNotFoundException, or a NullPointerException. To understand the function's true behavior, the developer must embark on a research project: reading the documentation (which may be out of date), reading the source code, and reading the source of every function it calls.

This breaks a developer's ability to reason locally about the code.

Don't Panic

Some modern languages, notably Rust, attempt to solve error handling this by creating a two-tiered system:

  • Recoverable Errors ( Result ): For expected failures (e.g., file not found). These are part of the type signature.
  • Unrecoverable Bugs ( panic! ): For programmer errors (e.g., index out of bounds). These are not part of the type signature.

While an improvement, this still creates a hidden side-channel for bugs. More critically, the panic! mechanism creates a deep schism between platforms, especially for embedded systems.

The unwind vs. abort Schism:

On servers, panic! defaults to unwind, a slow and complex process that runs cleanup code (destructors). This adds a significant "tax" to the binary size, which is unacceptable on resource-constrained devices.

On embedded systems, developers are forced to configure panics to abort, which immediately halts the program.

The Broken Promise of abort: When panic = "abort" is used, the language's core safety promise—that resources will be cleaned up on failure (RAII via Drop in Rust)—is broken. Destructors are never called. A MutexGuard will leave a mutex permanently locked. A peripheral that was supposed to be disabled is left in an active state. The very code written to ensure safety on failure becomes useless.

This patched-together model is not a first-principles solution. Aela requires a single, unified system that is safe, deterministic, and efficient on all platforms.

The Fault Model

The Principle of the Honest Contract: Aela avoids ambiguity in failure handling by enforcing that the outcome of a function must be encoded in its signature.

Function Signatures

A function declares its potential to terminate due to an unrecoverable logic bug by using the | operator in its return type. This operator separates the single success type from a list of one or more fault types.

fn get_at(slice: &[u8], index: int) -> u8 | OutOfBounds;

This signature is an honest contract. It tells any caller: "This function will either return a u8 , or it will terminate with an OutOfBounds fault. There are no other possibilities."

The fault and raise Keywords

  • `fault` : A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from struct or enum , which represent data and recoverable errors.
  • fault OutOfBounds(index: int, len: int);
  • `raise` : A keyword that triggers a fault. It immediately stops the current function's execution and propagates the fault to the caller. raise is considered a terminal action.
  • raise OutOfBounds(index: index, len: len);

The Standard match Statement

The match statement is how Aela handles the outcome of functions that may terminate with faults.

Example
0 match ( expression ) {
1 pattern1 = > { . . . } ,
2 pattern2 = > { . . . } , // potentially a fault type!
3 . . .
4 }

Semantic Rules

The safety and special behavior of fault handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:

If the expression being evaluated by a match statement has a fault path in its signature (i.e., contains a | ), then the compiler enforces a "Terminal Arm Rule" on any arm that matches a fault -declared type.

This rule is context-dependent. It is triggered by the signature of the function being called, not just the type of the pattern. This is the key insight that resolves all ambiguity.

The "Terminal Arm Rule" is defined as: The block of the arm must end with a terminal statement. Aela does not have implicit returns, so this is a direct check of the final statement in the block.

Terminal statements are:

  • raise ;
  • std::abort();
  • std::halt();
  • std::reboot();

Note

pure fn ketword must not introduce or handle faults; they cannot have a | in their return type and cannot raise.

Note

Faults must not cross FFI; board/FFI shims must convert faults to domain-appropriate codes or terminals.

Note

AP131 outlines a proposal to have return be the equivalent of raise . Allowing both and specifying that they’re identical.

Note

AP132 outlines a proposal to permit functions to be generic over an open set of faults (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;

Note

AP134 outlines a proposal to add a desugaring operator. let b = get_at(xs, 0)?; // expands to match/raise

Complete Examples: The Rule in Practice

These two examples demonstrate how the context-dependent rule creates a safe and unambiguous system.

Example 1: Handling a Live Fault Event

Example
0 // The compiler sees the '|' in the signature, so it activates the Terminal Arm Rule for this match.
1 match ( create_packet ( user_size ) ) {
2 Some ( packet ) = > { /* This arm is normal. */ } ,
3 None = > { /* This arm is normal. */ } ,
4
5 // The compiler sees that `PacketTooLarge` is a `fault` type and applies the rule.
6 f : PacketTooLarge = > {
7 log : : critical ( "Logic error : Invalid packet size requested . " , f ) ;
8 // The block ends with a known terminal keyword. The code is valid.
9 std : : reboot ( ) ;
10 }
11 }

If reboot; were omitted, the compiler would issue a clear error: "Fault-handling arm must end with a terminal statement."

Example 2: Inspecting a Fault as Data

Example
0 // This function returns a fault object as a value. Its signature has NO '|'.
1 fn inspect_issues ( ) - > PacketTooLarge ;
2
3 // The compiler sees NO '|' in the signature, so it DOES NOT activate the Terminal Arm Rule.
4 match ( inspect_issues ( ) ) {
5
6 // Even though `PacketTooLarge` is a `fault` type, the rule is not active.
7 // This arm is treated as a normal pattern match.
8 f : PacketTooLarge = > {
9 log : : warn ( "A non - critical issue was detected : " , f ) ;
10 // The block is allowed to complete normally. The code is valid.
11 }
12 }

Memory & Mutability

1. Default Allocation Semantics

  • All values start on the stack by default.
  • Stack allocations are:
  • Fast
  • Scoped
  • Owned directly by the binding.
Example
0 let foo : Foo = { num : 0 } ; // Foo is stack-allocated

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.

Example
0 let x : & T = new { . . . val } ; // Allocate on the heap
1 let x : & T = new shared { . . . val } ; // Single-threaded, mutable
2 let x : & T = new shared atomic { . . . val } ; // Thread-safe atomic
3 var x : & T = new weak { . . . val } ; // Mutable weak reference
4 var x : & T = new static { . . . val } ; // New without malloc
5 var x : & T = new static atomic { . . . val } ; // New without malloc, Thread-safe atomic

Behavior of new Modifiers

Modifier Behavior Description
(none) Heap Allocation (OS based allocator). Returns a handle/reference to a freshly allocated object, immutable and can not be loaned.
shared Heap. Shared ownership, single-threaded. Allowed to be loaned; not thread-safe; not Send/Sync-like.
shared atomic Heap. Shared ownership, thread-safe. Reference counts and interior coordination use atomics; Send/Sync if T satisfies the “atomic-safe” requirements you define.
weak Heap, weak handle to a shared object. Does not keep the allocation alive; must be paired with at least one strong shared/shared atomic owner somewhere to be useful.
static Static storage, no OS allocator. Object is placed/constructed in static memory (BSS/RODATA/flash/SECTION), suitable for bare-metal/MCUs. Lifetime: program-long (or until explicitly torn down by system semantics).
static atomic Static storage, thread-safe coordination via atomics. Shared global counters updated in ISR + mainline, Lock-free buffers (ring buffers for UART, DMA, etc.). Configuration/state variables read by multiple cores or ISRs. On a simple single-core MCU with no interrupts, it’s redundant but harmless.
  • 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 :

Keyword Meaning
let Immutable binding (read-only)
var Mutable binding (read-write)
  • The mut keyword is not necesasry here.
  • Mutability is not encoded in types, structs, or fields.
  • let and var are both lexically scoped.

Example

Example
0 let a : & Foo = new shared { . . . foo } ; // Immutable heap reference
1 var b : & Foo = new shared { . . . foo } ; // Mutable heap reference

Note

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

4. Weak References & Cycle Prevention

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'

Example
0 if let strong_ref = weak_ref {
1 // This block only runs if the object is still alive.
2 // 'strong_ref' is a new, temporary strong reference of type &Foo.
3 strong_ref . do_something ( ) ;
4 }

5. Copying Stack Values

  • Heap allocation requires copying the stack value:
Example
0 new shared { . . . foo } // `{ ...foo }` performs a field-wise copy
  • This avoids moving ownership from the stack. Moves are not allowed .

5. Reference Types and Behavior

Kind Syntax RC Type Thread-Safe Mutable
Stack value let x: T = ... None N/A No
Heap reference let x: &T = new shared {...} RC No No
Heap reference (mutable) var x: &T = new shared {...} RC No Yes
Heap reference (atomic) let/var x: &T = new shared atomic {} ARC Yes Depends

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.
a copy of the number 10 is passed. // bar(stack_str); -> a copy of the {ptr, i64} struct is passed." lang="example" title="- Stack Allocated" id="5096a1ef49907">
- Stack Allocated
0 let stack_int : i32 = 10 ; // The variable 'stack_int' IS the number 10.
1 let stack_str : string = "hello" ; // The variable 'stack_str' IS the {ptr, i64} struct.
2
3 // When calling a function:
4 // foo(stack_int); -> a copy of the number 10 is passed.
5 // bar(stack_str); -> a copy of the {ptr, i64} struct is passed.

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.
- Heap allocated via new
0 let heap_int : i32 = new 42 ; // 'heap_int' is a POINTER to a box containing 42.
1 let heap_obj : MyStruct = new { } ; // 'heap_obj' is a POINTER to a box containing a MyStruct.
2 let heap_arr : u8 [ ] = new [ 1 , 2 , 3 ] ; // 'heap_arr' is a POINTER to a box for the array data.
3
4 // When calling a function:
5 // foo(heap_int); -> a copy of the POINTER is passed. The heap data is not touched.

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.
- Special Case
0 let captured_var = new "text" ;
1
2 let my_closure = fn ( ) {
3 print ( captured_var ) ; // Captures the pointer 'captured_var'.
4 } ;
5
6 // 'my_closure' is a {func_ptr, env_ptr} struct.
7 // 'env_ptr' points to a heap box which contains a copy of the 'captured_var' pointer.

Refinement & Dependent Types

TL;DR: Refinement & dependent types are types that embed logical conditions or values themselves, making illegal states unrepresentable by construction.

If you're coming from languages like JavaScript, C++, or Rust, you're used to type systems that check the shape of your data. For example, a type checker ensures you don't use a string where a number is expected.

Aela takes this a step further with refinement types and dependent types . These are features that allow the type system to understand and check the values of your data, not just their shape. It's more rigorous that shape checking, it's a value-aware check that happens entirely at compile time .

Motivation

Most type systems validate shape (ie., "this is an int "). Aela also validates value-level facts : a string is non-empty , an integer is non-zero , a vector’s length matches what your function promises. This turns bugs into compile‑time errors and makes code self-documenting.

  • Earlier feedback: logical mistakes become type errors you see during compilation.
  • Stronger intent: types like NonEmptyString and NonZeroint tell the reader (and the compiler) exactly what you mean.
  • Confidence: fewer defensive checks sprinkled across your code.

Compile-Time VS. Run-Time Arguments

Aela uses a single parameter list for functions, with an optional compile-time section separated from the run-time section by a semicolon ; . Parameters are separated by commas. If a parameter has a type annotation, it will be considered a value parameter. If a value has no type annotation, it will be considered a type.

Example
0 fn f ( T , U ; x : T , y : U ) - > T { return x ; }
1 └┬─┘ └┬───────┘
2 │ └─ Run - Time Parameters
3 └─ Compile - Time Parameters
4
5 fn g ( T ; ) - > T { . . . } // Compile-Time Only (rare but allowed; note trailing `;`)
6 fn h ( x : i32 ) - > i32 { return x ; } // Run Time Only (no `;`)

Rules

  • Tokens before ; are compile-time parameters (type or const/value-level),
  • Type parameters: bare identifiers (ie., T , U ).
  • Const parameters: Name: Type form (ie., N: int ).
  • Tokens after ; are run-time parameters (the usual name: Type , with optional mut / spread, per language rules).
  • If there’s no ; , the entire list is treated as run-time parameters.
  • If the CT part is empty , omit ; (preferred style). If the RT part is empty and CT is present, keep a trailing ; .

Refinement Types: add a where -clause to any base type

A refinement type is a base type with a logical predicate.

Syntax : { id: Type where predicate }

Example
0 // A string that must be non-empty
1 type NonEmptyString = { s : string where std : : length ( s ) > 0 } ;
2
3 let good : NonEmptyString = "Aela" ; // ok
4 let bad : NonEmptyString = "" ; // compile-time error

Use refinements when you want value-aware validation while keeping the underlying representation.

Note

The compiler statically checks predicates where it can (literals, constant expressions, and facts learned from prior code/contracts). When a predicate can’t be decided statically, you’ll provide evidence (see “Proving facts to the compiler”).

Dependent Types: when types mention values

A dependent type is a type that depends on values .

A simple, practical pattern is to refine a function’s return by its inputs :

Example
0 fn add ( a : i32 , b : i32 ) - > { r : i32 where r = = a + b } {
1 return a + b ;
2 }

Here the return type depends on the run-time values a and b . The compiler enforces this contract at compile time wherever it can be proven, and narrows follow-up reasoning.

Another common pattern uses compile-time const parameters to index types:

Example
0 // Conceptual example; CT params appear before `;`
1 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) {
2 // implementation builds a vector whose length is M+N
3 }
  • T is a type parameter .
  • M and N are const parameters (compile-time integers).
  • The result type’s length computes to M + N at the type level .

Proving facts to the compiler

There are three common ways to convince the compiler of a refinement:

  1. Literals and constant expressions — obvious at compile time:
Example
0 let z : NonZeroint = 10 ; // trivially valid
  1. Local reasoning / guards — use a guard to establish a fact for a scope:
Example
0 fn safe_head ( xs : string [ ] ) - > { s : string where std : : length ( s ) > 0 } {
1 if ( std : : length ( xs ) > 0 ) {
2 return xs [ 0 ] ; // compiler knows length(xs) > 0 in this block
3 } else {
4 // handle empty case or return an option/result type
5 }
6 }
  1. Type-level contracts — express properties in the type and let the compiler check uses:
Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }
3 // Callers must provide evidence that `d != 0`.

Note

In more advanced code, system properties and invariants (see KW_REQUIRES , KW_ENSURES , KW_INVARIANT ) can encode broader guarantees, which the compiler uses as facts within the relevant scope.

End‑to‑End: making division-by-zero impossible

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1
2 fn safe_divide ( numer : i32 , denom : NonZeroint ) - > i32 {
3 return numer / denom ;
4 }
5
6 let a : i32 = 100 ;
7 let b : NonZeroint = 10 ; // proven at compile time
8 let ok = safe_divide ( a , b ) ; // compiles
9
10 let c : i32 = 0 ;
11 let err = safe_divide ( a , c ) ; // type error: expected NonZeroint, got i32

Parameter List: full spec (informal)

Example
0 // Declarations
1 fn name ( CT ; RT ) - > Ret { . . . }
2 fn name ( RT ) - > Ret { . . . } // no CT part → omit `;`
3 fn name ( CT ; ) - > Ret { . . . } // CT-only (allowed)
4
5 // CT parameters
6 typeparam : : = IDENTIFIER // ie., T, U
7 constparam : : = IDENTIFIER ':' Type // ie., N: int, K: U64
8 CT : : = typeparam | constparam ( ',' . . . )
9
10 // RT parameters
11 param : : = [ '...' ] [ 'mut' ] IDENTIFIER ':' Type
12 RT : : = param ( ',' . . . )

Validation

  • The CT side only accepts type/const parameters (no mut , no spreads).
  • The RT side accepts ordinary parameters.
  • A single top‑level ; within the parentheses splits CT from RT.
  • Style: omit an empty CT (; ...) — prefer just ( ... ) .

Choosing Refinement vs. Dependent

Use refinement types when:

  • You’re constraining a familiar base type ( i32 , string , a struct) with a predicate ( n != 0 , len(s) > 0 ).
  • You want to reuse existing APIs with stronger safety.

Use dependent types when:

  • The shape of your result depends on inputs (lengths, indices, protocol states).
  • You have natural compile-time parameters (ie., a block size N: int ).

They compose well: dependent function types can return refinement types, and vice versa.

Error messages (ergonomics)

  • CT/RT mixup : “Compile-time parameter list may only contain type/const parameters.”
  • Missing `;` : If the first parameter looks like a type/const param ( T or N: int ), suggest adding the ; .
  • Unproven refinement : Point to the predicate and suggest guards or helper constructors to provide evidence.

FAQ

Q: Do I have to write CT parameters at call sites? A: Typically no — they’re inferred from RT arguments and expected return types. You can guide inference via annotations.

Q: Can I have multiple `;`? A: No. There is at most one top‑level ; per parameter list.

Q: Are const parameters immutable? A: Yes. They are compile-time values; mutability doesn’t apply.

Q: What about async/pure/thread modifiers? A: These work unchanged and apply to the function as a whole; the ; split only affects parameter binding.

Worked examples (with ; )

1) Identity with a type parameter

Example
0 fn id ( T ; x : T ) - > T { return x ; }

2) Map over a vector (type‑level only)

Example
0 fn map ( T , U ; f : fn ( T ) - > U , xs : Vec ( T ) ) - > Vec ( U ) { . . . }

3) Concat with const lengths (conceptual)

Example
0 fn concat ( T , M : int , N : int ; a : Vec ( T , M ) , b : Vec ( T , N ) ) - > Vec ( T , M + N ) { . . . }

4) Safe division with a refinement type

Example
0 type NonZeroint = { n : i32 where n ! = 0 } ;
1 fn safe_divide ( n : i32 , d : NonZeroint ) - > i32 { return n / d ; }

Function Types

Why functions feel like they have “colors” (and how Aela fixes it)

Many languages split the world into synchronous and asynchronous functions. That split tends to spread—call sites, types, libraries—until everything is “[colored][1].” Aela acknowledges that programs have different execution disciplines (purity, async, thread-safety), then solves the composition pain with first-class types , clear call rules , and built‑in intrinsics so you can cross boundaries intentionally and safely.

At a glance:

  • Three disciplines (colors): pure , thread , async .
  • Simple call rules enforced by the checker.
  • Intrinsic adapters (escape hatches) to cross colors when needed.
  • Contracts ( requires / ensures ) and system blocks to guard risky crossings.

The three disciplines

pure

  • What it means: No observable side effects; referentially transparent.
  • When to use: Deterministic computation, validation, transforms.
  • Gotchas: Cannot call async or impure functions. May be combined with thread if the work is offloaded safely.

thread

  • What it means: Safe to run off the main executor (e.g., in a worker). No ambient event‑loop assumptions; data must be sendable or shared safely.
  • When to use: CPU‑bound work, blocking IO wrapped properly, parallelizable tasks.
  • Combines with: pure (i.e., pure thread fn ).

async

  • What it means: May suspend at await points, returns a future/awaitable.
  • When to use: IO‑bound workflows, coordination with timers, event‑driven code.
  • Note: async is not pure . It stands alone.

Call rules (the short version)

  • pure → may call only pure .
  • thread → may call thread or pure ; invoking a thread fn yields a Task handle.
  • uncolored (impure) → may call thread / pure directly and async via intrinsic.
  • async → may await other async functions or Task handles, and also call pure / thread without suspension.
  • await is legal inside both async fn and thread fn , because awaiting a Task join or future is permitted in either discipline.

Note

The checker gives precise diagnostics and suggests the right intrinsic when you cross a boundary.

Function types are first‑class

Aela’s type system includes function types with their discipline. These are expressed with refinement/dependent types instead of generics:

Example
0 pure fn ( x : u32 ) - > u32
1 thread fn ( bytes : Bytes ) - > Digest
2 async fn ( path : Path ) - > Result ( file : File , err : IoError )

Function parameters can carry refinements on their arguments or return types, e.g.:

Example
0 pure fn ( n : int where n > 0 ) - > Factorial ( n )

This makes intrinsics predictable and type‑safe, without requiring a generic system.

Crossing boundaries: standard intrinsics

To make crossing disciplines predictable and ergonomic, Aela ships intrinsics in the standard library:

Example
0 std : : concurrency : : to_threaded
1 std : : concurrency : : to_async
2 std : : concurrency : : to_blocking
3 std : : concurrency : : detach
4 std : : concurrency : : join

These are typed adapters that the checker understands.

Signatures & typing rules (no generics required)

Aela doesn’t need parametric generics here—these intrinsics are schematic over types and use refinement/dependent predicates to express constraints. We write them informally as “for any types X, Y…”, and the checker discharges the side conditions.

`to_threaded` *

Example
0 // for any types X, Y
1 // Preferred: lift pure/CPU-bound work onto a worker pool
2 fn to_threaded ( f : pure fn ( X ) - > Y ) - > thread fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )
4
5 // Also allowed (impure function), with the same sendability requirements
6 fn to_threaded ( f : fn ( X ) - > Y ) - > thread fn ( X ) - > Y
7 where Sendable ( X ) & & Sendable ( captures ( f ) )

Checks: argument and captured values must be sendable or shared/atomic . No reliance on an ambient event loop.

`to_async` *

Example
0 // for any types X, Y
1 fn to_async ( f : thread fn ( X ) - > Y ) - > async fn ( X ) - > Y
2
3 // Lifts a plain sync function too (discouraged unless necessary)
4 fn to_async ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
5 where Sendable ( X ) & & Sendable ( captures ( f ) )

Runtime model: schedules on the blocking/CPU pool; if the pool is saturated, the returned future suspends until capacity is available.

`to_blocking` * (the common case inside async )

Example
0 // for any types X, Y
1 // Inside async: run synchronous work without stalling the event loop
2 fn to_blocking ( f : fn ( X ) - > Y ) - > async fn ( X ) - > Y
3 where Sendable ( X ) & & Sendable ( captures ( f ) )

This is analogous to Rust Tokio’s `block_in_place`: it yields to the scheduler and executes on the blocking pool.

`block_on` * (drive async to completion from a worker thread)

Example
0 // for any type T
1 fn block_on ( fut : async fn ( ) - > T ) - > thread fn ( ) - > T

Policy: Forbidden on the event‑loop thread; prefer to_async / to_blocking when in async contexts.

`detach` / `join` *

Example
0 type Handle ( T )
1 fn detach ( fut : async fn ( ) - > T ) - > Handle ( T )
2 fn join ( h : Handle ( T ) ) - > async fn ( ) - > T

Diagnostics you’ll see

  • “Argument to `to_threaded` captures non‑sendable state Rc(T).”
  • “`to_blocking` called from non‑async context.”
  • “Pool saturated: `to_async` may suspend until space frees up.”

Examples

CPU work from async (don’t block the loop):

Example
0 async fn load_and_hash ( path : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( path ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 return digest ;
4 }

Submit a threaded task and await the handle:

Example
0 let t : Task ( Digest ) = to_threaded ( compute_hash ) ( bytes ) ;
1 let d : Digest = await t ; // structured join

Drive async to completion from a worker thread:

Example
0 thread fn load_cfg_sync ( ) - > Config {
1 std : : concurrency : : block_on ( load_cfg_async ) ( )
2 }

Lift pure compute to workers:

Example
0 pure fn sum ( xs : & [ i32 ] ) - > i32 { /* ... */ }
1 let task : Task ( i32 ) = std : : concurrency : : to_threaded ( sum ) ( nums ) ;
2 let result : i32 = await task ;

Use blocking work from async:

Example
0 async fn hash_file ( p : string ) - > Digest {
1 let data = await std : : concurrency : : to_blocking ( read_file ) ( p ) ;
2 let digest = await std : : concurrency : : to_blocking ( compute_hash ) ( data ) ;
3 digest
4 }

Use `to_async` to present sync/threaded as async:

Example
0 thread fn compress ( data : Bytes ) - > Bytes { /* CPU intensive */ }
1
2 async fn upload ( path : string ) - > Result ( Url , IoError ) {
3 let compressed = await std : : concurrency : : to_async ( compress ) ( await read_file ( path ) ) ;
4 return await send_to_server ( compressed ) ;
5 }

Detached background task:

Example
0 let h = std : : concurrency : : detach ( expensive_build ( ) ) ;
1 await std : : concurrency : : join ( h ) ;

Idioms and examples

  • Keep core transforms pure , wrap with intrinsics at the edges.
  • Use thread { ... } blocks for structured parallelism; all tasks inside must complete before exit.
  • Use std::select to race multiple async sources and cancel losers automatically.

FFI without foot‑guns

Declare foreign functions with explicit disciplines and refinements:

Example
0 ffi read_file = async fn ( path : string where exists ( path ) ) - > Result ( string , IoError )

Then wrap with system policies to guard where they are allowed:

parse_config } }" lang="aela" title="Example" id="8c9dff8f39f5b">
Example
0 system IO {
1 action ReadConfigAllowed ( ) - > Config
2 requires io_capability ( )
3 { await read_file ( " / etc / app . json" ) . ? | > parse_config }
4 }

Concurrency & mutability

  • Use shared / atomic types for cross‑thread data.
  • thread functions may operate on shared safely.
  • pure functions must not mutate shared state.

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.”
&Self T { return &self.0; } fn other(self: &Self as S, other: &Self as O) -> &O T { return &other.0; } } fn demo_methods() { let p1: Pair(int) = (1, 2); let p2: Pair(int) = (3, 4); let r1 = p1.first(); let r2 = p1.other(&p2); print(r1); print(r2); } // 4) Higher-order function: label flows through function type fn map_head(xs: &Vec(T) as A, f: Fn(&A T) -> U) -> &A U { return f(&xs[0]); } fn demo_hof() { let nums: Vec(int) = [1, 2, 3]; let head_ref = map_head(&nums, fn(x: &int) -> &int { return x; }); print(head_ref); } // 5) Multiple inputs require label: `as A` disambiguates the return fn pick(a: &T as A, b: &T) -> &A T { // body could choose either; label tells the checker the result is tied to `a` return a; } // 6) Optional: Outlives relation (advanced) fn choose_longer(a: &T as X, b: &T as Y) -> &X T where Y : X { return a; } // 7) Struct constructor with label reuse struct Window(T) { head: &A T, tail: &B T } fn mk_window(xs: &Vec(T) as A, ys: &Vec(T) as B) -> Window(T) { return Window { head: &xs[0], tail: &ys[0] }; } fn demo_window() { let xs: Vec(int) = [1,2,3]; let ys: Vec(int) = [4,5,6]; let w = mk_window(&xs, &ys); print(w.head); print(w.tail); } // 8) Diagnostics-friendly failure (commented): // fn bad_pick(a: &T, b: &T) -> &T { // if cond { return a; } else { return b; } // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`. // }" lang="aela" title="Example" id="afc4d82ee77ff">
Example
0 // 1) Disambiguate which input a returned reference is tied to
1 fn first_of_two ( a : & T as A , b : & T ) - > & A T {
2 return a ;
3 }
4
5 fn demo_first_of_two ( ) {
6 let x : int = 10 ;
7 let y : int = 20 ;
8 let rx = & x ;
9 let ry = & y ;
10
11 let r = first_of_two ( rx , ry ) ;
12 print ( r ) ;
13 }
14
15 // 2) Struct field referencing an argument via label
16 struct View ( T ) { data : & A T }
17
18 fn make_view ( x : & T as A ) - > View ( T ) {
19 return View { data : x } ;
20 }
21
22 fn demo_view ( ) {
23 let s : string = "hello" ;
24 let v = make_view ( & s ) ;
25 print ( v . data ) ;
26 }
27
28 // 3) Methods: implicit Self label + explicit labels to disambiguate
29 impl Pair ( T ) {
30 fn first ( self : & Self ) - > & Self T {
31 return & self . 0 ;
32 }
33
34 fn other ( self : & Self as S , other : & Self as O ) - > & O T {
35 return & other . 0 ;
36 }
37 }
38
39 fn demo_methods ( ) {
40 let p1 : Pair ( int ) = ( 1 , 2 ) ;
41 let p2 : Pair ( int ) = ( 3 , 4 ) ;
42
43 let r1 = p1 . first ( ) ;
44 let r2 = p1 . other ( & p2 ) ;
45 print ( r1 ) ;
46 print ( r2 ) ;
47 }
48
49 // 4) Higher-order function: label flows through function type
50 fn map_head ( xs : & Vec ( T ) as A , f : Fn ( & A T ) - > U ) - > & A U {
51 return f ( & xs [ 0 ] ) ;
52 }
53
54 fn demo_hof ( ) {
55 let nums : Vec ( int ) = [ 1 , 2 , 3 ] ;
56 let head_ref = map_head ( & nums , fn ( x : & int ) - > & int { return x ; } ) ;
57 print ( head_ref ) ;
58 }
59
60 // 5) Multiple inputs require label: `as A` disambiguates the return
61 fn pick ( a : & T as A , b : & T ) - > & A T {
62 // body could choose either; label tells the checker the result is tied to `a`
63 return a ;
64 }
65
66 // 6) Optional: Outlives relation (advanced)
67 fn choose_longer ( a : & T as X , b : & T as Y ) - > & X T where Y : X {
68 return a ;
69 }
70
71 // 7) Struct constructor with label reuse
72 struct Window ( T ) { head : & A T , tail : & B T }
73
74 fn mk_window ( xs : & Vec ( T ) as A , ys : & Vec ( T ) as B ) - > Window ( T ) {
75 return Window { head : & xs [ 0 ] , tail : & ys [ 0 ] } ;
76 }
77
78 fn demo_window ( ) {
79 let xs : Vec ( int ) = [ 1 , 2 , 3 ] ;
80 let ys : Vec ( int ) = [ 4 , 5 , 6 ] ;
81 let w = mk_window ( & xs , & ys ) ;
82 print ( w . head ) ;
83 print ( w . tail ) ;
84 }
85
86 // 8) Diagnostics-friendly failure (commented):
87 // fn bad_pick(a: &T, b: &T) -> &T {
88 // if cond { return a; } else { return b; }
89 // // Error: ambiguous return lifetime. Add `as A` to a (or b) and return `&A T`.
90 // }

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

Example
0 let s : string = "hi" ;
1 let r = & s ; // borrow starts
2 print ( r ) ; // last use of r
3 var t = s ; // OK allowed: r’s region ended at last use (lexically-free)

L1 — Loan Creation

Example
0 var x : int = 0 ;
1 let r = & x ; // L(x, shared)
2 let m = & mut x ; // Not OK conflict later under A1, but creation itself establishes L(x, unique)

L2 — Loan Propagation

Example
0 fn id_ref ( p : & int ) - > & int { p }
1 let x : int = 1 ;
2 let r1 = & x ; // L(x, shared)
3 let r2 = id_ref ( r1 ) ; // loan propagates to r2 until last use
4 print ( r2 ) ; // OK!

A1 — Unique Exclusivity

Example
0 var v : int = 0 ;
1 let m = & mut v ; // L(v, unique)
2 let r = & v ; // Not OK! A1: unique excludes any concurrent shared borrow

A2 — Shared Read‑Only

Example
0 var n : int = 0 ;
1 let a = & n ; // L(n, shared)
2 let b = & n ; // another shared loan
3 print ( * a + * b ) ; // OK! reads allowed
4 n = 5 ; // Not OK! A2: write while shared loans alive

I1 — Write Invalidates

Example
0 var s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ;
3 s . push ( " ! " ) ; // Not OK! I1: write to s while shared loan alive (if r not yet last‑used)

I2 — Move Invalidates

Example
0 var s : string = "a" ;
1 let r = & s ; // L(s, shared)
2 var t = s ; // Not OK! I2: move invalidates loans; r would dangle

I3 — Overlap/Fields

Example
0 struct P { x : int , y : int }
1 var p : P = P { x : 1 , y : 2 } ;
2 let mx = & mut p . x ; // L(p.x, unique)
3 let my = & mut p . y ; // OK, disjoint fields: allowed
4
5 var arr : [ int ; 3 ] = [ 0 , 1 , 2 ] ;
6 let a = & mut arr [ 0 ] ;
7 let b = & mut arr [ 1 ] ; // not OK, if indices distinct constants
8 let i = 0 ; let j = read_index ( ) ;
9 let c = & mut arr [ i ] ;
10 let d = & mut arr [ j ] ; // Not OK conservatively, may overlap unless proven disjoint (use split helpers)

U1 — Use Requires Alive

Example
0 let s : string = "hi" ;
1 let r = & s ; // L(s, shared)
2 print ( r ) ; // OK! use while alive
3 // after last use r ends; any further use would be not OK (dead borrow)

U2 — No After‑Free

Example
0 fn bad ( ) {
1 let s : string = "x" ;
2 let r = & s ;
3 drop ( s ) ; // base place dead
4 print ( r ) ; // Not OK: U2: use after base death
5 }

RB1 — Shared from Unique

Example
0 var v : int = 0 ;
1 let mu = & mut v ; // L(v, unique)
2
3 // Shared reborrow of the same place (auto-deref from &mut int to int)
4 let rs : & int = & mu ; // creates L(v, shared)
5
6 print ( rs ) ;
7
8 // Write through the unique borrow (auto-deref on assignment)
9 mu = 3 ; // must end shared loan before writing via `mu`

RB2 — Unique from Unique (optional v1)

Example
0 var v : int = 0 ;
1 let mu1 = & mut v ;
2 let mu2 = & mut mu1 ; // unique reborrow of v; allowed only if no overlapping use via mu1

E1 — No Escaping Borrows

Example
0 fn leak_ref ( ) - > & int {
1 let x : int = 1 ;
2 return & x ; // Not OK! Escapes to caller; Not OK, dies at function end
3 }
4
5 fn head ( s : & string ) - > & char {
6 return & s [ 0 ] ;
7 } // OK! Summary ties return to arg

M1 — Binding Mutability

Example
0 let x : int = 0 ;
1 let rx = & mut x ; // Not OK: M1: &mut requires mutable base
2 var y : int = 0 ;
3 let ry = & mut y ; // OK

M2 — No Shared Mutability Without Atomics

Example
0 shared var n : int = 0 ; // shared location
1 let r1 = & n ; let r2 = & n ; // shared borrows
2 n = n + 1 ; // Not OK concurrent write without atomic discipline
3 atomic var a : int = 0 ; // with atomic, writes are allowed by policy

T1 — Temporaries

Example
0 print ( & ( make_string ( ) ) ) ; // OK temporary lives through call; reference dies at last use
1 let r = & ( make_string ( ) ) ;
2 print ( r ) ; // Not OK if r would outlive the temporary’s last use

T2 — Branches/Loops/Match

Example
0 let s : string = "x" ;
1 let r = & s ;
2 if cond { print ( r ) ; } else { print ( r ) ; }
3 // r is used on both paths; live set at join = intersection ⇒ still alive until after the if
4 var t = s ; // not OK must occur after r’s last use on all paths

F1 — FFI Preconditions

Example
0 ffi puts : ( & char ) - > int = . . . ;
1 let s : string = "hi" ;
2 let r = & s [ 0 ] ;
3 puts ( r ) ; // OK if FFI summary: does not retain; Not OK if it may retain (escape)

F2 — FFI Postconditions

Example
0 ffi c_strchr : ( & char , int ) - > & char = . . . ; // trusted: result aliases input
1
2 fn first_a ( s : & string ) - > & char {
3 c_strchr ( & s [ 0 ] , 'a' ) // OK allowed only because summary ties result to arg region
4 }

RFT1 — Refinement Well‑Formedness

Example
0 let x : int = 5 ;
1 let y : { z : & int where initialized ( z ) } = { z : & x } ; // OK predicate references lifetime‑relevant property

RFT2 — Discharge at Use Sites

Example
0 fn show ( p : { z : & int where not_escaped ( z ) } ) - > void {
1 print ( p . z ) ; // OK! checker discharges `not_escaped` from current loan facts
2 }

inter‑Procedural Summary (Elision)

Example
0 fn get_first ( a : & [ int ] ) - > & int {
1 return & a [ 0 ] ;
2 }
3
4 // elaborated internally: for<ρ> fn(&ρ [int]) -> &ρ int
5 // caller instantiates ρ from its argument; return tied to same ρ

Structs with Reference Fields (Implicit Regions)

Example
0 struct Node ( T ) { data : & T } // elaborates to Node<ρ, T>
1
2 fn demo ( ) - > void {
3 let x : int = 1 ;
4 var n : Node ( int ) = Node { data : & x } ; // OK n: Node<ρx, int>
5 }
6
7 fn bad ( ) - > void {
8 var n : Node ( int ) ;
9
10 {
11 let x : int = 1 ;
12 n = Node { data : & x } ; // Not OK n outlives x ⇒ region check fails
13 }
14 }

Async Phase 1 — No Unique Loans Across Await

Example
0 async fn step ( mut v : & int ) - > void {
1 let m = v ; // borrow unique via parameter
2 await tick ( ) ; // Not OK, unique loan across await in phase 1
3 }

Closures — Capture Classification

void { move x }; // by‑value move ⇒ FnOnce" lang="aela" title="Example" id="e459ee693aab5">
Example
0 var n : int = 0 ;
1 let c1 = fn ( ) - > void { print ( & n ) ; } ; // shared borrow capture ⇒ Fn
2 let c2 = fn ( ) - > void { n = n + 1 ; } ; // unique borrow capture ⇒ FnMut
3 let x : string = "hi" ;
4 let c3 = fn ( ) - > void { move x } ; // by‑value move ⇒ FnOnce

RTOS Harmony

Linux Setup

You most likely need to edit your udev rules

Example
0 sudo curl - L - o / etc / udev / rules . d / 50 - cmsis - dap . rules \
1 https : / / raw . githubusercontent . com / pyocd / pyOCD / main / udev / 50 - cmsis - dap . rules

If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.

Example
0 lsusb | grep - iE 'arduino|cmsis|dap|renesas'
1 Bus 001 Device 005 : ID 2341 : 1002 Arduino SA . . .

Replace ID VVVV:PPPP

Example
0 # Arduino UNO R4 WiFi (CMSIS-DAP) — custom rule
1 SUBSYSTEM = = "usb" , ATTR { idVendor } = = "VVVV" , ATTR { idProduct } = = "PPPP" , MODE : = "0666"
2 SUBSYSTEM = = "hidraw" , ATTRS { idVendor } = = "VVVV" , ATTRS { idProduct } = = "PPPP" , MODE : = "0666"

Reload, re-enumerate

Example
0 sudo udevadm control - - reload - rules
1 sudo udevadm trigger

Unplug & Replug, press the reset button & then check:

Example
0 pyocd list

Zephyr

Install

Example
0 git cmake ninja python python - pip dtc wget

Install the Zephyr CLI tool

Example
0 pip install west

Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.

Example
0 sudo usermod - a - G dialout $USER

Create a project directory. Create a python environment in the project directory. Initialize it as a new zephyr project. Run the update command to get all the sub-repos.

Example
0 mkdir ~ / projects / z
1 python - m venv ~ / projects / z / . venv
2 west init ~ / projects / z
3 west update

Go back to your projects root and get the minimal SDK for cross compiling.

Example
0 cd ~ / projects
1 wget https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz

Calculate the SHA sum if you want

Example
0 wget - O - https : / / github . com / zephyrproject - rtos / sdk - ng / releases / download / v0 . 17 . 4 / sha256 . sum | shasum - - check - - ignore - missing

Extract the SDK and run the setup

Example
0 tar xvf zephyr - sdk - 0 . 17 . 4_linux - aarch64_minimal . tar . xz
1 cd ~ / projects / zephyr - sdk - 0 . 17 . 4
2 . / setup . sh

Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)

Example
0 # 1. Navigate to your project directory
1 cd ~ / projects / z
2
3 # 2. Activate the Python virtual environment for 'west'
4 source . / . venv / bin / activate
5
6 # 3. Manually export the SDK path to ensure it's found
7 export ZEPHYR_SDK_INSTALL_DIR = ~ / projects / zephyr - sdk - 0 . 17 . 4
8
9 # 4. Source the Zephyr environment to link everything together
10 source . / zephyr / zephyr - env . sh
11
12 # 5. Install a shit ton of dependencies
13 pip - 3 install - r zephyr / scripts / requirements . txt

Compile & Flash Test

Finally, build an Arduino image. I use Blinky here because its super simple and makes sense to start with as a sanity test.

Example
0 west build - p auto - b arduino_uno_r4 zephyr / samples / blinky
1 west flash

Integrating with Aela

Aela can output object files, so it's very simple to create a Zephyr project with Aela by just adding CMakeLists.txt and prj.conf files.

Example
0 myapp /
1 ├─ CMakeLists . txt
2 ├─ prj . conf
3 ├─ index . json
4 └─ index . ae

Example prj.conf

Example
0 # Prefer minimal libc over newlib (if you don’t need full POSIX/locale/etc.)
1 CONFIG_NEWLIB_LIBC = n
2 CONFIG_MINIMAL_LIBC = y
3 # If you must use newlib, at least disable float printf/scanf:
4 # CONFIG_NEWLIB_LIBC_FLOAT_PRINTF=n
5 # CONFIG_NEWLIB_LIBC_FLOAT_SCANF=n
6
7 # Logging/printk/console (turn off what you don't need)
8 CONFIG_PRINTK = n
9 CONFIG_LOG = n
10 # or, if you need logs:
11 # CONFIG_LOG=y
12 # CONFIG_LOG_MODE_MINIMAL=y
13 # CONFIG_LOG_DEFAULT_LEVEL=0
14
15 # Shell/console features often sneak in via defaults
16 CONFIG_CONSOLE = n
17 CONFIG_UART_CONSOLE = n
18 CONFIG_SHELL = n
19
20 # Link-time optimization can trim more
21 CONFIG_LTO = y
22 CONFIG_SIZE_OPTIMIZATIONS = y
23
24 # Assertions & debug
25 CONFIG_ASSERT = n
26 CONFIG_DEBUG = n
27 CONFIG_DEBUG_INFO = n # (debug symbols only affect .elf, not .bin size)
28
29 # Heap & stacks
30 CONFIG_HEAP_MEM_POOL_SIZE = 0 # if you don’t malloc at all
31 CONFIG_MAIN_STACK_SIZE = 1024 # tune as low as your app can tolerate

Example CMakeLists.txt

${AELA_OBJ}" VERBATIM ) add_library(aela_objects OBJECT ${AELA_OBJ}) set_source_files_properties(${AELA_OBJ} PROPERTIES GENERATED TRUE) # Link your Aela object (contains `main`) into the Zephyr app target_link_libraries(app PRIVATE aela_objects)" lang="cmake" title="Example" id="2051be01a6894">
Example
0 cmake_minimum_required ( VERSION 3 . 20 )
1 find_package ( Zephyr REQUIRED HINTS $ENV { ZEPHYR_BASE } )
2 project ( myapp )
3
4 # You can also pass these with: -DAEC=/path/aec -DAEC_FLAGS="..."
5 set ( AEC "aec" CACHE FILEPATH "Path to Aela compiler" )
6 set ( AEC_FLAGS "" CACHE STRING "Extra flags for Aela" )
7
8 # Optional: mirror Zephyr’s CPU/FPU flags so the .o matches the board ABI
9 # (We read what Zephyr passes to the C toolchain and reuse the ARM-related bits.)
10 get_property ( _Z_OPTS TARGET zephyr_interface PROPERTY INTERFACE_COMPILE_OPTIONS )
11 set ( _AE_ARM_OPTS "" )
12 foreach ( opt IN LISTS _Z_OPTS )
13 if ( opt MATCHES " ^ - m ( cpu | thumb | float - abi | fpu ) " ) ; list ( APPEND _AE_ARM_OPTS "$ { opt } " ) ; endif ( )
14 endforeach ( )
15
16 set ( AELA_SRC $ { CMAKE_CURRENT_SOURCE_DIR } / myprog . ae )
17 set ( AELA_OBJ $ { CMAKE_CURRENT_BINARY_DIR } / aela / myprog . obj . o )
18
19 add_custom_command (
20 OUTPUT $ { AELA_OBJ }
21 COMMAND $ { CMAKE_COMMAND } - E make_directory $ { CMAKE_CURRENT_BINARY_DIR } / aela
22 COMMAND $ { AEC } $ { AEC_FLAGS } $ { _AE_ARM_OPTS } - c $ { AELA_SRC } - o $ { AELA_OBJ }
23 DEPENDS $ { AELA_SRC }
24 COMMENT "Aela : $ { AELA_SRC } - > $ { AELA_OBJ } "
25 VERBATIM
26 )
27
28 add_library ( aela_objects OBJECT $ { AELA_OBJ } )
29 set_source_files_properties ( $ { AELA_OBJ } PROPERTIES GENERATED TRUE )
30
31 # Link your Aela object (contains `main`) into the Zephyr app
32 target_link_libraries ( app PRIVATE aela_objects )

Compiling

Example
0 west build - b arduino_uno_r4_wifi myapp - p \
1 - DCMAKE_EXPORT_COMPILE_COMMANDS = ON \
2 - DAEC = $ ( command - v aec )
3 west flash

Note

The _AE_ARM_OPTS trick copies exactly the -mcpu/-mfpu/-mfloat-abi/-mthumb flags Zephyr uses for this board, so your Aela object links ABI-cleanly without you guessing the right combo. (UNO R4 WiFi is a Cortex-M4; Zephyr’s board page confirms the arch.)

FreeRTOS

Discover Platform Build Flags

Lets assume an Arduino R4 here as an example.

We need to "spy" on the Arduino CLI to get the exact compiler and linker flags required for the R4 WiFi. The Aela build system will pass these directly to its underlyng C compiler. Arduino code files are called "sketches".

  1. Create a dummy sketch:
temp_sketch/temp_sketch.ino" lang="bash" title="Example" id="2274fcd531ebc">
Example
0 mkdir temp_sketch
1 echo " void setup ( ) { } void loop ( ) { } " > temp_sketch / temp_sketch . ino
  1. Run a verbose compile:
Example
0 arduino - cli compile - - fqbn arduino : renesas_uno : unor4wifi - - verbose temp_sketch
  1. Find and copy the linker command. Scroll through the output and find the longest command, which will start with something like .../arm-none-eabi-g++ ... . It will be a very long line that links all the object files and libraries together. Copy this entire command into a text editor. We're going to use its flags.

It will look something like this (shortened for clarity): .../arm-none-eabi-g++ -Os -Wl,--gc-sections -mcpu=cortex-m4 ... -L/path/to/build -Wl,--start-group -lArduinoCore -lrtos -lm -Wl,--end-group ...

We will now transfer the important parts of that command into your index.json .

Step 2: Project Structure

Organize your project with your source code inside a src directory.

Example
0 aela_freertos_blinky /
1 ├── index . json # The project manifest (our main focus)
2 └── src /
3 ├── main . ae # Your Aela application logic
4 └── shim . c # The C entry-point shim

Step 3: The index.json Manifest

This is the control center. We'll define a custom platform target called "arduino_r4" and place all the flags we discovered into the link section.

Create the file `index.json` (unless it was created via aec init ):

Example
0 {
1 "name" : "aela - freertos - blinky" ,
2 "version" : "0 . 1 . 0" ,
3 "entry" : "src / main . ae" ,
4
5 "sources" : {
6 "shared" : [
7 "src / shim . c"
8 ]
9 } ,
10
11 "link" : {
12 "platform" : {
13 "arduino_r4" : [
14 " - mcpu = cortex - m4" ,
15 " - mthumb" ,
16 " - mfloat - abi = hard" ,
17 " - mfpu = fpv4 - sp - d16" ,
18
19 " - Os" ,
20 " - Wl , - - gc - sections" ,
21 " - Wl , - - script = / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI / linker_script . ld" ,
22
23 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / cores / arduino" ,
24 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / variants / UNOR4WIFI" ,
25 " - I / home / user / . arduino15 / packages / arduino / hardware / renesas_uno / 1 . 1 . 0 / libraries / Arduino_FreeRTOS / src" ,
26
27 " - L / tmp / arduino / build - 123456789 . . . " ,
28
29 " - Wl , - - start - group" ,
30 " - lArduinoCore" ,
31 " - lrtos" ,
32 " - lm" ,
33 " - Wl , - - end - group"
34 ]
35 }
36 }
37 }

Note

You must replace the placeholder paths ( /home/user/... , /tmp/arduino/... ) with the full, absolute paths you copied from your verbose compiler output in Step 1.

Step 4: The Source Code

The source code is the same as before, but now it lives in the src/ directory.

src/main.ae

src/main.ae
0 // FFI Declarations for C functions
1 struct TaskHandle_t ;
2 type TaskFunction_t = fn ( & void ) - > void ;
3
4 ffi pinMode = fn ( u32 , u32 ) - > void ;
5 ffi digitalWrite = fn ( u32 , u32 ) - > void ;
6 ffi xTaskCreate = fn ( TaskFunction_t , string , u32 , & void , u32 , & TaskHandle_t ) - > i32 ;
7 ffi vTaskStartScheduler = fn ( ) - > void ;
8 ffi vTaskDelay = fn ( u32 ) - > void ;
9
10 // Constants
11 let LED_BUILTIN : u32 = 13 ;
12 let OUTPUT : u32 = 1 ;
13 let HIGH : u32 = 1 ;
14 let LOW : u32 = 0 ;
15
16 // The task that will blink the LED.
17 fn blinkTask ( params : & void ) - > void {
18 pinMode ( LED_BUILTIN , OUTPUT ) ;
19 while ( true ) {
20 digitalWrite ( LED_BUILTIN , HIGH ) ;
21 vTaskDelay ( 500 ) ;
22 digitalWrite ( LED_BUILTIN , LOW ) ;
23 vTaskDelay ( 500 ) ;
24 }
25 }
26
27 // Main entry point called from our C shim.
28 export fn aela_rtos ( ) - > void {
29 xTaskCreate ( blinkTask , "Blinker" , 128 , null , 1 , null ) ;
30 vTaskStartScheduler ( ) ;
31 }

src/shim.c

src/shim.c
0 #include
1
2 // Declare the external function defined in our Aela code.
3 extern void aela_rtos ( ) ;
4
5 // Standard Arduino entry point.
6 void setup ( ) {
7 aela_rtos ( ) ;
8 }
9
10 // loop() will never be reached, but must exist to link correctly.
11 void loop ( ) { }

Step 5: Build and Flash

You tell the Aela compiler what you're targeting, and it uses the manifest to set the correct build flags.

Build the project for the target triple:

Example
0 # This command tells Aela to cross-compile for the specified target.
1 # It will then find the "thumbv7em-none-eabihf" key in your index.json.
2 aec build - - platform = "arduino_r4" - - target thumbv7em - none - eabihf

Flash the output. The build process should still result in a .uf2 file in a build directory. You can then flash it with the Arduino CLI as before.

Example
0 arduino - cli upload - - fqbn arduino : renesas_uno : unor4wifi - - input - file build / aela - freertos - blinky . uf2

FAQ

Why is Aela 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.