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.
Language Philosophy & Goals
Aela is ieneered for high-assurance embedded systems where failure is not an option. The language design prioritizes determinism , safety , and auditability above all else. Any feature that introduces ambiguity, hidden runtime costs, or non-local side effects has been strictly excluded.
Aela is designed to integrate seamlessly into existing embedded ecosystems. It maintains a stable ABI, produces object files compatible with standard build systems (like CMake), and provides native interoperability with C and C++. This includes automatic binding generation via header inclusion, precise memory layout control (packed/ordered structs), and Inversion of Control (IoC) patterns for system calls.
Excluded Features
The following features are common in general-purpose languages but are excluded from Aela to guarantee safety and predictability.
| Feature | Rationale |
|---|---|
| Generic `int` |
Ambiguity.
Platform-dependent integer sizes (16 vs 32 vs 64-bit) make portable formal verification mathematically impossible. Aela strictly enforces explicit, fixed-width types (ie,
i32
,
u64
) that behave identically on every architecture.
|
| Optional Braces | Syntactic Ambiguity. Optional braces lead to catastrophic control flow errors (ie, "Applieto fail"). Aela mandates braces for all control flow blocks, ensuring that execution scope matches visual indentation. |
| Pointer Arithmetic | Memory Safety. Direct pointer manipulation is the primary cause of buffer overflows. Aela replaces raw pointers with safe, bounds-checked slice operations. |
| Panics |
Control Flow Safety.
Panics create hidden, unrecoverable failure paths that bypass the type system. In Aela, all failure states must be represented in the function signature (ie,
Result(T)
), forcing caller handling.
|
| Exceptions | Determinism. Exceptions introduce non-local control flow and unpredictable stack unwinding, which complicates WCET (Worst-Case Execution Time) analysis. Error handling in Aela is strictly linear and explicit. |
| Implicit Heap |
Predictability.
Implicit allocation (ie,
malloc
hidden in
String
) causes fragmentation and latency spikes. Aela uses explicit
new(region)
, requiring all dynamic memory to be allocated within pre-defined, deterministic arenas.
|
| Global Mutable State | Concurrency Safety. Global variables introduce hidden dependencies ("spooky action at a distance"), making local reasoning and thread safety impossible. State must be passed explicitly or encapsulated in safe hardware abstractions. |
| Lifetime Annotations | ienomics. Explicit lifetimes add significant syntactic noise and cognitive load. Aela’s compiler infers ownership duration automatically, enforcing safety without burdening the programmer. |
| Macros |
Transparency.
Macros obscure code logic and impede static analysis. Aela replaces textual macros with
ast { ... }
blocks—strictly compile-time functions that generate type-checked ASTs, ensuring toolability and predictability.
|
| `unsafe` Blocks |
Integrity.
Broad
unsafe
blocks allow safety violations to hide anywhere. Aela instead provides a small set of "ceremoniously unsafe" intrinsic operations, making potential vulnerabilities easy to audit.
|
| Attributes | Explicitness. Attributes often inject hidden behavior or side effects. Aela avoids meta-programming tags in favor of explicit code patterns. |
| Advanced Traits | Readability. Complex trait hierarchies lead to cryptic errors and slow compilation. Aela prioritizes concrete types and simple interfaces over abstract expressive power. |
| Inline Assembly | Portability. Inline assembly breaks the optimizer and static analysis tools. Low-level architecture-specific routines must be implemented via the stable C ABI to maintain a clean verification boundary. |
| `null` Keyword |
Type Safety.
Null pointers are a billion-dollar mistake. The absence of a value must be explicitly typed (ie,
Option(T)
), forcing the programmer to handle the "empty" case.
|
| Operator Overloading |
Clarity.
Overloading hides the computational cost of operations (ie,
+
triggering a matrix allocation). Function calls must be explicit to ensure predictable performance.
|
| Implicit Conversions |
Precision.
Implicit casting hides data truncation and precision loss bugs. All type conversions must be explicit (ie,
val as u16
), forcing the programmer to acknowlie the change in data width.
|
| Unbounded Recursion | Stack Safety. Unbounded recursion prevents static stack usage analysis. Aela requires iteration via loops (which are bounded by variants) or strictly bounded recursion depth. |
| Variable Shadowing | Verification Soundness. Shadowing creates ambiguity in logical proofs regarding which "version" of a variable an invariant refers to. Aela mandates unique names for all variables within a scope. |
| Function Overloading |
Resolution Determinism.
Overloading creates ambiguity in call resolution. Aela requires unique function names (ie,
func_u8
vs
func_i32
), ensuring the call site explicitly matches the definition.
|
| Float Equality (`==`) |
Numerical Correctness.
Exact floating-point comparison is widely considered incorrect due to IEEE 754 representation errors. Aela enforces "fuzzy" comparison using explicit epsilon checks (ie,
abs(a - b) < 0.001
).
|
Included Features
These features provide the modern tooling and safety guarantees expected of a next-generation system language.
| Feature | Description |
|---|---|
| Compile-Time Memory Safety | Zero-overhead memory protection derived from region analysis and strict ownership rules, guaranteeing access safety without a garbage collector. |
| Automatic Reference Counting | Deterministic resource management where owned objects are reference-counted automatically, ensuring cleanup without manual intervention. |
| Automatic RAII |
Compiler-injected
drop
functions ensure that resources (memory, file handles, locks) are released deterministically when they go out of scope.
|
| Native Formal Verification |
Verification is a first-class citizen. Invariants (
#requires
,
#ensures
) are part of the language syntax, allowing the compiler to prove correctness without external specification files.
|
| Dependent Types | A pragmatic subset of dependent types (value-indexed types) allows the compiler to reason about the shape and size of data structures at compile time, eliminating an entire class of runtime bounds-checking errors. |
| Native Structured Concurrency | Concurrency is scoped and hierarchical. Child tasks cannot outlive their parent scopes, preventing "detached thread" leaks and ensuring rigorous cleanup of concurrent resources. |
| Automatic C/C++ Binding | Seamless interop via direct header import. The compiler parses C/C++ headers and automatically generates type-safe Aela bindings, eliminating the need for manual FFI wrappers. |
Open Source Version
An open source version of the core of the language is roadmapped for December 2026
Excluded Features
| Resource Analysis | WCET & Stack Calc | Stripped | Calculating Worst-Case Execution Time and Max Stack Usage is strictly a regulatory requirement for certification (DO-178C), not needed for general coding. |
|---|---|---|---|
| Traceability | Req Linking (DOORS) | Stripped | Linking code lines to specific requirements (ie, #req("1.4")) is valuable only to teams using heavy ALM tools like DOORS/Jama. |
| Hardware | Certified BSPs | Stripped | Support for niche safety chips (Infineon Aurix, TI Hercules) is expensive to maintain. OSS targets Linux/Generic MCU/WASM. |
| Library | Certified Std Lib | Stripped | The OSS library works, but the Enterprise library comes with a "Qualification Kit" (TCL) and legal warranty for safety claims. |
| Migration | C-to-Aela Lifter | Stripped | Tools that automatically translate C headers/source to Aela are high-value enterprise migration utilities, not daily developer tools. |
| Security | Global Taint Analysis | Stripped | Tracking "untrusted data" flows across the entire project is a specific cybersecurity compliance need (ISO 21434). |
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.
- `test`
-
The Test behavior when running
aec test. - `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: i32) -> 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: i32) -> 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 compiler enforces linear semantics on failure types. If a function signature contains a | (failure path), the caller cannot ignore the result.
| Validity | Code | Reasoning | |
|---|---|---|---|
| Valid |
let x = get_at(0)
;
|
Valid, but x is now a union that must be unpacked. | |
| Valid |
return get_at(0);
|
Valid if the caller also returns | OutOfBounds. |
NOTE
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
i32
"). 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: i32). -
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: i32).
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: i32), 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
Testing
The language provides a built-in, zero-overhead testing facility designed for systems programming. It prioritizes process isolation and developer control over magic.
Overview
Tests in the language are defined by the
#test
attribute. When compiling for production, all functions, imports, and variables marked with
#test
are stripped from the binary, ensuring zero runtime overhead.
When running
aec test
, the compiler builds your test files as separate executables and runs them in parallel.
Writing a Basic Test
To create a test, mark a function with
#test
. By convention, tests accept a reference to a
Tap
(Test Anything Protocol) harness, though this is customizable.
The
#test
notation can precede any expression or function declaration. And you can put a test in any file.
The Test Entry Point
Unlike managed languages that hide the test runner, you own the entry point . This gives you complete control over initialization, threading models, and exit codes.
Every test file must contain a
main
function marked with
#test
that returns an
i32
.
Warning: Be careful to return
0or1. Do not returnt.faileddirectly. POSIX exit codes wrap around at 256, so returning256(failures) results in exit code0(Success).
Test Configuration (
index.json
)
Configure the test runner in your package manifest. You can define which files are treated as test suites. Organize your files however you want.
- `files` : A list of glob patterns. Each matching file is compiled into its own isolated process.
-
`quiet`
: If
true, successful tests (TAPok) are suppressed, and only failures (not ok) are printed.
Conditional Imports
Apply
#test
to import statements when importing mocking libraries or heavy test dependencies that should never end up in your production binary.
Bring Your Own Framework (BYOF)
Because you control
main
, you are not forced to use the default
Tap
harness. You can implement custom reporting logic or interface with hardware.
If you are testing bare-metal hardware where
stdout
is not available, define what
ae_stdout_write
is, or you'll get a compile time error.
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
Aela provides a stable ABI (Please review abi.h or
aec help abi
).
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.
Language Philosophy & Goals
Aela is ieneered for high-assurance embedded systems where failure is not an option. The language design prioritizes determinism , safety , and auditability above all else. Any feature that introduces ambiguity, hidden runtime costs, or non-local side effects has been strictly excluded.
Aela is designed to integrate seamlessly into existing embedded ecosystems. It maintains a stable ABI, produces object files compatible with standard build systems (like CMake), and provides native interoperability with C and C++. This includes automatic binding generation via header inclusion, precise memory layout control (packed/ordered structs), and Inversion of Control (IoC) patterns for system calls.
Excluded Features
The following features are common in general-purpose languages but are excluded from Aela to guarantee safety and predictability.
| Feature | Rationale |
|---|---|
| Generic `int` |
Ambiguity.
Platform-dependent integer sizes (16 vs 32 vs 64-bit) make portable formal verification mathematically impossible. Aela strictly enforces explicit, fixed-width types (ie,
i32
,
u64
) that behave identically on every architecture.
|
| Optional Braces | Syntactic Ambiguity. Optional braces lead to catastrophic control flow errors (ie, "Applieto fail"). Aela mandates braces for all control flow blocks, ensuring that execution scope matches visual indentation. |
| Pointer Arithmetic | Memory Safety. Direct pointer manipulation is the primary cause of buffer overflows. Aela replaces raw pointers with safe, bounds-checked slice operations. |
| Panics |
Control Flow Safety.
Panics create hidden, unrecoverable failure paths that bypass the type system. In Aela, all failure states must be represented in the function signature (ie,
Result(T)
), forcing caller handling.
|
| Exceptions | Determinism. Exceptions introduce non-local control flow and unpredictable stack unwinding, which complicates WCET (Worst-Case Execution Time) analysis. Error handling in Aela is strictly linear and explicit. |
| Implicit Heap |
Predictability.
Implicit allocation (ie,
malloc
hidden in
String
) causes fragmentation and latency spikes. Aela uses explicit
new(region)
, requiring all dynamic memory to be allocated within pre-defined, deterministic arenas.
|
| Global Mutable State | Concurrency Safety. Global variables introduce hidden dependencies ("spooky action at a distance"), making local reasoning and thread safety impossible. State must be passed explicitly or encapsulated in safe hardware abstractions. |
| Lifetime Annotations | ienomics. Explicit lifetimes add significant syntactic noise and cognitive load. Aela’s compiler infers ownership duration automatically, enforcing safety without burdening the programmer. |
| Macros |
Transparency.
Macros obscure code logic and impede static analysis. Aela replaces textual macros with
ast { ... }
blocks—strictly compile-time functions that generate type-checked ASTs, ensuring toolability and predictability.
|
| `unsafe` Blocks |
Integrity.
Broad
unsafe
blocks allow safety violations to hide anywhere. Aela instead provides a small set of "ceremoniously unsafe" intrinsic operations, making potential vulnerabilities easy to audit.
|
| Attributes | Explicitness. Attributes often inject hidden behavior or side effects. Aela avoids meta-programming tags in favor of explicit code patterns. |
| Advanced Traits | Readability. Complex trait hierarchies lead to cryptic errors and slow compilation. Aela prioritizes concrete types and simple interfaces over abstract expressive power. |
| Inline Assembly | Portability. Inline assembly breaks the optimizer and static analysis tools. Low-level architecture-specific routines must be implemented via the stable C ABI to maintain a clean verification boundary. |
| `null` Keyword |
Type Safety.
Null pointers are a billion-dollar mistake. The absence of a value must be explicitly typed (ie,
Option(T)
), forcing the programmer to handle the "empty" case.
|
| Operator Overloading |
Clarity.
Overloading hides the computational cost of operations (ie,
+
triggering a matrix allocation). Function calls must be explicit to ensure predictable performance.
|
| Implicit Conversions |
Precision.
Implicit casting hides data truncation and precision loss bugs. All type conversions must be explicit (ie,
val as u16
), forcing the programmer to acknowlie the change in data width.
|
| Unbounded Recursion | Stack Safety. Unbounded recursion prevents static stack usage analysis. Aela requires iteration via loops (which are bounded by variants) or strictly bounded recursion depth. |
| Variable Shadowing | Verification Soundness. Shadowing creates ambiguity in logical proofs regarding which "version" of a variable an invariant refers to. Aela mandates unique names for all variables within a scope. |
| Function Overloading |
Resolution Determinism.
Overloading creates ambiguity in call resolution. Aela requires unique function names (ie,
func_u8
vs
func_i32
), ensuring the call site explicitly matches the definition.
|
| Float Equality (`==`) |
Numerical Correctness.
Exact floating-point comparison is widely considered incorrect due to IEEE 754 representation errors. Aela enforces "fuzzy" comparison using explicit epsilon checks (ie,
abs(a - b) < 0.001
).
|
Included Features
These features provide the modern tooling and safety guarantees expected of a next-generation system language.
| Feature | Description |
|---|---|
| Compile-Time Memory Safety | Zero-overhead memory protection derived from region analysis and strict ownership rules, guaranteeing access safety without a garbage collector. |
| Automatic Reference Counting | Deterministic resource management where owned objects are reference-counted automatically, ensuring cleanup without manual intervention. |
| Automatic RAII |
Compiler-injected
drop
functions ensure that resources (memory, file handles, locks) are released deterministically when they go out of scope.
|
| Native Formal Verification |
Verification is a first-class citizen. Invariants (
#requires
,
#ensures
) are part of the language syntax, allowing the compiler to prove correctness without external specification files.
|
| Dependent Types | A pragmatic subset of dependent types (value-indexed types) allows the compiler to reason about the shape and size of data structures at compile time, eliminating an entire class of runtime bounds-checking errors. |
| Native Structured Concurrency | Concurrency is scoped and hierarchical. Child tasks cannot outlive their parent scopes, preventing "detached thread" leaks and ensuring rigorous cleanup of concurrent resources. |
| Automatic C/C++ Binding | Seamless interop via direct header import. The compiler parses C/C++ headers and automatically generates type-safe Aela bindings, eliminating the need for manual FFI wrappers. |
Open Source Version
An open source version of the core of the language is roadmapped for December 2026
Excluded Features
| Resource Analysis | WCET & Stack Calc | Stripped | Calculating Worst-Case Execution Time and Max Stack Usage is strictly a regulatory requirement for certification (DO-178C), not needed for general coding. |
|---|---|---|---|
| Traceability | Req Linking (DOORS) | Stripped | Linking code lines to specific requirements (ie, #req("1.4")) is valuable only to teams using heavy ALM tools like DOORS/Jama. |
| Hardware | Certified BSPs | Stripped | Support for niche safety chips (Infineon Aurix, TI Hercules) is expensive to maintain. OSS targets Linux/Generic MCU/WASM. |
| Library | Certified Std Lib | Stripped | The OSS library works, but the Enterprise library comes with a "Qualification Kit" (TCL) and legal warranty for safety claims. |
| Migration | C-to-Aela Lifter | Stripped | Tools that automatically translate C headers/source to Aela are high-value enterprise migration utilities, not daily developer tools. |
| Security | Global Taint Analysis | Stripped | Tracking "untrusted data" flows across the entire project is a specific cybersecurity compliance need (ISO 21434). |
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.
- `test`
-
The Test behavior when running
aec test. - `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: i32) -> 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: i32) -> 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 compiler enforces linear semantics on failure types. If a function signature contains a | (failure path), the caller cannot ignore the result.
| Validity | Code | Reasoning | |
|---|---|---|---|
| Valid |
let x = get_at(0)
;
|
Valid, but x is now a union that must be unpacked. | |
| Valid |
return get_at(0);
|
Valid if the caller also returns | OutOfBounds. |
NOTE
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
i32
"). 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: i32). -
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: i32).
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: i32), 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
Testing
The language provides a built-in, zero-overhead testing facility designed for systems programming. It prioritizes process isolation and developer control over magic.
Overview
Tests in the language are defined by the
#test
attribute. When compiling for production, all functions, imports, and variables marked with
#test
are stripped from the binary, ensuring zero runtime overhead.
When running
aec test
, the compiler builds your test files as separate executables and runs them in parallel.
Writing a Basic Test
To create a test, mark a function with
#test
. By convention, tests accept a reference to a
Tap
(Test Anything Protocol) harness, though this is customizable.
The
#test
notation can precede any expression or function declaration. And you can put a test in any file.
The Test Entry Point
Unlike managed languages that hide the test runner, you own the entry point . This gives you complete control over initialization, threading models, and exit codes.
Every test file must contain a
main
function marked with
#test
that returns an
i32
.
Warning: Be careful to return
0or1. Do not returnt.faileddirectly. POSIX exit codes wrap around at 256, so returning256(failures) results in exit code0(Success).
Test Configuration (
index.json
)
Configure the test runner in your package manifest. You can define which files are treated as test suites. Organize your files however you want.
- `files` : A list of glob patterns. Each matching file is compiled into its own isolated process.
-
`quiet`
: If
true, successful tests (TAPok) are suppressed, and only failures (not ok) are printed.
Conditional Imports
Apply
#test
to import statements when importing mocking libraries or heavy test dependencies that should never end up in your production binary.
Bring Your Own Framework (BYOF)
Because you control
main
, you are not forced to use the default
Tap
harness. You can implement custom reporting logic or interface with hardware.
If you are testing bare-metal hardware where
stdout
is not available, define what
ae_stdout_write
is, or you'll get a compile time error.
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
Aela provides a stable ABI (Please review abi.h or
aec help abi
).
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.
Language Philosophy & Goals
Aela is ieneered for high-assurance embedded systems where failure is not an option. The language design prioritizes determinism , safety , and auditability above all else. Any feature that introduces ambiguity, hidden runtime costs, or non-local side effects has been strictly excluded.
Aela is designed to integrate seamlessly into existing embedded ecosystems. It maintains a stable ABI, produces object files compatible with standard build systems (like CMake), and provides native interoperability with C and C++. This includes automatic binding generation via header inclusion, precise memory layout control (packed/ordered structs), and Inversion of Control (IoC) patterns for system calls.
Excluded Features
The following features are common in general-purpose languages but are excluded from Aela to guarantee safety and predictability.
| Feature | Rationale |
|---|---|
| Generic `int` |
Ambiguity.
Platform-dependent integer sizes (16 vs 32 vs 64-bit) make portable formal verification mathematically impossible. Aela strictly enforces explicit, fixed-width types (ie,
i32
,
u64
) that behave identically on every architecture.
|
| Optional Braces | Syntactic Ambiguity. Optional braces lead to catastrophic control flow errors (ie, "Applieto fail"). Aela mandates braces for all control flow blocks, ensuring that execution scope matches visual indentation. |
| Pointer Arithmetic | Memory Safety. Direct pointer manipulation is the primary cause of buffer overflows. Aela replaces raw pointers with safe, bounds-checked slice operations. |
| Panics |
Control Flow Safety.
Panics create hidden, unrecoverable failure paths that bypass the type system. In Aela, all failure states must be represented in the function signature (ie,
Result(T)
), forcing caller handling.
|
| Exceptions | Determinism. Exceptions introduce non-local control flow and unpredictable stack unwinding, which complicates WCET (Worst-Case Execution Time) analysis. Error handling in Aela is strictly linear and explicit. |
| Implicit Heap |
Predictability.
Implicit allocation (ie,
malloc
hidden in
String
) causes fragmentation and latency spikes. Aela uses explicit
new(region)
, requiring all dynamic memory to be allocated within pre-defined, deterministic arenas.
|
| Global Mutable State | Concurrency Safety. Global variables introduce hidden dependencies ("spooky action at a distance"), making local reasoning and thread safety impossible. State must be passed explicitly or encapsulated in safe hardware abstractions. |
| Lifetime Annotations | ienomics. Explicit lifetimes add significant syntactic noise and cognitive load. Aela’s compiler infers ownership duration automatically, enforcing safety without burdening the programmer. |
| Macros |
Transparency.
Macros obscure code logic and impede static analysis. Aela replaces textual macros with
ast { ... }
blocks—strictly compile-time functions that generate type-checked ASTs, ensuring toolability and predictability.
|
| `unsafe` Blocks |
Integrity.
Broad
unsafe
blocks allow safety violations to hide anywhere. Aela instead provides a small set of "ceremoniously unsafe" intrinsic operations, making potential vulnerabilities easy to audit.
|
| Attributes | Explicitness. Attributes often inject hidden behavior or side effects. Aela avoids meta-programming tags in favor of explicit code patterns. |
| Advanced Traits | Readability. Complex trait hierarchies lead to cryptic errors and slow compilation. Aela prioritizes concrete types and simple interfaces over abstract expressive power. |
| Inline Assembly | Portability. Inline assembly breaks the optimizer and static analysis tools. Low-level architecture-specific routines must be implemented via the stable C ABI to maintain a clean verification boundary. |
| `null` Keyword |
Type Safety.
Null pointers are a billion-dollar mistake. The absence of a value must be explicitly typed (ie,
Option(T)
), forcing the programmer to handle the "empty" case.
|
| Operator Overloading |
Clarity.
Overloading hides the computational cost of operations (ie,
+
triggering a matrix allocation). Function calls must be explicit to ensure predictable performance.
|
| Implicit Conversions |
Precision.
Implicit casting hides data truncation and precision loss bugs. All type conversions must be explicit (ie,
val as u16
), forcing the programmer to acknowlie the change in data width.
|
| Unbounded Recursion | Stack Safety. Unbounded recursion prevents static stack usage analysis. Aela requires iteration via loops (which are bounded by variants) or strictly bounded recursion depth. |
| Variable Shadowing | Verification Soundness. Shadowing creates ambiguity in logical proofs regarding which "version" of a variable an invariant refers to. Aela mandates unique names for all variables within a scope. |
| Function Overloading |
Resolution Determinism.
Overloading creates ambiguity in call resolution. Aela requires unique function names (ie,
func_u8
vs
func_i32
), ensuring the call site explicitly matches the definition.
|
| Float Equality (`==`) |
Numerical Correctness.
Exact floating-point comparison is widely considered incorrect due to IEEE 754 representation errors. Aela enforces "fuzzy" comparison using explicit epsilon checks (ie,
abs(a - b) < 0.001
).
|
Included Features
These features provide the modern tooling and safety guarantees expected of a next-generation system language.
| Feature | Description |
|---|---|
| Compile-Time Memory Safety | Zero-overhead memory protection derived from region analysis and strict ownership rules, guaranteeing access safety without a garbage collector. |
| Automatic Reference Counting | Deterministic resource management where owned objects are reference-counted automatically, ensuring cleanup without manual intervention. |
| Automatic RAII |
Compiler-injected
drop
functions ensure that resources (memory, file handles, locks) are released deterministically when they go out of scope.
|
| Native Formal Verification |
Verification is a first-class citizen. Invariants (
#requires
,
#ensures
) are part of the language syntax, allowing the compiler to prove correctness without external specification files.
|
| Dependent Types | A pragmatic subset of dependent types (value-indexed types) allows the compiler to reason about the shape and size of data structures at compile time, eliminating an entire class of runtime bounds-checking errors. |
| Native Structured Concurrency | Concurrency is scoped and hierarchical. Child tasks cannot outlive their parent scopes, preventing "detached thread" leaks and ensuring rigorous cleanup of concurrent resources. |
| Automatic C/C++ Binding | Seamless interop via direct header import. The compiler parses C/C++ headers and automatically generates type-safe Aela bindings, eliminating the need for manual FFI wrappers. |
Open Source Version
An open source version of the core of the language is roadmapped for December 2026
Excluded Features
| Resource Analysis | WCET & Stack Calc | Stripped | Calculating Worst-Case Execution Time and Max Stack Usage is strictly a regulatory requirement for certification (DO-178C), not needed for general coding. |
|---|---|---|---|
| Traceability | Req Linking (DOORS) | Stripped | Linking code lines to specific requirements (ie, #req("1.4")) is valuable only to teams using heavy ALM tools like DOORS/Jama. |
| Hardware | Certified BSPs | Stripped | Support for niche safety chips (Infineon Aurix, TI Hercules) is expensive to maintain. OSS targets Linux/Generic MCU/WASM. |
| Library | Certified Std Lib | Stripped | The OSS library works, but the Enterprise library comes with a "Qualification Kit" (TCL) and legal warranty for safety claims. |
| Migration | C-to-Aela Lifter | Stripped | Tools that automatically translate C headers/source to Aela are high-value enterprise migration utilities, not daily developer tools. |
| Security | Global Taint Analysis | Stripped | Tracking "untrusted data" flows across the entire project is a specific cybersecurity compliance need (ISO 21434). |
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.
- `test`
-
The Test behavior when running
aec test. - `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: i32) -> 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: i32) -> 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 compiler enforces linear semantics on failure types. If a function signature contains a | (failure path), the caller cannot ignore the result.
| Validity | Code | Reasoning | |
|---|---|---|---|
| Valid |
let x = get_at(0)
;
|
Valid, but x is now a union that must be unpacked. | |
| Valid |
return get_at(0);
|
Valid if the caller also returns | OutOfBounds. |
NOTE
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
i32
"). 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: i32). -
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: i32).
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: i32), 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
Testing
The language provides a built-in, zero-overhead testing facility designed for systems programming. It prioritizes process isolation and developer control over magic.
Overview
Tests in the language are defined by the
#test
attribute. When compiling for production, all functions, imports, and variables marked with
#test
are stripped from the binary, ensuring zero runtime overhead.
When running
aec test
, the compiler builds your test files as separate executables and runs them in parallel.
Writing a Basic Test
To create a test, mark a function with
#test
. By convention, tests accept a reference to a
Tap
(Test Anything Protocol) harness, though this is customizable.
The
#test
notation can precede any expression or function declaration. And you can put a test in any file.
The Test Entry Point
Unlike managed languages that hide the test runner, you own the entry point . This gives you complete control over initialization, threading models, and exit codes.
Every test file must contain a
main
function marked with
#test
that returns an
i32
.
Warning: Be careful to return
0or1. Do not returnt.faileddirectly. POSIX exit codes wrap around at 256, so returning256(failures) results in exit code0(Success).
Test Configuration (
index.json
)
Configure the test runner in your package manifest. You can define which files are treated as test suites. Organize your files however you want.
- `files` : A list of glob patterns. Each matching file is compiled into its own isolated process.
-
`quiet`
: If
true, successful tests (TAPok) are suppressed, and only failures (not ok) are printed.
Conditional Imports
Apply
#test
to import statements when importing mocking libraries or heavy test dependencies that should never end up in your production binary.
Bring Your Own Framework (BYOF)
Because you control
main
, you are not forced to use the default
Tap
harness. You can implement custom reporting logic or interface with hardware.
If you are testing bare-metal hardware where
stdout
is not available, define what
ae_stdout_write
is, or you'll get a compile time error.
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
Aela provides a stable ABI (Please review abi.h or
aec help abi
).
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.
Language Philosophy & Goals
Aela is ieneered for high-assurance embedded systems where failure is not an option. The language design prioritizes determinism , safety , and auditability above all else. Any feature that introduces ambiguity, hidden runtime costs, or non-local side effects has been strictly excluded.
Aela is designed to integrate seamlessly into existing embedded ecosystems. It maintains a stable ABI, produces object files compatible with standard build systems (like CMake), and provides native interoperability with C and C++. This includes automatic binding generation via header inclusion, precise memory layout control (packed/ordered structs), and Inversion of Control (IoC) patterns for system calls.
Excluded Features
The following features are common in general-purpose languages but are excluded from Aela to guarantee safety and predictability.
| Feature | Rationale |
|---|---|
| Generic `int` |
Ambiguity.
Platform-dependent integer sizes (16 vs 32 vs 64-bit) make portable formal verification mathematically impossible. Aela strictly enforces explicit, fixed-width types (ie,
i32
,
u64
) that behave identically on every architecture.
|
| Optional Braces | Syntactic Ambiguity. Optional braces lead to catastrophic control flow errors (ie, "Applieto fail"). Aela mandates braces for all control flow blocks, ensuring that execution scope matches visual indentation. |
| Pointer Arithmetic | Memory Safety. Direct pointer manipulation is the primary cause of buffer overflows. Aela replaces raw pointers with safe, bounds-checked slice operations. |
| Panics |
Control Flow Safety.
Panics create hidden, unrecoverable failure paths that bypass the type system. In Aela, all failure states must be represented in the function signature (ie,
Result(T)
), forcing caller handling.
|
| Exceptions | Determinism. Exceptions introduce non-local control flow and unpredictable stack unwinding, which complicates WCET (Worst-Case Execution Time) analysis. Error handling in Aela is strictly linear and explicit. |
| Implicit Heap |
Predictability.
Implicit allocation (ie,
malloc
hidden in
String
) causes fragmentation and latency spikes. Aela uses explicit
new(region)
, requiring all dynamic memory to be allocated within pre-defined, deterministic arenas.
|
| Global Mutable State | Concurrency Safety. Global variables introduce hidden dependencies ("spooky action at a distance"), making local reasoning and thread safety impossible. State must be passed explicitly or encapsulated in safe hardware abstractions. |
| Lifetime Annotations | ienomics. Explicit lifetimes add significant syntactic noise and cognitive load. Aela’s compiler infers ownership duration automatically, enforcing safety without burdening the programmer. |
| Macros |
Transparency.
Macros obscure code logic and impede static analysis. Aela replaces textual macros with
ast { ... }
blocks—strictly compile-time functions that generate type-checked ASTs, ensuring toolability and predictability.
|
| `unsafe` Blocks |
Integrity.
Broad
unsafe
blocks allow safety violations to hide anywhere. Aela instead provides a small set of "ceremoniously unsafe" intrinsic operations, making potential vulnerabilities easy to audit.
|
| Attributes | Explicitness. Attributes often inject hidden behavior or side effects. Aela avoids meta-programming tags in favor of explicit code patterns. |
| Advanced Traits | Readability. Complex trait hierarchies lead to cryptic errors and slow compilation. Aela prioritizes concrete types and simple interfaces over abstract expressive power. |
| Inline Assembly | Portability. Inline assembly breaks the optimizer and static analysis tools. Low-level architecture-specific routines must be implemented via the stable C ABI to maintain a clean verification boundary. |
| `null` Keyword |
Type Safety.
Null pointers are a billion-dollar mistake. The absence of a value must be explicitly typed (ie,
Option(T)
), forcing the programmer to handle the "empty" case.
|
| Operator Overloading |
Clarity.
Overloading hides the computational cost of operations (ie,
+
triggering a matrix allocation). Function calls must be explicit to ensure predictable performance.
|
| Implicit Conversions |
Precision.
Implicit casting hides data truncation and precision loss bugs. All type conversions must be explicit (ie,
val as u16
), forcing the programmer to acknowlie the change in data width.
|
| Unbounded Recursion | Stack Safety. Unbounded recursion prevents static stack usage analysis. Aela requires iteration via loops (which are bounded by variants) or strictly bounded recursion depth. |
| Variable Shadowing | Verification Soundness. Shadowing creates ambiguity in logical proofs regarding which "version" of a variable an invariant refers to. Aela mandates unique names for all variables within a scope. |
| Function Overloading |
Resolution Determinism.
Overloading creates ambiguity in call resolution. Aela requires unique function names (ie,
func_u8
vs
func_i32
), ensuring the call site explicitly matches the definition.
|
| Float Equality (`==`) |
Numerical Correctness.
Exact floating-point comparison is widely considered incorrect due to IEEE 754 representation errors. Aela enforces "fuzzy" comparison using explicit epsilon checks (ie,
abs(a - b) < 0.001
).
|
Included Features
These features provide the modern tooling and safety guarantees expected of a next-generation system language.
| Feature | Description |
|---|---|
| Compile-Time Memory Safety | Zero-overhead memory protection derived from region analysis and strict ownership rules, guaranteeing access safety without a garbage collector. |
| Automatic Reference Counting | Deterministic resource management where owned objects are reference-counted automatically, ensuring cleanup without manual intervention. |
| Automatic RAII |
Compiler-injected
drop
functions ensure that resources (memory, file handles, locks) are released deterministically when they go out of scope.
|
| Native Formal Verification |
Verification is a first-class citizen. Invariants (
#requires
,
#ensures
) are part of the language syntax, allowing the compiler to prove correctness without external specification files.
|
| Dependent Types | A pragmatic subset of dependent types (value-indexed types) allows the compiler to reason about the shape and size of data structures at compile time, eliminating an entire class of runtime bounds-checking errors. |
| Native Structured Concurrency | Concurrency is scoped and hierarchical. Child tasks cannot outlive their parent scopes, preventing "detached thread" leaks and ensuring rigorous cleanup of concurrent resources. |
| Automatic C/C++ Binding | Seamless interop via direct header import. The compiler parses C/C++ headers and automatically generates type-safe Aela bindings, eliminating the need for manual FFI wrappers. |
Open Source Version
An open source version of the core of the language is roadmapped for December 2026
Excluded Features
| Resource Analysis | WCET & Stack Calc | Stripped | Calculating Worst-Case Execution Time and Max Stack Usage is strictly a regulatory requirement for certification (DO-178C), not needed for general coding. |
|---|---|---|---|
| Traceability | Req Linking (DOORS) | Stripped | Linking code lines to specific requirements (ie, #req("1.4")) is valuable only to teams using heavy ALM tools like DOORS/Jama. |
| Hardware | Certified BSPs | Stripped | Support for niche safety chips (Infineon Aurix, TI Hercules) is expensive to maintain. OSS targets Linux/Generic MCU/WASM. |
| Library | Certified Std Lib | Stripped | The OSS library works, but the Enterprise library comes with a "Qualification Kit" (TCL) and legal warranty for safety claims. |
| Migration | C-to-Aela Lifter | Stripped | Tools that automatically translate C headers/source to Aela are high-value enterprise migration utilities, not daily developer tools. |
| Security | Global Taint Analysis | Stripped | Tracking "untrusted data" flows across the entire project is a specific cybersecurity compliance need (ISO 21434). |
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.
- `test`
-
The Test behavior when running
aec test. - `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: i32) -> 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: i32) -> 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 compiler enforces linear semantics on failure types. If a function signature contains a | (failure path), the caller cannot ignore the result.
| Validity | Code | Reasoning | |
|---|---|---|---|
| Valid |
let x = get_at(0)
;
|
Valid, but x is now a union that must be unpacked. | |
| Valid |
return get_at(0);
|
Valid if the caller also returns | OutOfBounds. |
NOTE
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
i32
"). 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: i32). -
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: i32).
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: i32), 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
Testing
The language provides a built-in, zero-overhead testing facility designed for systems programming. It prioritizes process isolation and developer control over magic.
Overview
Tests in the language are defined by the
#test
attribute. When compiling for production, all functions, imports, and variables marked with
#test
are stripped from the binary, ensuring zero runtime overhead.
When running
aec test
, the compiler builds your test files as separate executables and runs them in parallel.
Writing a Basic Test
To create a test, mark a function with
#test
. By convention, tests accept a reference to a
Tap
(Test Anything Protocol) harness, though this is customizable.
The
#test
notation can precede any expression or function declaration. And you can put a test in any file.
The Test Entry Point
Unlike managed languages that hide the test runner, you own the entry point . This gives you complete control over initialization, threading models, and exit codes.
Every test file must contain a
main
function marked with
#test
that returns an
i32
.
Warning: Be careful to return
0or1. Do not returnt.faileddirectly. POSIX exit codes wrap around at 256, so returning256(failures) results in exit code0(Success).
Test Configuration (
index.json
)
Configure the test runner in your package manifest. You can define which files are treated as test suites. Organize your files however you want.
- `files` : A list of glob patterns. Each matching file is compiled into its own isolated process.
-
`quiet`
: If
true, successful tests (TAPok) are suppressed, and only failures (not ok) are printed.
Conditional Imports
Apply
#test
to import statements when importing mocking libraries or heavy test dependencies that should never end up in your production binary.
Bring Your Own Framework (BYOF)
Because you control
main
, you are not forced to use the default
Tap
harness. You can implement custom reporting logic or interface with hardware.
If you are testing bare-metal hardware where
stdout
is not available, define what
ae_stdout_write
is, or you'll get a compile time error.
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
Aela provides a stable ABI (Please review abi.h or
aec help abi
).
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.