Overview
Aela is a commercial-source language for embedded systems. It's a compiled, formally-verified and memory-safe language with a strong, static type system.
Programming Language Landscape
This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.
Langauge Goals
All language design decisions revolve around providing determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is avoided.
Aela also focuses on harmony with C and C++. Aela outputs object files that work with existing build systems like cmake. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like
write(2)
.
| Avoided Feature | Reasoning |
|---|---|
| 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. |
| 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
|
unsafe
blocks are an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of ceremoniously 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. |
| 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 | √ | √ | |||
| Native Formal Verification | √ | ||||
| Dependent & Refinement Types | √ | ||||
| Native Concurrency | √ | ||||
| Structured Concurrency | √ | √ | |||
| Automatic C/C++ safe binding | √ |
Get Started
Install the compiler
In a new directory, create a new project using the following command.
This will create some default files.
Edit the
index.json
file to name your project.
Next you’ll edit the main.ae file
To build your project, run the following command.
You’ll see a new directory with the compiled program that you can run.
Compiler Modes
aec build
This is your traditional, one-shot Ahead-Of-Time (AOT) compiler command.
| What | Compiles your entire project from source into a final, optimized executable binary. |
| How | It invokes the compiler engine, which runs all formal verifications, performs release-level optimizations (which can be slow), and links everything together. It's a non-interactive process designed for final output. |
| Why | Running in a Continuous Integration (CI) pipeline or when you're ready to create a production version of your application. |
aec run
This is a convenience command for development.
| What | Builds and immediately executes your program. |
| How | It's a simple wrapper that first performs an aec build (likely with fewer optimizations to be faster than a release build) and then runs the resulting binary. |
| Why | Quickly testing a command-line application's behavior without needing a full watch session. |
aec daemonize
This command exposes the engine's interactive mode directly to the command line.
| What | Starts the persistent, incremental engine to monitor files and provide continuous feedback in the terminal. |
| How | This will enable you to set watches on directories and enable incremental builds, and maintain stateful sessions. |
| Why | This is ideal or developers who prefer working in the terminal, or for anyone using AI tooling. |
aec package
This is a higher-level workflow and distribution tool.
| What | Bundles your project into a distributable format. |
| How | It would first run aec build --release to create the optimized executable. Then, it would gather other assets—like documentation, licenses, and configuration files—and package them into a compressed archive (like a .tar.gz) for publishing to a registry or for distribution. |
| Why | Publishing a new version of your library or application for others to use. |
Examples
Parallel Execution
This example shows a mutex integrity test proving that under real parallel execution, the runtime’s blocking Mutex ensures safe, deterministic updates to shared memory.
It demonstrates the following aspects...
- Mutual exclusion: Only one task updates balance at a time.
- Data race prevention: The final count matches expected value.
- Safe synchronization: Mutex correctly enforces memory ordering and release semantics.
- Task scheduling realism: The MPMC work-stealig scheduler interleaves threads genuinely—this isn’t cooperative or simulated concurrency.
Mutexes
Module and Package System
Aela’s module system is built around
packages
, each described by a manifest file named
index.json
.
- Every project is a package.
- Packages may depend on other packages.
- Packages can ship precompiled binaries plus source , so you get fast builds without losing debuggability.
- The same manifest also controls FFI build config and embedded resource budgets .
Package Manifest:
index.json
At the root of every Aela package, there is an
index.json
file. It tells the compiler everything it needs to know about the package.
Core Fields
- `name`
- Human- and tool-facing name of the package. Used in tooling and (optionally) in dependency resolution.
- `version`
-
Free-form version string (commonly
MAJOR.MINOR.PATCH). - `entry`
- Path to the top-level Aela file that should be compiled when this package is built.
- `output` (optional)
- Where to place the final executable or library. If omitted, the compiler chooses a default.
- `repo`
- An optional top-level block describes how the package’s source was obtained.
Repository Metadata
- `rev` is for reproducibility.
- `sources` is for multi-location source resolution.
- `hash` is for verifying fetched archives.
This is primarily for:
Dependencies
Dependencies are described as an
array of objects
, not a map. This matches the current
AelaPackageDependency
parsing code:
| Field | Type | Required | Description |
|---|---|---|---|
name
|
string | Yes |
Import name (
import ui from "ui";
).
|
url
|
string | Yes | Local path, git URL, remote archive, etc. |
sha256
|
string | Yes | Integrity hash of the dependency. Must match fetched content. |
- Ensures reproducible builds
- Prevents supply-chain tampering
- Allows local caching keyed by (url, sha256)
- Aligns with the repo.hash model at the package level
- Makes dependency resolution deterministic and safe
Why sha256 is now mandatory: The driver code:
-
Parses
dependenciesas a JSON array. -
Copies
name,url, andsha256intoAelaPackageDependency. -
Enforces a maximum of
MAX_PACKAGE_DEPS(currently 32).
Exporting and Importing Symbols
Aela defaults to
file-local
visibility. You must explicitly
export
to make symbols available to other modules.
Exports
Re-exports
You can “re-export” symbols from another file to build a neat public API:
Consumers can now just:
Imports
There are two main import styles: namespace imports and named imports .
Namespace Import
-
Brings the entire module under an alias (
ui,helpers). -
You access symbols with
alias::Symbol.
Named Imports
-
Windowis imported directly into the local scope. -
WindowOptionsis imported asOptions.
Source Layout Control:
include
/
exclude
The manifest can specify which files belong to the package with glob patterns .
In C, these map into:
-
include_patterns[]/num_include_patterns -
exclude_patterns[]/num_exclude_patterns
The parser:
-
Reads both
includeandexcludeas arrays of strings. - Uses an arena allocator to store the patterns.
-
Logs a warning if you exceed
MAX_PACKAGE_INCLUDE_PATTERNSorMAX_PACKAGE_EXCLUDE_PATTERNS.
If no
include
section is present, the compiler falls back to a default convention (implementation-dependent).
Native Build Configuration (FFI)
To talk to C, C++, Objective-C, etc., the manifest exposes three main sections:
- `sources` – native source files to compile
- `link` – link flags and libraries
- `compile` – compiler config and per-source-type flags
These are all parsed by the code you already have in
package.c
.
sources
In C (
AelaSourcesConfig
):
-
shared,darwin,ios,linux,android,windowsare all supported. -
Each is parsed as a dynamic string array via
parse_dynamic_string_array.
The build tool:
-
Compiles
sharedfor all platforms. - Compiles platform-specific lists only for that target.
link
In C (
AelaLinkConfig
):
-
platformis broken out into anAelaLinkPlatformConfigwith arrays fordarwin,ios,linux,windows,android. -
sharedis a cross-platform set of link flags.
The driver:
-
Merges
shared+ platform-specific flags for the active target. - Combines link flags from your dependencies as well.
compile
The
compile
block lets you:
- Specify a default compiler.
- Provide shared and platform-specific flags.
-
Override flags per
source type pattern
(e.g.
*.mmvs*.c).
This maps to:
-
AelaCompileConfig.compiler -
AelaCompileConfig.flags(shared,darwin, etc.) -
AelaCompileConfig.source_types[]:
-
pattern(e.g."*.mm") -
optional
compileroverride -
flags[]for that pattern
Embedded-First Targets and Budgets
Because Aela is embedded-systems-first , the manifest supports explicit targets with resource budgets .
This lets you say:
“On this board, keep flash under 64 KiB, RAM under 16 KiB, and average CPU under 60% over 10 ms windows.”
targets
Array
Top-level
targets
is an array of target definitions:
In C, each entry becomes an
AelaTargetConfig
:
The
budgets
shape:
Numeric vs Object Form
The parser is intentionally flexible:
You can write:
Or:
Both are accepted and stored as
flash_bytes_max
. Same idea for
ram_bytes
,
stack_bytes
,
heap_bytes
.
For CPU:
is parsed into:
-
cpu_max_pct = 60.0 -
cpu_window_ms = 10
How tooling can use this
The runtime/compiler can:
- After linking, read map / ELF / DWARF / LLD output to compute:
-
Flash usage:
.text + .rodata -
RAM usage:
.data + .bss
-
Compare against
*_bytes_max. -
Export CPU counters and compare to
cpu_max_pctovercpu_window_ms. - Surface all of that in the TUI (“Perf Details”) as:
- “Flash: 48 KiB / 64 KiB (75%)”
- “RAM: 8 KiB / 16 KiB (50%)”
- “CPU: 42% / 60% (10 ms window)”
Even before full enforcement, the manifest gives you a single, declarative place to specify what “too big” means for each device.
Putting It All Together
A more realistic
index.json
for an embedded app using native UI + budgets might look like:
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 failure 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! defails 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.
Just Fail
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
failure
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
failure. There are no other possibilities."
The
failure
and
fail
Keywords
-
`failure`
: A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from
structorenum, which represent data and recoverable errors.
-
`fail`
: A keyword that triggers a failure. It immediately stops the current function's execution and propagates the failure to the caller.
raiseis considered a terminal action.
The Standard
match
Statement
The
match
statement is how Aela handles the outcome of functions that may terminate with fails.
Semantic Rules
The safety and special behavior of fail handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:
If the expression being evaluated by a
matchstatement has a fail path in its signature (i.e., contains a|), then the compiler enforces a "Terminal Arm Rule" on any arm that matches afail-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:
-
fail{ ... }; -
std::abort(); -
std::halt(); -
std::reboot();
Note
purefn ketword must not introduce or handle fails; they cannot have a | in their return type and cannot raise.
Note
Failures must not cross FFI; board/FFI shims must convert fails to domain-appropriate codes or terminals.
Note
AP131outlines a proposal to havereturnbe the equivalent ofraise. Allowing both and specifying that they’re identical.
Note
AP132outlines a proposal to permit functions to be generic over an open set of fails (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;
Note
AP134outlines 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: Handling a Live Failure Event
If
reboot;
were omitted, the compiler would issue a clear error:
"Failure-handling arm must end with a terminal statement."
Example: Inspecting a Failure as Data
Example: Simple Conditional Failure
You do not need match to use failures. A very common pattern is a plain conditional that branches directly to fail when a contract is violated.
The signature
-> u8 | OutOfBounds
states up front that this function can either: return a
u8
, or terminate with an
OutOfBounds
failure. The if branch makes the logic explicit: If the index is invalid, we must fail with OutOfBounds. Otherwise, the function proceeds normally and returns a byte. There is no hidden panic and no surprise exit. Any caller can see, from the type alone, that
get_at
has a possible OutOfBounds failure.
Memory & Mutability
1. Default Allocation Semantics
- All values start on the stack by default.
- Stack allocations are:
- Fast
- Scoped
- Owned directly by the binding.
2. Heap Allocation
To allocate a value on the heap, use the
new
keyword with one of the following modifiers:
Syntax
All heap allocatations are reference counted.
Behavior 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. |
weak
|
Heap, weak handle to a shared object. | Does not keep the allocation alive; must be paired with at least one strong shared/shared 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). |
3. Mutability Semantics
Mutability is determined only by the binding keyword :
| Keyword | Meaning |
|---|---|
let
|
Immutable binding (read-only) |
var
|
Mutable binding (read-write) |
-
The
mutkeyword is not necesasry here. - Mutability is not encoded in types, structs, or fields.
-
letandvarare both lexically scoped.
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 { ... };
// Explicitly create a weak reference from a strong one. let weak_ref: weak &Foo = weak(strong_ref);
The if let Upgrade Pattern
Accessing the object behind a weak reference is inherently optional, as the object may have been deallocated. Aela enforces safe access through a conditional if let binding.
// Given a variable 'weak_ref' of type 'weak &Foo'
5. Copying Stack Values
- Heap allocation requires copying the stack value:
- This avoids moving ownership from the stack. Moves are not allowed .
5. Reference Types and Behavior
| Kind | Syntax | RC Type | Thread-Safe | Mutable |
|---|---|---|---|---|
| Stack value |
let x: T = ...
|
None | N/A | No |
| Heap reference |
let x: &T = new {...}
|
RC | No | No |
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 }.
Calling Conventions
How variables are allocated and passed to functions. The 'new' keyword is the explicit signal for heap allocation and reference counting.
Primitives & Simple Structs (Stack Allocated)
- Rule: Variables declared WITHOUT the 'new' keyword live on the stack.
- In Memory: The variable holds the data directly.
- Function Passing: Passed BY VALUE (a full copy is made).
- Lifetime: Automatic (destroyed when the variable goes out of scope).
- Reference Counted: No.
Boxed Values (Heap Allocated via 'new')
- Rule: Variables initialized WITH the 'new' keyword are allocated on the heap.
- In Memory: The variable holds a POINTER to a "box" on the heap.
- Function Passing: Passed BY REFERENCE (a copy of the pointer is made).
- Lifetime: Managed (Reference Counted).
- Reference Counted: Yes.
Closure Captures
- 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. Theenv_ptrpoints 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.
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
NonEmptyStringandNonZerointtell 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.
Rules
-
Tokens
before
;are compile-time parameters (type or const/value-level), -
Type parameters:
bare identifiers (ie.,
T,U). -
Const parameters:
Name: Typeform (ie.,N: int). -
Tokens
after
;are run-time parameters (the usualname: Type, with optionalmut/ 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 }
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 :
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:
-
Tis a type parameter . -
MandNare const parameters (compile-time integers). -
The result type’s length
computes
to
M + Nat the type level .
Proving facts to the compiler
There are three common ways to convince the compiler of a refinement:
- Literals and constant expressions — obvious at compile time:
- Local reasoning / guards — use a guard to establish a fact for a scope:
- Type-level contracts — express properties in the type and let the compiler check uses:
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
Parameter List: full spec (informal)
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 (
TorN: 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
2) Map over a vector (type‑level only)
3) Concat with const lengths (conceptual)
4) Safe division with a refinement type
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, task-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.
In addition to regular functions, there are
three disciplines
(colors):
pure
,
task
,
async
.
- Simple call rules enforced by the checker.
- Intrinsic adapters (escape hatches) to cross colors when needed.
-
Contracts
(
requires/ensures) andsystemblocks 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
asyncor impure functions. May be combined withtaskif the work is offloaded safely.
task
- 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 task fn).
async
-
What it means:
May suspend at
awaitpoints, returns a future/awaitable. - When to use: IO‑bound workflows, coordination with timers, event‑driven code.
-
Note:
asyncis notpure. It stands alone.
Call rules (the short version)
-
pure-> may call onlypure. -
task-> may calltaskorpure; invoking atask fnyields aTaskhandle. -
uncolored
(impure) → may call
task/puredirectly andasyncvia intrinsic. -
async-> mayawaitotherasyncfunctions orTaskhandles, and also callpure/taskwithout suspension. -
awaitis legal inside bothasync fnandtask fn, because awaiting aTaskjoin 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:
Function parameters can carry refinements on their arguments or return types, e.g.:
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:
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_tasked` *
Checks:
argument and captured values must be sendable or
shared/atomic
. No reliance on an ambient event loop.
`to_async` *
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
)
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 task)
Policy:
Forbidden on the event‑loop task; prefer
to_async
/
to_blocking
when in async contexts.
`detach` / `join` *
Diagnostics you’ll see
- “Argument to `to_tasked` 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):
Submit a tasked task and await the handle:
Drive async to completion from a worker task:
Lift pure compute to workers:
Use blocking work from async:
Use `to_async` to present sync/tasked as async:
Detached background task:
Idioms and examples
-
Keep core transforms
pure, wrap with intrinsics at the edges. -
Use
work { ... }blocks for structured parallelism; all tasks inside must complete before exit. -
Use
std::selectto race multiple async sources and cancel losers automatically.
Concurrency & mutability
-
Use
Atomictypes for cross‑task data. -
taskfunctions may operate onsharedsafely. -
purefunctions 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 thatpis borrowed, withkind ∈ {shared, unique}. -
Program Point
q: A location in the control-flow graph (CFG). -
Alive(L, q)
: Predicate meaning loan
Lis still valid at pointq(lexically-free semantics). - Operations :
-
reads(p, q): a read of placepatq. -
writes(p, q): a write to placepatq. -
moves(p, q): a move from placepatq. -
Aliases(x, p, q)
:
xholds a reference topatq(logical predicate, tracked via loan origins). -
Escape(r, q)
: Reference
rescapes its region atq(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[]) -> &i32elaborates tofor<ρ> 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 markerA.
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:
selfimplicitly labeledSelf, but can also be explicitly labeled:self: &Self as S. -
Diagnostics:
Role-based: “return value tied to param
a(label A) butadoes not live long enough.” Quick fixes: “Addas Ato param.”
Lifetimes in Data Structures
-
Reference fields implicitly carry region parameters.
struct Node { data: &T }elaborates tostruct Node<ρ, T> { data: &ρ T }. -
Construction instantiates
ρfrom the argument’s region. Error if struct outlives the referenced data.
Place Overlap (I3)
-
poverlapsp. -
poverlapsp.f. Distinct fields disjoint. -
arr[i]vsarr[j]: disjoint if indices are distinct compile-time constants; else conservative overlap. -
Library intrinsics like
split_at_mutprovide 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
awaitunless the origin outlives the entire future. Practically: locals cannot crossawait; only borrows from captured fields of the async task can. -
Phase 2:
Desugar
asyncto state machines and check across suspension points, enabling safe long-lived borrows.
Closures (FunctionExpression)
- Capture classification:
- Read-only → shared.
- Mutate → unique.
- Move → by-value.
- Trait mapping: shared → Fn; unique → FnMut; move → FnOnce.
- Escaping closures require captured regions to outlive closure region.
Refinement Types
-
Built-in predicates like
initialized(x),not_escaped(x)are decidable and do not require heavy SMT. - User-defined predicates and full logical refinement are measured to avoid compile-time blowups and underspecification.
Diagnostics Without Lifetime Names
-
Role-based regions: “returned reference must not outlive borrow of
arr.” - Highlight borrow creation, return site, and conflict.
- Optional symbolic labels (r1, r2) in error messages for clarity.
Rule-by-Rule Examples
Rule-by-Rule Examples (Concrete)
R0 — Implicit, Lexically-Free Regions
L1 — Loan Creation
L2 — Loan Propagation
A1 — Unique Exclusivity
A2 — Shared Read‑Only
I1 — Write Invalidates
I2 — Move Invalidates
I3 — Overlap/Fields
U1 — Use Requires Alive
U2 — No After‑Free
RB1 — Shared from Unique
RB2 — Unique from Unique (optional v1)
E1 — No Escaping Borrows
M1 — Binding Mutability
M2 — No Shared Mutability Without Atomics
T1 — Temporaries
T2 — Branches/Loops/Match
F1 — FFI Preconditions
F2 — FFI Postconditions
RFT1 — Refinement Well‑Formedness
RFT2 — Discharge at Use Sites
inter‑Procedural Summary (Elision)
Structs with Reference Fields (Implicit Regions)
Async Phase 1 — No Unique Loans Across Await
Closures — Capture Classification
C/C++ Harmony
Most languages' safty stops at the FFI boundary. But by automating the creation of safe FFI boundaries and embedding more of the C/C++ code's contracts directly into Aela's type system. Instead of just marking a boundary as unsafe and leaving the safety burden entirely on the developer, Aela can actively assist in verifying the C/C++ side of the interaction.
Automatically Generate "Diplomatic" Wrappers
Instead of manually writing write unsafe blocks and wrapper functions (This is tedious and error-prone). Aela can automate this.
Aela Compile can parse C/C++ header files (.h, .hpp) and automatically generatee the FFI bindings and a safe, idiomatic Aela wrapper. It's much more sophisticated than a simple binding generator.
Contract Inference
The tool can analyze C++ code for clues about contracts.
For instance, it can interpret a gsl::not_null
Resource Management
If a C function create_foo() returns a pointer that must be freed with
destroy_foo()
, the generator can automatically create a smart pointer or RAII object in Aela that calls
destroy_foo()
on scope exit. This eliminates a huge class of resource leak bugs.
Error Handling
It can translate C-style error codes e.g.,
return -1;
or
errno = EINVAL;
into Aela's native error-handling mechanism, like Result types or exceptions.
This moves the burden from the developer having to manually ensure safety to the too providing a verifiably safe starting point.
A Type System for C/C++ Interop
Aela's type system can understand C/C++'s quirks better. It encodes invariants about C pointers and memory directly into the types.
Sized Pointers
Instead of a raw pointer, Aela has types like Pointer(T, size_t N), which represent a pointer to a buffer of N elements. This allows the compiler to enforce bounds checking at the FFI boundary.
Nullability and Ownership
Explicitly differentiate between Pointer(T) (nullable) and Reference(T) (non-nullable). And types that encode ownership semantics like OwnedPointer(T) (must be freed) vs. BorrowedPointer(T) (must not be freed).
Tainted Data
Data coming from C/C++ is considered "tainted" by the type system. It needs to be explicitly validated (e.g., checking a string for valid UTF-8, ensuring a value is within an expected range) before it can be used in the safe context.
Integrate Static and Dynamic Analysis
Since Aela is written in C, it can integrate powerful C/C++ analysis tools directly into the build process.
Clang's Analyzers
Aela uses libraries from the Clang/LLVM project to perform static analysis on the C/C++ code. During compilation, it automatically invokes analyzers to check for things like null pointer dereferences, use-after-free, or buffer overflows in the C code being called, and flag a warning or error if a potential issue is found.
Boundary Sanitization
A "debug mode" for FFI that injects runtime checks at the boundary.
When your code calls a C function, it could automatically add canaries or check buffer boundaries. When C code calls back into Aela, it can validate incoming pointers and data. This is similar to running with AddressSanitizer (ASan), but it's focused specifically on the FFI-boundary risks.
By taking these steps, Aela doesn't just stop its safety guarantees at the boundary. It actively polices that boundary, making brownfield integration significantly safer and more robust than the manual, high-discipline approach required by other languages.
RTOS Harmony
Linux Setup
You most likely need to edit your udev rules
If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.
Replace ID VVVV:PPPP
Reload, re-enumerate
Unplug & Replug, press the reset button & then check:
Zephyr
Install
Install the Zephyr CLI tool
Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.
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.
Go back to your projects root and get the minimal SDK for cross compiling.
Calculate the SHA sum if you want
Extract the SDK and run the setup
Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)
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.
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
prj.conf
Example
CMakeLists.txt
Compiling
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".
- Create a dummy sketch:
- Run a verbose compile:
-
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.
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
):
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/shim.c
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:
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.
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. It's a compiled, formally-verified and memory-safe language with a strong, static type system.
Programming Language Landscape
This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.
Langauge Goals
All language design decisions revolve around providing determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is avoided.
Aela also focuses on harmony with C and C++. Aela outputs object files that work with existing build systems like cmake. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like
write(2)
.
| Avoided Feature | Reasoning |
|---|---|
| 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. |
| 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
|
unsafe
blocks are an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of ceremoniously 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. |
| 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 | √ | √ | |||
| Native Formal Verification | √ | ||||
| Dependent & Refinement Types | √ | ||||
| Native Concurrency | √ | ||||
| Structured Concurrency | √ | √ | |||
| Automatic C/C++ safe binding | √ |
Get Started
Install the compiler
In a new directory, create a new project using the following command.
This will create some default files.
Edit the
index.json
file to name your project.
Next you’ll edit the main.ae file
To build your project, run the following command.
You’ll see a new directory with the compiled program that you can run.
Compiler Modes
aec build
This is your traditional, one-shot Ahead-Of-Time (AOT) compiler command.
| What | Compiles your entire project from source into a final, optimized executable binary. |
| How | It invokes the compiler engine, which runs all formal verifications, performs release-level optimizations (which can be slow), and links everything together. It's a non-interactive process designed for final output. |
| Why | Running in a Continuous Integration (CI) pipeline or when you're ready to create a production version of your application. |
aec run
This is a convenience command for development.
| What | Builds and immediately executes your program. |
| How | It's a simple wrapper that first performs an aec build (likely with fewer optimizations to be faster than a release build) and then runs the resulting binary. |
| Why | Quickly testing a command-line application's behavior without needing a full watch session. |
aec daemonize
This command exposes the engine's interactive mode directly to the command line.
| What | Starts the persistent, incremental engine to monitor files and provide continuous feedback in the terminal. |
| How | This will enable you to set watches on directories and enable incremental builds, and maintain stateful sessions. |
| Why | This is ideal or developers who prefer working in the terminal, or for anyone using AI tooling. |
aec package
This is a higher-level workflow and distribution tool.
| What | Bundles your project into a distributable format. |
| How | It would first run aec build --release to create the optimized executable. Then, it would gather other assets—like documentation, licenses, and configuration files—and package them into a compressed archive (like a .tar.gz) for publishing to a registry or for distribution. |
| Why | Publishing a new version of your library or application for others to use. |
Examples
Parallel Execution
This example shows a mutex integrity test proving that under real parallel execution, the runtime’s blocking Mutex ensures safe, deterministic updates to shared memory.
It demonstrates the following aspects...
- Mutual exclusion: Only one task updates balance at a time.
- Data race prevention: The final count matches expected value.
- Safe synchronization: Mutex correctly enforces memory ordering and release semantics.
- Task scheduling realism: The MPMC work-stealig scheduler interleaves threads genuinely—this isn’t cooperative or simulated concurrency.
Mutexes
Module and Package System
Aela’s module system is built around
packages
, each described by a manifest file named
index.json
.
- Every project is a package.
- Packages may depend on other packages.
- Packages can ship precompiled binaries plus source , so you get fast builds without losing debuggability.
- The same manifest also controls FFI build config and embedded resource budgets .
Package Manifest:
index.json
At the root of every Aela package, there is an
index.json
file. It tells the compiler everything it needs to know about the package.
Core Fields
- `name`
- Human- and tool-facing name of the package. Used in tooling and (optionally) in dependency resolution.
- `version`
-
Free-form version string (commonly
MAJOR.MINOR.PATCH). - `entry`
- Path to the top-level Aela file that should be compiled when this package is built.
- `output` (optional)
- Where to place the final executable or library. If omitted, the compiler chooses a default.
- `repo`
- An optional top-level block describes how the package’s source was obtained.
Repository Metadata
- `rev` is for reproducibility.
- `sources` is for multi-location source resolution.
- `hash` is for verifying fetched archives.
This is primarily for:
Dependencies
Dependencies are described as an
array of objects
, not a map. This matches the current
AelaPackageDependency
parsing code:
| Field | Type | Required | Description |
|---|---|---|---|
name
|
string | Yes |
Import name (
import ui from "ui";
).
|
url
|
string | Yes | Local path, git URL, remote archive, etc. |
sha256
|
string | Yes | Integrity hash of the dependency. Must match fetched content. |
- Ensures reproducible builds
- Prevents supply-chain tampering
- Allows local caching keyed by (url, sha256)
- Aligns with the repo.hash model at the package level
- Makes dependency resolution deterministic and safe
Why sha256 is now mandatory: The driver code:
-
Parses
dependenciesas a JSON array. -
Copies
name,url, andsha256intoAelaPackageDependency. -
Enforces a maximum of
MAX_PACKAGE_DEPS(currently 32).
Exporting and Importing Symbols
Aela defaults to
file-local
visibility. You must explicitly
export
to make symbols available to other modules.
Exports
Re-exports
You can “re-export” symbols from another file to build a neat public API:
Consumers can now just:
Imports
There are two main import styles: namespace imports and named imports .
Namespace Import
-
Brings the entire module under an alias (
ui,helpers). -
You access symbols with
alias::Symbol.
Named Imports
-
Windowis imported directly into the local scope. -
WindowOptionsis imported asOptions.
Source Layout Control:
include
/
exclude
The manifest can specify which files belong to the package with glob patterns .
In C, these map into:
-
include_patterns[]/num_include_patterns -
exclude_patterns[]/num_exclude_patterns
The parser:
-
Reads both
includeandexcludeas arrays of strings. - Uses an arena allocator to store the patterns.
-
Logs a warning if you exceed
MAX_PACKAGE_INCLUDE_PATTERNSorMAX_PACKAGE_EXCLUDE_PATTERNS.
If no
include
section is present, the compiler falls back to a default convention (implementation-dependent).
Native Build Configuration (FFI)
To talk to C, C++, Objective-C, etc., the manifest exposes three main sections:
- `sources` – native source files to compile
- `link` – link flags and libraries
- `compile` – compiler config and per-source-type flags
These are all parsed by the code you already have in
package.c
.
sources
In C (
AelaSourcesConfig
):
-
shared,darwin,ios,linux,android,windowsare all supported. -
Each is parsed as a dynamic string array via
parse_dynamic_string_array.
The build tool:
-
Compiles
sharedfor all platforms. - Compiles platform-specific lists only for that target.
link
In C (
AelaLinkConfig
):
-
platformis broken out into anAelaLinkPlatformConfigwith arrays fordarwin,ios,linux,windows,android. -
sharedis a cross-platform set of link flags.
The driver:
-
Merges
shared+ platform-specific flags for the active target. - Combines link flags from your dependencies as well.
compile
The
compile
block lets you:
- Specify a default compiler.
- Provide shared and platform-specific flags.
-
Override flags per
source type pattern
(e.g.
*.mmvs*.c).
This maps to:
-
AelaCompileConfig.compiler -
AelaCompileConfig.flags(shared,darwin, etc.) -
AelaCompileConfig.source_types[]:
-
pattern(e.g."*.mm") -
optional
compileroverride -
flags[]for that pattern
Embedded-First Targets and Budgets
Because Aela is embedded-systems-first , the manifest supports explicit targets with resource budgets .
This lets you say:
“On this board, keep flash under 64 KiB, RAM under 16 KiB, and average CPU under 60% over 10 ms windows.”
targets
Array
Top-level
targets
is an array of target definitions:
In C, each entry becomes an
AelaTargetConfig
:
The
budgets
shape:
Numeric vs Object Form
The parser is intentionally flexible:
You can write:
Or:
Both are accepted and stored as
flash_bytes_max
. Same idea for
ram_bytes
,
stack_bytes
,
heap_bytes
.
For CPU:
is parsed into:
-
cpu_max_pct = 60.0 -
cpu_window_ms = 10
How tooling can use this
The runtime/compiler can:
- After linking, read map / ELF / DWARF / LLD output to compute:
-
Flash usage:
.text + .rodata -
RAM usage:
.data + .bss
-
Compare against
*_bytes_max. -
Export CPU counters and compare to
cpu_max_pctovercpu_window_ms. - Surface all of that in the TUI (“Perf Details”) as:
- “Flash: 48 KiB / 64 KiB (75%)”
- “RAM: 8 KiB / 16 KiB (50%)”
- “CPU: 42% / 60% (10 ms window)”
Even before full enforcement, the manifest gives you a single, declarative place to specify what “too big” means for each device.
Putting It All Together
A more realistic
index.json
for an embedded app using native UI + budgets might look like:
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 failure 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! defails 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.
Just Fail
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
failure
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
failure. There are no other possibilities."
The
failure
and
fail
Keywords
-
`failure`
: A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from
structorenum, which represent data and recoverable errors.
-
`fail`
: A keyword that triggers a failure. It immediately stops the current function's execution and propagates the failure to the caller.
raiseis considered a terminal action.
The Standard
match
Statement
The
match
statement is how Aela handles the outcome of functions that may terminate with fails.
Semantic Rules
The safety and special behavior of fail handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:
If the expression being evaluated by a
matchstatement has a fail path in its signature (i.e., contains a|), then the compiler enforces a "Terminal Arm Rule" on any arm that matches afail-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:
-
fail{ ... }; -
std::abort(); -
std::halt(); -
std::reboot();
Note
purefn ketword must not introduce or handle fails; they cannot have a | in their return type and cannot raise.
Note
Failures must not cross FFI; board/FFI shims must convert fails to domain-appropriate codes or terminals.
Note
AP131outlines a proposal to havereturnbe the equivalent ofraise. Allowing both and specifying that they’re identical.
Note
AP132outlines a proposal to permit functions to be generic over an open set of fails (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;
Note
AP134outlines 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: Handling a Live Failure Event
If
reboot;
were omitted, the compiler would issue a clear error:
"Failure-handling arm must end with a terminal statement."
Example: Inspecting a Failure as Data
Example: Simple Conditional Failure
You do not need match to use failures. A very common pattern is a plain conditional that branches directly to fail when a contract is violated.
The signature
-> u8 | OutOfBounds
states up front that this function can either: return a
u8
, or terminate with an
OutOfBounds
failure. The if branch makes the logic explicit: If the index is invalid, we must fail with OutOfBounds. Otherwise, the function proceeds normally and returns a byte. There is no hidden panic and no surprise exit. Any caller can see, from the type alone, that
get_at
has a possible OutOfBounds failure.
Memory & Mutability
1. Default Allocation Semantics
- All values start on the stack by default.
- Stack allocations are:
- Fast
- Scoped
- Owned directly by the binding.
2. Heap Allocation
To allocate a value on the heap, use the
new
keyword with one of the following modifiers:
Syntax
All heap allocatations are reference counted.
Behavior 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. |
weak
|
Heap, weak handle to a shared object. | Does not keep the allocation alive; must be paired with at least one strong shared/shared 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). |
3. Mutability Semantics
Mutability is determined only by the binding keyword :
| Keyword | Meaning |
|---|---|
let
|
Immutable binding (read-only) |
var
|
Mutable binding (read-write) |
-
The
mutkeyword is not necesasry here. - Mutability is not encoded in types, structs, or fields.
-
letandvarare both lexically scoped.
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 { ... };
// Explicitly create a weak reference from a strong one. let weak_ref: weak &Foo = weak(strong_ref);
The if let Upgrade Pattern
Accessing the object behind a weak reference is inherently optional, as the object may have been deallocated. Aela enforces safe access through a conditional if let binding.
// Given a variable 'weak_ref' of type 'weak &Foo'
5. Copying Stack Values
- Heap allocation requires copying the stack value:
- This avoids moving ownership from the stack. Moves are not allowed .
5. Reference Types and Behavior
| Kind | Syntax | RC Type | Thread-Safe | Mutable |
|---|---|---|---|---|
| Stack value |
let x: T = ...
|
None | N/A | No |
| Heap reference |
let x: &T = new {...}
|
RC | No | No |
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 }.
Calling Conventions
How variables are allocated and passed to functions. The 'new' keyword is the explicit signal for heap allocation and reference counting.
Primitives & Simple Structs (Stack Allocated)
- Rule: Variables declared WITHOUT the 'new' keyword live on the stack.
- In Memory: The variable holds the data directly.
- Function Passing: Passed BY VALUE (a full copy is made).
- Lifetime: Automatic (destroyed when the variable goes out of scope).
- Reference Counted: No.
Boxed Values (Heap Allocated via 'new')
- Rule: Variables initialized WITH the 'new' keyword are allocated on the heap.
- In Memory: The variable holds a POINTER to a "box" on the heap.
- Function Passing: Passed BY REFERENCE (a copy of the pointer is made).
- Lifetime: Managed (Reference Counted).
- Reference Counted: Yes.
Closure Captures
- 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. Theenv_ptrpoints 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.
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
NonEmptyStringandNonZerointtell 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.
Rules
-
Tokens
before
;are compile-time parameters (type or const/value-level), -
Type parameters:
bare identifiers (ie.,
T,U). -
Const parameters:
Name: Typeform (ie.,N: int). -
Tokens
after
;are run-time parameters (the usualname: Type, with optionalmut/ 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 }
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 :
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:
-
Tis a type parameter . -
MandNare const parameters (compile-time integers). -
The result type’s length
computes
to
M + Nat the type level .
Proving facts to the compiler
There are three common ways to convince the compiler of a refinement:
- Literals and constant expressions — obvious at compile time:
- Local reasoning / guards — use a guard to establish a fact for a scope:
- Type-level contracts — express properties in the type and let the compiler check uses:
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
Parameter List: full spec (informal)
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 (
TorN: 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
2) Map over a vector (type‑level only)
3) Concat with const lengths (conceptual)
4) Safe division with a refinement type
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, task-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.
In addition to regular functions, there are
three disciplines
(colors):
pure
,
task
,
async
.
- Simple call rules enforced by the checker.
- Intrinsic adapters (escape hatches) to cross colors when needed.
-
Contracts
(
requires/ensures) andsystemblocks 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
asyncor impure functions. May be combined withtaskif the work is offloaded safely.
task
- 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 task fn).
async
-
What it means:
May suspend at
awaitpoints, returns a future/awaitable. - When to use: IO‑bound workflows, coordination with timers, event‑driven code.
-
Note:
asyncis notpure. It stands alone.
Call rules (the short version)
-
pure-> may call onlypure. -
task-> may calltaskorpure; invoking atask fnyields aTaskhandle. -
uncolored
(impure) → may call
task/puredirectly andasyncvia intrinsic. -
async-> mayawaitotherasyncfunctions orTaskhandles, and also callpure/taskwithout suspension. -
awaitis legal inside bothasync fnandtask fn, because awaiting aTaskjoin 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:
Function parameters can carry refinements on their arguments or return types, e.g.:
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:
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_tasked` *
Checks:
argument and captured values must be sendable or
shared/atomic
. No reliance on an ambient event loop.
`to_async` *
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
)
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 task)
Policy:
Forbidden on the event‑loop task; prefer
to_async
/
to_blocking
when in async contexts.
`detach` / `join` *
Diagnostics you’ll see
- “Argument to `to_tasked` 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):
Submit a tasked task and await the handle:
Drive async to completion from a worker task:
Lift pure compute to workers:
Use blocking work from async:
Use `to_async` to present sync/tasked as async:
Detached background task:
Idioms and examples
-
Keep core transforms
pure, wrap with intrinsics at the edges. -
Use
work { ... }blocks for structured parallelism; all tasks inside must complete before exit. -
Use
std::selectto race multiple async sources and cancel losers automatically.
Concurrency & mutability
-
Use
Atomictypes for cross‑task data. -
taskfunctions may operate onsharedsafely. -
purefunctions 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 thatpis borrowed, withkind ∈ {shared, unique}. -
Program Point
q: A location in the control-flow graph (CFG). -
Alive(L, q)
: Predicate meaning loan
Lis still valid at pointq(lexically-free semantics). - Operations :
-
reads(p, q): a read of placepatq. -
writes(p, q): a write to placepatq. -
moves(p, q): a move from placepatq. -
Aliases(x, p, q)
:
xholds a reference topatq(logical predicate, tracked via loan origins). -
Escape(r, q)
: Reference
rescapes its region atq(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[]) -> &i32elaborates tofor<ρ> 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 markerA.
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:
selfimplicitly labeledSelf, but can also be explicitly labeled:self: &Self as S. -
Diagnostics:
Role-based: “return value tied to param
a(label A) butadoes not live long enough.” Quick fixes: “Addas Ato param.”
Lifetimes in Data Structures
-
Reference fields implicitly carry region parameters.
struct Node { data: &T }elaborates tostruct Node<ρ, T> { data: &ρ T }. -
Construction instantiates
ρfrom the argument’s region. Error if struct outlives the referenced data.
Place Overlap (I3)
-
poverlapsp. -
poverlapsp.f. Distinct fields disjoint. -
arr[i]vsarr[j]: disjoint if indices are distinct compile-time constants; else conservative overlap. -
Library intrinsics like
split_at_mutprovide 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
awaitunless the origin outlives the entire future. Practically: locals cannot crossawait; only borrows from captured fields of the async task can. -
Phase 2:
Desugar
asyncto state machines and check across suspension points, enabling safe long-lived borrows.
Closures (FunctionExpression)
- Capture classification:
- Read-only → shared.
- Mutate → unique.
- Move → by-value.
- Trait mapping: shared → Fn; unique → FnMut; move → FnOnce.
- Escaping closures require captured regions to outlive closure region.
Refinement Types
-
Built-in predicates like
initialized(x),not_escaped(x)are decidable and do not require heavy SMT. - User-defined predicates and full logical refinement are measured to avoid compile-time blowups and underspecification.
Diagnostics Without Lifetime Names
-
Role-based regions: “returned reference must not outlive borrow of
arr.” - Highlight borrow creation, return site, and conflict.
- Optional symbolic labels (r1, r2) in error messages for clarity.
Rule-by-Rule Examples
Rule-by-Rule Examples (Concrete)
R0 — Implicit, Lexically-Free Regions
L1 — Loan Creation
L2 — Loan Propagation
A1 — Unique Exclusivity
A2 — Shared Read‑Only
I1 — Write Invalidates
I2 — Move Invalidates
I3 — Overlap/Fields
U1 — Use Requires Alive
U2 — No After‑Free
RB1 — Shared from Unique
RB2 — Unique from Unique (optional v1)
E1 — No Escaping Borrows
M1 — Binding Mutability
M2 — No Shared Mutability Without Atomics
T1 — Temporaries
T2 — Branches/Loops/Match
F1 — FFI Preconditions
F2 — FFI Postconditions
RFT1 — Refinement Well‑Formedness
RFT2 — Discharge at Use Sites
inter‑Procedural Summary (Elision)
Structs with Reference Fields (Implicit Regions)
Async Phase 1 — No Unique Loans Across Await
Closures — Capture Classification
C/C++ Harmony
Most languages' safty stops at the FFI boundary. But by automating the creation of safe FFI boundaries and embedding more of the C/C++ code's contracts directly into Aela's type system. Instead of just marking a boundary as unsafe and leaving the safety burden entirely on the developer, Aela can actively assist in verifying the C/C++ side of the interaction.
Automatically Generate "Diplomatic" Wrappers
Instead of manually writing write unsafe blocks and wrapper functions (This is tedious and error-prone). Aela can automate this.
Aela Compile can parse C/C++ header files (.h, .hpp) and automatically generatee the FFI bindings and a safe, idiomatic Aela wrapper. It's much more sophisticated than a simple binding generator.
Contract Inference
The tool can analyze C++ code for clues about contracts.
For instance, it can interpret a gsl::not_null
Resource Management
If a C function create_foo() returns a pointer that must be freed with
destroy_foo()
, the generator can automatically create a smart pointer or RAII object in Aela that calls
destroy_foo()
on scope exit. This eliminates a huge class of resource leak bugs.
Error Handling
It can translate C-style error codes e.g.,
return -1;
or
errno = EINVAL;
into Aela's native error-handling mechanism, like Result types or exceptions.
This moves the burden from the developer having to manually ensure safety to the too providing a verifiably safe starting point.
A Type System for C/C++ Interop
Aela's type system can understand C/C++'s quirks better. It encodes invariants about C pointers and memory directly into the types.
Sized Pointers
Instead of a raw pointer, Aela has types like Pointer(T, size_t N), which represent a pointer to a buffer of N elements. This allows the compiler to enforce bounds checking at the FFI boundary.
Nullability and Ownership
Explicitly differentiate between Pointer(T) (nullable) and Reference(T) (non-nullable). And types that encode ownership semantics like OwnedPointer(T) (must be freed) vs. BorrowedPointer(T) (must not be freed).
Tainted Data
Data coming from C/C++ is considered "tainted" by the type system. It needs to be explicitly validated (e.g., checking a string for valid UTF-8, ensuring a value is within an expected range) before it can be used in the safe context.
Integrate Static and Dynamic Analysis
Since Aela is written in C, it can integrate powerful C/C++ analysis tools directly into the build process.
Clang's Analyzers
Aela uses libraries from the Clang/LLVM project to perform static analysis on the C/C++ code. During compilation, it automatically invokes analyzers to check for things like null pointer dereferences, use-after-free, or buffer overflows in the C code being called, and flag a warning or error if a potential issue is found.
Boundary Sanitization
A "debug mode" for FFI that injects runtime checks at the boundary.
When your code calls a C function, it could automatically add canaries or check buffer boundaries. When C code calls back into Aela, it can validate incoming pointers and data. This is similar to running with AddressSanitizer (ASan), but it's focused specifically on the FFI-boundary risks.
By taking these steps, Aela doesn't just stop its safety guarantees at the boundary. It actively polices that boundary, making brownfield integration significantly safer and more robust than the manual, high-discipline approach required by other languages.
RTOS Harmony
Linux Setup
You most likely need to edit your udev rules
If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.
Replace ID VVVV:PPPP
Reload, re-enumerate
Unplug & Replug, press the reset button & then check:
Zephyr
Install
Install the Zephyr CLI tool
Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.
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.
Go back to your projects root and get the minimal SDK for cross compiling.
Calculate the SHA sum if you want
Extract the SDK and run the setup
Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)
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.
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
prj.conf
Example
CMakeLists.txt
Compiling
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".
- Create a dummy sketch:
- Run a verbose compile:
-
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.
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
):
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/shim.c
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:
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.
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. It's a compiled, formally-verified and memory-safe language with a strong, static type system.
Programming Language Landscape
This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.
Langauge Goals
All language design decisions revolve around providing determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is avoided.
Aela also focuses on harmony with C and C++. Aela outputs object files that work with existing build systems like cmake. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like
write(2)
.
| Avoided Feature | Reasoning |
|---|---|
| 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. |
| 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
|
unsafe
blocks are an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of ceremoniously 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. |
| 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 | √ | √ | |||
| Native Formal Verification | √ | ||||
| Dependent & Refinement Types | √ | ||||
| Native Concurrency | √ | ||||
| Structured Concurrency | √ | √ | |||
| Automatic C/C++ safe binding | √ |
Get Started
Install the compiler
In a new directory, create a new project using the following command.
This will create some default files.
Edit the
index.json
file to name your project.
Next you’ll edit the main.ae file
To build your project, run the following command.
You’ll see a new directory with the compiled program that you can run.
Compiler Modes
aec build
This is your traditional, one-shot Ahead-Of-Time (AOT) compiler command.
| What | Compiles your entire project from source into a final, optimized executable binary. |
| How | It invokes the compiler engine, which runs all formal verifications, performs release-level optimizations (which can be slow), and links everything together. It's a non-interactive process designed for final output. |
| Why | Running in a Continuous Integration (CI) pipeline or when you're ready to create a production version of your application. |
aec run
This is a convenience command for development.
| What | Builds and immediately executes your program. |
| How | It's a simple wrapper that first performs an aec build (likely with fewer optimizations to be faster than a release build) and then runs the resulting binary. |
| Why | Quickly testing a command-line application's behavior without needing a full watch session. |
aec daemonize
This command exposes the engine's interactive mode directly to the command line.
| What | Starts the persistent, incremental engine to monitor files and provide continuous feedback in the terminal. |
| How | This will enable you to set watches on directories and enable incremental builds, and maintain stateful sessions. |
| Why | This is ideal or developers who prefer working in the terminal, or for anyone using AI tooling. |
aec package
This is a higher-level workflow and distribution tool.
| What | Bundles your project into a distributable format. |
| How | It would first run aec build --release to create the optimized executable. Then, it would gather other assets—like documentation, licenses, and configuration files—and package them into a compressed archive (like a .tar.gz) for publishing to a registry or for distribution. |
| Why | Publishing a new version of your library or application for others to use. |
Examples
Parallel Execution
This example shows a mutex integrity test proving that under real parallel execution, the runtime’s blocking Mutex ensures safe, deterministic updates to shared memory.
It demonstrates the following aspects...
- Mutual exclusion: Only one task updates balance at a time.
- Data race prevention: The final count matches expected value.
- Safe synchronization: Mutex correctly enforces memory ordering and release semantics.
- Task scheduling realism: The MPMC work-stealig scheduler interleaves threads genuinely—this isn’t cooperative or simulated concurrency.
Mutexes
Module and Package System
Aela’s module system is built around
packages
, each described by a manifest file named
index.json
.
- Every project is a package.
- Packages may depend on other packages.
- Packages can ship precompiled binaries plus source , so you get fast builds without losing debuggability.
- The same manifest also controls FFI build config and embedded resource budgets .
Package Manifest:
index.json
At the root of every Aela package, there is an
index.json
file. It tells the compiler everything it needs to know about the package.
Core Fields
- `name`
- Human- and tool-facing name of the package. Used in tooling and (optionally) in dependency resolution.
- `version`
-
Free-form version string (commonly
MAJOR.MINOR.PATCH). - `entry`
- Path to the top-level Aela file that should be compiled when this package is built.
- `output` (optional)
- Where to place the final executable or library. If omitted, the compiler chooses a default.
- `repo`
- An optional top-level block describes how the package’s source was obtained.
Repository Metadata
- `rev` is for reproducibility.
- `sources` is for multi-location source resolution.
- `hash` is for verifying fetched archives.
This is primarily for:
Dependencies
Dependencies are described as an
array of objects
, not a map. This matches the current
AelaPackageDependency
parsing code:
| Field | Type | Required | Description |
|---|---|---|---|
name
|
string | Yes |
Import name (
import ui from "ui";
).
|
url
|
string | Yes | Local path, git URL, remote archive, etc. |
sha256
|
string | Yes | Integrity hash of the dependency. Must match fetched content. |
- Ensures reproducible builds
- Prevents supply-chain tampering
- Allows local caching keyed by (url, sha256)
- Aligns with the repo.hash model at the package level
- Makes dependency resolution deterministic and safe
Why sha256 is now mandatory: The driver code:
-
Parses
dependenciesas a JSON array. -
Copies
name,url, andsha256intoAelaPackageDependency. -
Enforces a maximum of
MAX_PACKAGE_DEPS(currently 32).
Exporting and Importing Symbols
Aela defaults to
file-local
visibility. You must explicitly
export
to make symbols available to other modules.
Exports
Re-exports
You can “re-export” symbols from another file to build a neat public API:
Consumers can now just:
Imports
There are two main import styles: namespace imports and named imports .
Namespace Import
-
Brings the entire module under an alias (
ui,helpers). -
You access symbols with
alias::Symbol.
Named Imports
-
Windowis imported directly into the local scope. -
WindowOptionsis imported asOptions.
Source Layout Control:
include
/
exclude
The manifest can specify which files belong to the package with glob patterns .
In C, these map into:
-
include_patterns[]/num_include_patterns -
exclude_patterns[]/num_exclude_patterns
The parser:
-
Reads both
includeandexcludeas arrays of strings. - Uses an arena allocator to store the patterns.
-
Logs a warning if you exceed
MAX_PACKAGE_INCLUDE_PATTERNSorMAX_PACKAGE_EXCLUDE_PATTERNS.
If no
include
section is present, the compiler falls back to a default convention (implementation-dependent).
Native Build Configuration (FFI)
To talk to C, C++, Objective-C, etc., the manifest exposes three main sections:
- `sources` – native source files to compile
- `link` – link flags and libraries
- `compile` – compiler config and per-source-type flags
These are all parsed by the code you already have in
package.c
.
sources
In C (
AelaSourcesConfig
):
-
shared,darwin,ios,linux,android,windowsare all supported. -
Each is parsed as a dynamic string array via
parse_dynamic_string_array.
The build tool:
-
Compiles
sharedfor all platforms. - Compiles platform-specific lists only for that target.
link
In C (
AelaLinkConfig
):
-
platformis broken out into anAelaLinkPlatformConfigwith arrays fordarwin,ios,linux,windows,android. -
sharedis a cross-platform set of link flags.
The driver:
-
Merges
shared+ platform-specific flags for the active target. - Combines link flags from your dependencies as well.
compile
The
compile
block lets you:
- Specify a default compiler.
- Provide shared and platform-specific flags.
-
Override flags per
source type pattern
(e.g.
*.mmvs*.c).
This maps to:
-
AelaCompileConfig.compiler -
AelaCompileConfig.flags(shared,darwin, etc.) -
AelaCompileConfig.source_types[]:
-
pattern(e.g."*.mm") -
optional
compileroverride -
flags[]for that pattern
Embedded-First Targets and Budgets
Because Aela is embedded-systems-first , the manifest supports explicit targets with resource budgets .
This lets you say:
“On this board, keep flash under 64 KiB, RAM under 16 KiB, and average CPU under 60% over 10 ms windows.”
targets
Array
Top-level
targets
is an array of target definitions:
In C, each entry becomes an
AelaTargetConfig
:
The
budgets
shape:
Numeric vs Object Form
The parser is intentionally flexible:
You can write:
Or:
Both are accepted and stored as
flash_bytes_max
. Same idea for
ram_bytes
,
stack_bytes
,
heap_bytes
.
For CPU:
is parsed into:
-
cpu_max_pct = 60.0 -
cpu_window_ms = 10
How tooling can use this
The runtime/compiler can:
- After linking, read map / ELF / DWARF / LLD output to compute:
-
Flash usage:
.text + .rodata -
RAM usage:
.data + .bss
-
Compare against
*_bytes_max. -
Export CPU counters and compare to
cpu_max_pctovercpu_window_ms. - Surface all of that in the TUI (“Perf Details”) as:
- “Flash: 48 KiB / 64 KiB (75%)”
- “RAM: 8 KiB / 16 KiB (50%)”
- “CPU: 42% / 60% (10 ms window)”
Even before full enforcement, the manifest gives you a single, declarative place to specify what “too big” means for each device.
Putting It All Together
A more realistic
index.json
for an embedded app using native UI + budgets might look like:
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 failure 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! defails 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.
Just Fail
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
failure
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
failure. There are no other possibilities."
The
failure
and
fail
Keywords
-
`failure`
: A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from
structorenum, which represent data and recoverable errors.
-
`fail`
: A keyword that triggers a failure. It immediately stops the current function's execution and propagates the failure to the caller.
raiseis considered a terminal action.
The Standard
match
Statement
The
match
statement is how Aela handles the outcome of functions that may terminate with fails.
Semantic Rules
The safety and special behavior of fail handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:
If the expression being evaluated by a
matchstatement has a fail path in its signature (i.e., contains a|), then the compiler enforces a "Terminal Arm Rule" on any arm that matches afail-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:
-
fail{ ... }; -
std::abort(); -
std::halt(); -
std::reboot();
Note
purefn ketword must not introduce or handle fails; they cannot have a | in their return type and cannot raise.
Note
Failures must not cross FFI; board/FFI shims must convert fails to domain-appropriate codes or terminals.
Note
AP131outlines a proposal to havereturnbe the equivalent ofraise. Allowing both and specifying that they’re identical.
Note
AP132outlines a proposal to permit functions to be generic over an open set of fails (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;
Note
AP134outlines 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: Handling a Live Failure Event
If
reboot;
were omitted, the compiler would issue a clear error:
"Failure-handling arm must end with a terminal statement."
Example: Inspecting a Failure as Data
Example: Simple Conditional Failure
You do not need match to use failures. A very common pattern is a plain conditional that branches directly to fail when a contract is violated.
The signature
-> u8 | OutOfBounds
states up front that this function can either: return a
u8
, or terminate with an
OutOfBounds
failure. The if branch makes the logic explicit: If the index is invalid, we must fail with OutOfBounds. Otherwise, the function proceeds normally and returns a byte. There is no hidden panic and no surprise exit. Any caller can see, from the type alone, that
get_at
has a possible OutOfBounds failure.
Memory & Mutability
1. Default Allocation Semantics
- All values start on the stack by default.
- Stack allocations are:
- Fast
- Scoped
- Owned directly by the binding.
2. Heap Allocation
To allocate a value on the heap, use the
new
keyword with one of the following modifiers:
Syntax
All heap allocatations are reference counted.
Behavior 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. |
weak
|
Heap, weak handle to a shared object. | Does not keep the allocation alive; must be paired with at least one strong shared/shared 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). |
3. Mutability Semantics
Mutability is determined only by the binding keyword :
| Keyword | Meaning |
|---|---|
let
|
Immutable binding (read-only) |
var
|
Mutable binding (read-write) |
-
The
mutkeyword is not necesasry here. - Mutability is not encoded in types, structs, or fields.
-
letandvarare both lexically scoped.
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 { ... };
// Explicitly create a weak reference from a strong one. let weak_ref: weak &Foo = weak(strong_ref);
The if let Upgrade Pattern
Accessing the object behind a weak reference is inherently optional, as the object may have been deallocated. Aela enforces safe access through a conditional if let binding.
// Given a variable 'weak_ref' of type 'weak &Foo'
5. Copying Stack Values
- Heap allocation requires copying the stack value:
- This avoids moving ownership from the stack. Moves are not allowed .
5. Reference Types and Behavior
| Kind | Syntax | RC Type | Thread-Safe | Mutable |
|---|---|---|---|---|
| Stack value |
let x: T = ...
|
None | N/A | No |
| Heap reference |
let x: &T = new {...}
|
RC | No | No |
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 }.
Calling Conventions
How variables are allocated and passed to functions. The 'new' keyword is the explicit signal for heap allocation and reference counting.
Primitives & Simple Structs (Stack Allocated)
- Rule: Variables declared WITHOUT the 'new' keyword live on the stack.
- In Memory: The variable holds the data directly.
- Function Passing: Passed BY VALUE (a full copy is made).
- Lifetime: Automatic (destroyed when the variable goes out of scope).
- Reference Counted: No.
Boxed Values (Heap Allocated via 'new')
- Rule: Variables initialized WITH the 'new' keyword are allocated on the heap.
- In Memory: The variable holds a POINTER to a "box" on the heap.
- Function Passing: Passed BY REFERENCE (a copy of the pointer is made).
- Lifetime: Managed (Reference Counted).
- Reference Counted: Yes.
Closure Captures
- 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. Theenv_ptrpoints 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.
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
NonEmptyStringandNonZerointtell 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.
Rules
-
Tokens
before
;are compile-time parameters (type or const/value-level), -
Type parameters:
bare identifiers (ie.,
T,U). -
Const parameters:
Name: Typeform (ie.,N: int). -
Tokens
after
;are run-time parameters (the usualname: Type, with optionalmut/ 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 }
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 :
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:
-
Tis a type parameter . -
MandNare const parameters (compile-time integers). -
The result type’s length
computes
to
M + Nat the type level .
Proving facts to the compiler
There are three common ways to convince the compiler of a refinement:
- Literals and constant expressions — obvious at compile time:
- Local reasoning / guards — use a guard to establish a fact for a scope:
- Type-level contracts — express properties in the type and let the compiler check uses:
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
Parameter List: full spec (informal)
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 (
TorN: 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
2) Map over a vector (type‑level only)
3) Concat with const lengths (conceptual)
4) Safe division with a refinement type
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, task-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.
In addition to regular functions, there are
three disciplines
(colors):
pure
,
task
,
async
.
- Simple call rules enforced by the checker.
- Intrinsic adapters (escape hatches) to cross colors when needed.
-
Contracts
(
requires/ensures) andsystemblocks 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
asyncor impure functions. May be combined withtaskif the work is offloaded safely.
task
- 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 task fn).
async
-
What it means:
May suspend at
awaitpoints, returns a future/awaitable. - When to use: IO‑bound workflows, coordination with timers, event‑driven code.
-
Note:
asyncis notpure. It stands alone.
Call rules (the short version)
-
pure-> may call onlypure. -
task-> may calltaskorpure; invoking atask fnyields aTaskhandle. -
uncolored
(impure) → may call
task/puredirectly andasyncvia intrinsic. -
async-> mayawaitotherasyncfunctions orTaskhandles, and also callpure/taskwithout suspension. -
awaitis legal inside bothasync fnandtask fn, because awaiting aTaskjoin 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:
Function parameters can carry refinements on their arguments or return types, e.g.:
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:
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_tasked` *
Checks:
argument and captured values must be sendable or
shared/atomic
. No reliance on an ambient event loop.
`to_async` *
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
)
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 task)
Policy:
Forbidden on the event‑loop task; prefer
to_async
/
to_blocking
when in async contexts.
`detach` / `join` *
Diagnostics you’ll see
- “Argument to `to_tasked` 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):
Submit a tasked task and await the handle:
Drive async to completion from a worker task:
Lift pure compute to workers:
Use blocking work from async:
Use `to_async` to present sync/tasked as async:
Detached background task:
Idioms and examples
-
Keep core transforms
pure, wrap with intrinsics at the edges. -
Use
work { ... }blocks for structured parallelism; all tasks inside must complete before exit. -
Use
std::selectto race multiple async sources and cancel losers automatically.
Concurrency & mutability
-
Use
Atomictypes for cross‑task data. -
taskfunctions may operate onsharedsafely. -
purefunctions 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 thatpis borrowed, withkind ∈ {shared, unique}. -
Program Point
q: A location in the control-flow graph (CFG). -
Alive(L, q)
: Predicate meaning loan
Lis still valid at pointq(lexically-free semantics). - Operations :
-
reads(p, q): a read of placepatq. -
writes(p, q): a write to placepatq. -
moves(p, q): a move from placepatq. -
Aliases(x, p, q)
:
xholds a reference topatq(logical predicate, tracked via loan origins). -
Escape(r, q)
: Reference
rescapes its region atq(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[]) -> &i32elaborates tofor<ρ> 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 markerA.
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:
selfimplicitly labeledSelf, but can also be explicitly labeled:self: &Self as S. -
Diagnostics:
Role-based: “return value tied to param
a(label A) butadoes not live long enough.” Quick fixes: “Addas Ato param.”
Lifetimes in Data Structures
-
Reference fields implicitly carry region parameters.
struct Node { data: &T }elaborates tostruct Node<ρ, T> { data: &ρ T }. -
Construction instantiates
ρfrom the argument’s region. Error if struct outlives the referenced data.
Place Overlap (I3)
-
poverlapsp. -
poverlapsp.f. Distinct fields disjoint. -
arr[i]vsarr[j]: disjoint if indices are distinct compile-time constants; else conservative overlap. -
Library intrinsics like
split_at_mutprovide 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
awaitunless the origin outlives the entire future. Practically: locals cannot crossawait; only borrows from captured fields of the async task can. -
Phase 2:
Desugar
asyncto state machines and check across suspension points, enabling safe long-lived borrows.
Closures (FunctionExpression)
- Capture classification:
- Read-only → shared.
- Mutate → unique.
- Move → by-value.
- Trait mapping: shared → Fn; unique → FnMut; move → FnOnce.
- Escaping closures require captured regions to outlive closure region.
Refinement Types
-
Built-in predicates like
initialized(x),not_escaped(x)are decidable and do not require heavy SMT. - User-defined predicates and full logical refinement are measured to avoid compile-time blowups and underspecification.
Diagnostics Without Lifetime Names
-
Role-based regions: “returned reference must not outlive borrow of
arr.” - Highlight borrow creation, return site, and conflict.
- Optional symbolic labels (r1, r2) in error messages for clarity.
Rule-by-Rule Examples
Rule-by-Rule Examples (Concrete)
R0 — Implicit, Lexically-Free Regions
L1 — Loan Creation
L2 — Loan Propagation
A1 — Unique Exclusivity
A2 — Shared Read‑Only
I1 — Write Invalidates
I2 — Move Invalidates
I3 — Overlap/Fields
U1 — Use Requires Alive
U2 — No After‑Free
RB1 — Shared from Unique
RB2 — Unique from Unique (optional v1)
E1 — No Escaping Borrows
M1 — Binding Mutability
M2 — No Shared Mutability Without Atomics
T1 — Temporaries
T2 — Branches/Loops/Match
F1 — FFI Preconditions
F2 — FFI Postconditions
RFT1 — Refinement Well‑Formedness
RFT2 — Discharge at Use Sites
inter‑Procedural Summary (Elision)
Structs with Reference Fields (Implicit Regions)
Async Phase 1 — No Unique Loans Across Await
Closures — Capture Classification
C/C++ Harmony
Most languages' safty stops at the FFI boundary. But by automating the creation of safe FFI boundaries and embedding more of the C/C++ code's contracts directly into Aela's type system. Instead of just marking a boundary as unsafe and leaving the safety burden entirely on the developer, Aela can actively assist in verifying the C/C++ side of the interaction.
Automatically Generate "Diplomatic" Wrappers
Instead of manually writing write unsafe blocks and wrapper functions (This is tedious and error-prone). Aela can automate this.
Aela Compile can parse C/C++ header files (.h, .hpp) and automatically generatee the FFI bindings and a safe, idiomatic Aela wrapper. It's much more sophisticated than a simple binding generator.
Contract Inference
The tool can analyze C++ code for clues about contracts.
For instance, it can interpret a gsl::not_null
Resource Management
If a C function create_foo() returns a pointer that must be freed with
destroy_foo()
, the generator can automatically create a smart pointer or RAII object in Aela that calls
destroy_foo()
on scope exit. This eliminates a huge class of resource leak bugs.
Error Handling
It can translate C-style error codes e.g.,
return -1;
or
errno = EINVAL;
into Aela's native error-handling mechanism, like Result types or exceptions.
This moves the burden from the developer having to manually ensure safety to the too providing a verifiably safe starting point.
A Type System for C/C++ Interop
Aela's type system can understand C/C++'s quirks better. It encodes invariants about C pointers and memory directly into the types.
Sized Pointers
Instead of a raw pointer, Aela has types like Pointer(T, size_t N), which represent a pointer to a buffer of N elements. This allows the compiler to enforce bounds checking at the FFI boundary.
Nullability and Ownership
Explicitly differentiate between Pointer(T) (nullable) and Reference(T) (non-nullable). And types that encode ownership semantics like OwnedPointer(T) (must be freed) vs. BorrowedPointer(T) (must not be freed).
Tainted Data
Data coming from C/C++ is considered "tainted" by the type system. It needs to be explicitly validated (e.g., checking a string for valid UTF-8, ensuring a value is within an expected range) before it can be used in the safe context.
Integrate Static and Dynamic Analysis
Since Aela is written in C, it can integrate powerful C/C++ analysis tools directly into the build process.
Clang's Analyzers
Aela uses libraries from the Clang/LLVM project to perform static analysis on the C/C++ code. During compilation, it automatically invokes analyzers to check for things like null pointer dereferences, use-after-free, or buffer overflows in the C code being called, and flag a warning or error if a potential issue is found.
Boundary Sanitization
A "debug mode" for FFI that injects runtime checks at the boundary.
When your code calls a C function, it could automatically add canaries or check buffer boundaries. When C code calls back into Aela, it can validate incoming pointers and data. This is similar to running with AddressSanitizer (ASan), but it's focused specifically on the FFI-boundary risks.
By taking these steps, Aela doesn't just stop its safety guarantees at the boundary. It actively polices that boundary, making brownfield integration significantly safer and more robust than the manual, high-discipline approach required by other languages.
RTOS Harmony
Linux Setup
You most likely need to edit your udev rules
If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.
Replace ID VVVV:PPPP
Reload, re-enumerate
Unplug & Replug, press the reset button & then check:
Zephyr
Install
Install the Zephyr CLI tool
Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.
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.
Go back to your projects root and get the minimal SDK for cross compiling.
Calculate the SHA sum if you want
Extract the SDK and run the setup
Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)
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.
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
prj.conf
Example
CMakeLists.txt
Compiling
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".
- Create a dummy sketch:
- Run a verbose compile:
-
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.
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
):
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/shim.c
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:
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.
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. It's a compiled, formally-verified and memory-safe language with a strong, static type system.
Programming Language Landscape
This is where Aela fits In terms of Simplicity vs Complexity, and Familiarity vs Uniqueness.
Langauge Goals
All language design decisions revolve around providing determinism, safety, and performance for embedded systems. Anything that compromises these goals through ambiguity, hidden costs, or non-local behavior is avoided.
Aela also focuses on harmony with C and C++. Aela outputs object files that work with existing build systems like cmake. It offers automatic binding through header inclusion, packed and ordered structs, and inversion of control for system calls like
write(2)
.
| Avoided Feature | Reasoning |
|---|---|
| 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. |
| 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
|
unsafe
blocks are an escape hatch that undermines the entire memory safety guarantee of the language. Aela issues a handful of ceremoniously 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. |
| 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 | √ | √ | |||
| Native Formal Verification | √ | ||||
| Dependent & Refinement Types | √ | ||||
| Native Concurrency | √ | ||||
| Structured Concurrency | √ | √ | |||
| Automatic C/C++ safe binding | √ |
Get Started
Install the compiler
In a new directory, create a new project using the following command.
This will create some default files.
Edit the
index.json
file to name your project.
Next you’ll edit the main.ae file
To build your project, run the following command.
You’ll see a new directory with the compiled program that you can run.
Compiler Modes
aec build
This is your traditional, one-shot Ahead-Of-Time (AOT) compiler command.
| What | Compiles your entire project from source into a final, optimized executable binary. |
| How | It invokes the compiler engine, which runs all formal verifications, performs release-level optimizations (which can be slow), and links everything together. It's a non-interactive process designed for final output. |
| Why | Running in a Continuous Integration (CI) pipeline or when you're ready to create a production version of your application. |
aec run
This is a convenience command for development.
| What | Builds and immediately executes your program. |
| How | It's a simple wrapper that first performs an aec build (likely with fewer optimizations to be faster than a release build) and then runs the resulting binary. |
| Why | Quickly testing a command-line application's behavior without needing a full watch session. |
aec daemonize
This command exposes the engine's interactive mode directly to the command line.
| What | Starts the persistent, incremental engine to monitor files and provide continuous feedback in the terminal. |
| How | This will enable you to set watches on directories and enable incremental builds, and maintain stateful sessions. |
| Why | This is ideal or developers who prefer working in the terminal, or for anyone using AI tooling. |
aec package
This is a higher-level workflow and distribution tool.
| What | Bundles your project into a distributable format. |
| How | It would first run aec build --release to create the optimized executable. Then, it would gather other assets—like documentation, licenses, and configuration files—and package them into a compressed archive (like a .tar.gz) for publishing to a registry or for distribution. |
| Why | Publishing a new version of your library or application for others to use. |
Examples
Parallel Execution
This example shows a mutex integrity test proving that under real parallel execution, the runtime’s blocking Mutex ensures safe, deterministic updates to shared memory.
It demonstrates the following aspects...
- Mutual exclusion: Only one task updates balance at a time.
- Data race prevention: The final count matches expected value.
- Safe synchronization: Mutex correctly enforces memory ordering and release semantics.
- Task scheduling realism: The MPMC work-stealig scheduler interleaves threads genuinely—this isn’t cooperative or simulated concurrency.
Mutexes
Module and Package System
Aela’s module system is built around
packages
, each described by a manifest file named
index.json
.
- Every project is a package.
- Packages may depend on other packages.
- Packages can ship precompiled binaries plus source , so you get fast builds without losing debuggability.
- The same manifest also controls FFI build config and embedded resource budgets .
Package Manifest:
index.json
At the root of every Aela package, there is an
index.json
file. It tells the compiler everything it needs to know about the package.
Core Fields
- `name`
- Human- and tool-facing name of the package. Used in tooling and (optionally) in dependency resolution.
- `version`
-
Free-form version string (commonly
MAJOR.MINOR.PATCH). - `entry`
- Path to the top-level Aela file that should be compiled when this package is built.
- `output` (optional)
- Where to place the final executable or library. If omitted, the compiler chooses a default.
- `repo`
- An optional top-level block describes how the package’s source was obtained.
Repository Metadata
- `rev` is for reproducibility.
- `sources` is for multi-location source resolution.
- `hash` is for verifying fetched archives.
This is primarily for:
Dependencies
Dependencies are described as an
array of objects
, not a map. This matches the current
AelaPackageDependency
parsing code:
| Field | Type | Required | Description |
|---|---|---|---|
name
|
string | Yes |
Import name (
import ui from "ui";
).
|
url
|
string | Yes | Local path, git URL, remote archive, etc. |
sha256
|
string | Yes | Integrity hash of the dependency. Must match fetched content. |
- Ensures reproducible builds
- Prevents supply-chain tampering
- Allows local caching keyed by (url, sha256)
- Aligns with the repo.hash model at the package level
- Makes dependency resolution deterministic and safe
Why sha256 is now mandatory: The driver code:
-
Parses
dependenciesas a JSON array. -
Copies
name,url, andsha256intoAelaPackageDependency. -
Enforces a maximum of
MAX_PACKAGE_DEPS(currently 32).
Exporting and Importing Symbols
Aela defaults to
file-local
visibility. You must explicitly
export
to make symbols available to other modules.
Exports
Re-exports
You can “re-export” symbols from another file to build a neat public API:
Consumers can now just:
Imports
There are two main import styles: namespace imports and named imports .
Namespace Import
-
Brings the entire module under an alias (
ui,helpers). -
You access symbols with
alias::Symbol.
Named Imports
-
Windowis imported directly into the local scope. -
WindowOptionsis imported asOptions.
Source Layout Control:
include
/
exclude
The manifest can specify which files belong to the package with glob patterns .
In C, these map into:
-
include_patterns[]/num_include_patterns -
exclude_patterns[]/num_exclude_patterns
The parser:
-
Reads both
includeandexcludeas arrays of strings. - Uses an arena allocator to store the patterns.
-
Logs a warning if you exceed
MAX_PACKAGE_INCLUDE_PATTERNSorMAX_PACKAGE_EXCLUDE_PATTERNS.
If no
include
section is present, the compiler falls back to a default convention (implementation-dependent).
Native Build Configuration (FFI)
To talk to C, C++, Objective-C, etc., the manifest exposes three main sections:
- `sources` – native source files to compile
- `link` – link flags and libraries
- `compile` – compiler config and per-source-type flags
These are all parsed by the code you already have in
package.c
.
sources
In C (
AelaSourcesConfig
):
-
shared,darwin,ios,linux,android,windowsare all supported. -
Each is parsed as a dynamic string array via
parse_dynamic_string_array.
The build tool:
-
Compiles
sharedfor all platforms. - Compiles platform-specific lists only for that target.
link
In C (
AelaLinkConfig
):
-
platformis broken out into anAelaLinkPlatformConfigwith arrays fordarwin,ios,linux,windows,android. -
sharedis a cross-platform set of link flags.
The driver:
-
Merges
shared+ platform-specific flags for the active target. - Combines link flags from your dependencies as well.
compile
The
compile
block lets you:
- Specify a default compiler.
- Provide shared and platform-specific flags.
-
Override flags per
source type pattern
(e.g.
*.mmvs*.c).
This maps to:
-
AelaCompileConfig.compiler -
AelaCompileConfig.flags(shared,darwin, etc.) -
AelaCompileConfig.source_types[]:
-
pattern(e.g."*.mm") -
optional
compileroverride -
flags[]for that pattern
Embedded-First Targets and Budgets
Because Aela is embedded-systems-first , the manifest supports explicit targets with resource budgets .
This lets you say:
“On this board, keep flash under 64 KiB, RAM under 16 KiB, and average CPU under 60% over 10 ms windows.”
targets
Array
Top-level
targets
is an array of target definitions:
In C, each entry becomes an
AelaTargetConfig
:
The
budgets
shape:
Numeric vs Object Form
The parser is intentionally flexible:
You can write:
Or:
Both are accepted and stored as
flash_bytes_max
. Same idea for
ram_bytes
,
stack_bytes
,
heap_bytes
.
For CPU:
is parsed into:
-
cpu_max_pct = 60.0 -
cpu_window_ms = 10
How tooling can use this
The runtime/compiler can:
- After linking, read map / ELF / DWARF / LLD output to compute:
-
Flash usage:
.text + .rodata -
RAM usage:
.data + .bss
-
Compare against
*_bytes_max. -
Export CPU counters and compare to
cpu_max_pctovercpu_window_ms. - Surface all of that in the TUI (“Perf Details”) as:
- “Flash: 48 KiB / 64 KiB (75%)”
- “RAM: 8 KiB / 16 KiB (50%)”
- “CPU: 42% / 60% (10 ms window)”
Even before full enforcement, the manifest gives you a single, declarative place to specify what “too big” means for each device.
Putting It All Together
A more realistic
index.json
for an embedded app using native UI + budgets might look like:
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 failure 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! defails 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.
Just Fail
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
failure
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
failure. There are no other possibilities."
The
failure
and
fail
Keywords
-
`failure`
: A keyword used to declare a type that represents a logic bug or contract violation. This distinguishes it from
structorenum, which represent data and recoverable errors.
-
`fail`
: A keyword that triggers a failure. It immediately stops the current function's execution and propagates the failure to the caller.
raiseis considered a terminal action.
The Standard
match
Statement
The
match
statement is how Aela handles the outcome of functions that may terminate with fails.
Semantic Rules
The safety and special behavior of fail handling are not derived from the syntax, but from a single, powerful semantic rule in the compiler:
If the expression being evaluated by a
matchstatement has a fail path in its signature (i.e., contains a|), then the compiler enforces a "Terminal Arm Rule" on any arm that matches afail-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:
-
fail{ ... }; -
std::abort(); -
std::halt(); -
std::reboot();
Note
purefn ketword must not introduce or handle fails; they cannot have a | in their return type and cannot raise.
Note
Failures must not cross FFI; board/FFI shims must convert fails to domain-appropriate codes or terminals.
Note
AP131outlines a proposal to havereturnbe the equivalent ofraise. Allowing both and specifying that they’re identical.
Note
AP132outlines a proposal to permit functions to be generic over an open set of fails (variadic type param), so adapters don’t re-enumerate: ie: fn map(f: fn(T) -> U | E..., x: T) -> U | E...;
Note
AP134outlines 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: Handling a Live Failure Event
If
reboot;
were omitted, the compiler would issue a clear error:
"Failure-handling arm must end with a terminal statement."
Example: Inspecting a Failure as Data
Example: Simple Conditional Failure
You do not need match to use failures. A very common pattern is a plain conditional that branches directly to fail when a contract is violated.
The signature
-> u8 | OutOfBounds
states up front that this function can either: return a
u8
, or terminate with an
OutOfBounds
failure. The if branch makes the logic explicit: If the index is invalid, we must fail with OutOfBounds. Otherwise, the function proceeds normally and returns a byte. There is no hidden panic and no surprise exit. Any caller can see, from the type alone, that
get_at
has a possible OutOfBounds failure.
Memory & Mutability
1. Default Allocation Semantics
- All values start on the stack by default.
- Stack allocations are:
- Fast
- Scoped
- Owned directly by the binding.
2. Heap Allocation
To allocate a value on the heap, use the
new
keyword with one of the following modifiers:
Syntax
All heap allocatations are reference counted.
Behavior 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. |
weak
|
Heap, weak handle to a shared object. | Does not keep the allocation alive; must be paired with at least one strong shared/shared 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). |
3. Mutability Semantics
Mutability is determined only by the binding keyword :
| Keyword | Meaning |
|---|---|
let
|
Immutable binding (read-only) |
var
|
Mutable binding (read-write) |
-
The
mutkeyword is not necesasry here. - Mutability is not encoded in types, structs, or fields.
-
letandvarare both lexically scoped.
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 { ... };
// Explicitly create a weak reference from a strong one. let weak_ref: weak &Foo = weak(strong_ref);
The if let Upgrade Pattern
Accessing the object behind a weak reference is inherently optional, as the object may have been deallocated. Aela enforces safe access through a conditional if let binding.
// Given a variable 'weak_ref' of type 'weak &Foo'
5. Copying Stack Values
- Heap allocation requires copying the stack value:
- This avoids moving ownership from the stack. Moves are not allowed .
5. Reference Types and Behavior
| Kind | Syntax | RC Type | Thread-Safe | Mutable |
|---|---|---|---|---|
| Stack value |
let x: T = ...
|
None | N/A | No |
| Heap reference |
let x: &T = new {...}
|
RC | No | No |
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 }.
Calling Conventions
How variables are allocated and passed to functions. The 'new' keyword is the explicit signal for heap allocation and reference counting.
Primitives & Simple Structs (Stack Allocated)
- Rule: Variables declared WITHOUT the 'new' keyword live on the stack.
- In Memory: The variable holds the data directly.
- Function Passing: Passed BY VALUE (a full copy is made).
- Lifetime: Automatic (destroyed when the variable goes out of scope).
- Reference Counted: No.
Boxed Values (Heap Allocated via 'new')
- Rule: Variables initialized WITH the 'new' keyword are allocated on the heap.
- In Memory: The variable holds a POINTER to a "box" on the heap.
- Function Passing: Passed BY REFERENCE (a copy of the pointer is made).
- Lifetime: Managed (Reference Counted).
- Reference Counted: Yes.
Closure Captures
- 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. Theenv_ptrpoints 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.
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
NonEmptyStringandNonZerointtell 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.
Rules
-
Tokens
before
;are compile-time parameters (type or const/value-level), -
Type parameters:
bare identifiers (ie.,
T,U). -
Const parameters:
Name: Typeform (ie.,N: int). -
Tokens
after
;are run-time parameters (the usualname: Type, with optionalmut/ 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 }
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 :
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:
-
Tis a type parameter . -
MandNare const parameters (compile-time integers). -
The result type’s length
computes
to
M + Nat the type level .
Proving facts to the compiler
There are three common ways to convince the compiler of a refinement:
- Literals and constant expressions — obvious at compile time:
- Local reasoning / guards — use a guard to establish a fact for a scope:
- Type-level contracts — express properties in the type and let the compiler check uses:
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
Parameter List: full spec (informal)
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 (
TorN: 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
2) Map over a vector (type‑level only)
3) Concat with const lengths (conceptual)
4) Safe division with a refinement type
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, task-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.
In addition to regular functions, there are
three disciplines
(colors):
pure
,
task
,
async
.
- Simple call rules enforced by the checker.
- Intrinsic adapters (escape hatches) to cross colors when needed.
-
Contracts
(
requires/ensures) andsystemblocks 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
asyncor impure functions. May be combined withtaskif the work is offloaded safely.
task
- 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 task fn).
async
-
What it means:
May suspend at
awaitpoints, returns a future/awaitable. - When to use: IO‑bound workflows, coordination with timers, event‑driven code.
-
Note:
asyncis notpure. It stands alone.
Call rules (the short version)
-
pure-> may call onlypure. -
task-> may calltaskorpure; invoking atask fnyields aTaskhandle. -
uncolored
(impure) → may call
task/puredirectly andasyncvia intrinsic. -
async-> mayawaitotherasyncfunctions orTaskhandles, and also callpure/taskwithout suspension. -
awaitis legal inside bothasync fnandtask fn, because awaiting aTaskjoin 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:
Function parameters can carry refinements on their arguments or return types, e.g.:
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:
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_tasked` *
Checks:
argument and captured values must be sendable or
shared/atomic
. No reliance on an ambient event loop.
`to_async` *
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
)
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 task)
Policy:
Forbidden on the event‑loop task; prefer
to_async
/
to_blocking
when in async contexts.
`detach` / `join` *
Diagnostics you’ll see
- “Argument to `to_tasked` 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):
Submit a tasked task and await the handle:
Drive async to completion from a worker task:
Lift pure compute to workers:
Use blocking work from async:
Use `to_async` to present sync/tasked as async:
Detached background task:
Idioms and examples
-
Keep core transforms
pure, wrap with intrinsics at the edges. -
Use
work { ... }blocks for structured parallelism; all tasks inside must complete before exit. -
Use
std::selectto race multiple async sources and cancel losers automatically.
Concurrency & mutability
-
Use
Atomictypes for cross‑task data. -
taskfunctions may operate onsharedsafely. -
purefunctions 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 thatpis borrowed, withkind ∈ {shared, unique}. -
Program Point
q: A location in the control-flow graph (CFG). -
Alive(L, q)
: Predicate meaning loan
Lis still valid at pointq(lexically-free semantics). - Operations :
-
reads(p, q): a read of placepatq. -
writes(p, q): a write to placepatq. -
moves(p, q): a move from placepatq. -
Aliases(x, p, q)
:
xholds a reference topatq(logical predicate, tracked via loan origins). -
Escape(r, q)
: Reference
rescapes its region atq(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[]) -> &i32elaborates tofor<ρ> 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 markerA.
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:
selfimplicitly labeledSelf, but can also be explicitly labeled:self: &Self as S. -
Diagnostics:
Role-based: “return value tied to param
a(label A) butadoes not live long enough.” Quick fixes: “Addas Ato param.”
Lifetimes in Data Structures
-
Reference fields implicitly carry region parameters.
struct Node { data: &T }elaborates tostruct Node<ρ, T> { data: &ρ T }. -
Construction instantiates
ρfrom the argument’s region. Error if struct outlives the referenced data.
Place Overlap (I3)
-
poverlapsp. -
poverlapsp.f. Distinct fields disjoint. -
arr[i]vsarr[j]: disjoint if indices are distinct compile-time constants; else conservative overlap. -
Library intrinsics like
split_at_mutprovide 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
awaitunless the origin outlives the entire future. Practically: locals cannot crossawait; only borrows from captured fields of the async task can. -
Phase 2:
Desugar
asyncto state machines and check across suspension points, enabling safe long-lived borrows.
Closures (FunctionExpression)
- Capture classification:
- Read-only → shared.
- Mutate → unique.
- Move → by-value.
- Trait mapping: shared → Fn; unique → FnMut; move → FnOnce.
- Escaping closures require captured regions to outlive closure region.
Refinement Types
-
Built-in predicates like
initialized(x),not_escaped(x)are decidable and do not require heavy SMT. - User-defined predicates and full logical refinement are measured to avoid compile-time blowups and underspecification.
Diagnostics Without Lifetime Names
-
Role-based regions: “returned reference must not outlive borrow of
arr.” - Highlight borrow creation, return site, and conflict.
- Optional symbolic labels (r1, r2) in error messages for clarity.
Rule-by-Rule Examples
Rule-by-Rule Examples (Concrete)
R0 — Implicit, Lexically-Free Regions
L1 — Loan Creation
L2 — Loan Propagation
A1 — Unique Exclusivity
A2 — Shared Read‑Only
I1 — Write Invalidates
I2 — Move Invalidates
I3 — Overlap/Fields
U1 — Use Requires Alive
U2 — No After‑Free
RB1 — Shared from Unique
RB2 — Unique from Unique (optional v1)
E1 — No Escaping Borrows
M1 — Binding Mutability
M2 — No Shared Mutability Without Atomics
T1 — Temporaries
T2 — Branches/Loops/Match
F1 — FFI Preconditions
F2 — FFI Postconditions
RFT1 — Refinement Well‑Formedness
RFT2 — Discharge at Use Sites
inter‑Procedural Summary (Elision)
Structs with Reference Fields (Implicit Regions)
Async Phase 1 — No Unique Loans Across Await
Closures — Capture Classification
C/C++ Harmony
Most languages' safty stops at the FFI boundary. But by automating the creation of safe FFI boundaries and embedding more of the C/C++ code's contracts directly into Aela's type system. Instead of just marking a boundary as unsafe and leaving the safety burden entirely on the developer, Aela can actively assist in verifying the C/C++ side of the interaction.
Automatically Generate "Diplomatic" Wrappers
Instead of manually writing write unsafe blocks and wrapper functions (This is tedious and error-prone). Aela can automate this.
Aela Compile can parse C/C++ header files (.h, .hpp) and automatically generatee the FFI bindings and a safe, idiomatic Aela wrapper. It's much more sophisticated than a simple binding generator.
Contract Inference
The tool can analyze C++ code for clues about contracts.
For instance, it can interpret a gsl::not_null
Resource Management
If a C function create_foo() returns a pointer that must be freed with
destroy_foo()
, the generator can automatically create a smart pointer or RAII object in Aela that calls
destroy_foo()
on scope exit. This eliminates a huge class of resource leak bugs.
Error Handling
It can translate C-style error codes e.g.,
return -1;
or
errno = EINVAL;
into Aela's native error-handling mechanism, like Result types or exceptions.
This moves the burden from the developer having to manually ensure safety to the too providing a verifiably safe starting point.
A Type System for C/C++ Interop
Aela's type system can understand C/C++'s quirks better. It encodes invariants about C pointers and memory directly into the types.
Sized Pointers
Instead of a raw pointer, Aela has types like Pointer(T, size_t N), which represent a pointer to a buffer of N elements. This allows the compiler to enforce bounds checking at the FFI boundary.
Nullability and Ownership
Explicitly differentiate between Pointer(T) (nullable) and Reference(T) (non-nullable). And types that encode ownership semantics like OwnedPointer(T) (must be freed) vs. BorrowedPointer(T) (must not be freed).
Tainted Data
Data coming from C/C++ is considered "tainted" by the type system. It needs to be explicitly validated (e.g., checking a string for valid UTF-8, ensuring a value is within an expected range) before it can be used in the safe context.
Integrate Static and Dynamic Analysis
Since Aela is written in C, it can integrate powerful C/C++ analysis tools directly into the build process.
Clang's Analyzers
Aela uses libraries from the Clang/LLVM project to perform static analysis on the C/C++ code. During compilation, it automatically invokes analyzers to check for things like null pointer dereferences, use-after-free, or buffer overflows in the C code being called, and flag a warning or error if a potential issue is found.
Boundary Sanitization
A "debug mode" for FFI that injects runtime checks at the boundary.
When your code calls a C function, it could automatically add canaries or check buffer boundaries. When C code calls back into Aela, it can validate incoming pointers and data. This is similar to running with AddressSanitizer (ASan), but it's focused specifically on the FFI-boundary risks.
By taking these steps, Aela doesn't just stop its safety guarantees at the boundary. It actively polices that boundary, making brownfield integration significantly safer and more robust than the manual, high-discipline approach required by other languages.
RTOS Harmony
Linux Setup
You most likely need to edit your udev rules
If it doesn’t have your board’s rules in it, list your board to get the vendor and product id.
Replace ID VVVV:PPPP
Reload, re-enumerate
Unplug & Replug, press the reset button & then check:
Zephyr
Install
Install the Zephyr CLI tool
Allows you to flash your Arduino without needing to use sudo every time. It gives your user account permission to access the USB device.
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.
Go back to your projects root and get the minimal SDK for cross compiling.
Calculate the SHA sum if you want
Extract the SDK and run the setup
Initialize everything by entering your zephyr directory, activate the python env and set the environment (links the SDK you just got)
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.
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
prj.conf
Example
CMakeLists.txt
Compiling
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".
- Create a dummy sketch:
- Run a verbose compile:
-
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.
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
):
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/shim.c
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:
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.
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.