Aela Programming Language

Aela is a compiled, memory-safe language with a strong, static type system. It started as a fork of Rust, but has been significantly modified for the specific needs of embedded systems — get started now .

Enter your customer Id to generate a compiler download

Formal Verification

Aela provides formally verifiable primitives for liveness and safety guarantees at compile time.

Dependent & Refinement Types

A rigorous type system that understands the value of the data at compile-time, not just the shape.

account.ae
1 struct Queue {
2 items : int [ ] ;
3 }
4
5 impl Queue {
6 // SAFETY: Items must never become negative
7 // in length (trivial for Array, but still formalized)
8 invariant queueHasNonNegativeLength = std : : length ( items ) > = 0
9
10 // LIVENESS: For any task, we guarantee the queue
11 // eventually becomes non-empty.
12 property eventuallyReceivesItem = forall ( let task : Task in Tasks ) {
13 eventually ( std : : length ( items ) ! = 0 )
14 }
15
16 async fn dequeue ( ) - > int {
17 requires true
18 ensures std : : length ( items ) < old ( std : : length ( items ) )
19
20 // Spin until queue has at least one item
21 while std : : is_empty ( items ) {
22 await wait_for_item ( ) ; // suspend point
23 }
24
25 let item = std : : pop ( items ) ;
26 return item ;
27 }
28
29 fn enqueue ( value : int ) {
30 requires true
31 ensures std : : contains ( items , value )
32
33 std : : push ( items , value ) ;
34 notify_waiters ( ) ; // awaken suspended dequeuers
35 }
36 }
f64 { return numerator / denominator; } // Bridge from untrusted inputs to proven code. fn process_division_request(num: i32, den: i32) -> void { print("Attempting to calculate {} / {}", num, den); // Flow-typing: inside this block the compiler knows den != 0, // so `den` refines to `NonZero`. if (den != 0) { let result: = safe_divide(num, den); print(" -> Success! Result: {}", result); } else { print(" -> Error: Division by zero was prevented."); } } fn main() -> int { process_division_request(100, 5); // succeeds process_division_request(99, 0); // safely rejected at the call site return 0; }" class="content-b" id="7193f0269126d">
types.ae
0 import { print } from "stdlib / io . ae" ;
1
2 // The `where` clause is a contract enforced by the compiler.
3 type NonZero = { n : i32 where n ! = 0 } ;
4
5 // Impossible to call with a zero denominator.
6 fn safe_divide ( numerator : f64 , denominator : NonZeroF64 ) - > f64 {
7 return numerator / denominator ;
8 }
9
10 // Bridge from untrusted inputs to proven code.
11 fn process_division_request ( num : i32 , den : i32 ) - > void {
12 print ( "Attempting to calculate { } / { } " , num , den ) ;
13
14 // Flow-typing: inside this block the compiler knows den != 0,
15 // so `den` refines to `NonZero`.
16 if ( den ! = 0 ) {
17 let result : = safe_divide ( num , den ) ;
18 print ( " - > Success ! Result : { } " , result ) ;
19 } else {
20 print ( " - > Error : Division by zero was prevented . " ) ;
21 }
22 }
23
24 fn main ( ) - > int {
25 process_division_request ( 100 , 5 ) ; // succeeds
26 process_division_request ( 99 , 0 ) ; // safely rejected at the call site
27 return 0 ;
28 }

Type Safety

Go beyond checking the shape of your types by establishing powerful compile-time constraints on their potential values.

Formal Verification

Encode mathematical proofs and invariants directly into the type system and close the gap between theoretical proofs and working code.

Small Surface Area

A minimal core with no macros, advanced traits, attributes, or complex metaprogramming reduces the language's surface area and potential complexity.

Designed For Bare Metal

The standard library was designed from the start with MCUs and bare metal in mind, only import what you want.

Fast Compile Times

Leaning on an optimized LLVM, we produce predictable, repeatable, cross-platform output, even fast cold builds.

JIT Enabled Development

An optional Just-In-Time (JIT) development mode provides an edit-and-continue experience, while release mode produces fast and lean final artifacts.

C and C++ BFFs

Integrate seamlessly with existing build tools thanks to a stable C ABI, object file output, and automatic binding via header files.

Structured Concurrency

Built-in async/await syntax powered by LLVM coroutines and an efficient event loop makes concurrent programming safe and easy to reason about.

An Interactive Compiler

The compiler includes a deeply integrated AI that continuously learns from the codebase to provide automated refactoring, bug fixes, and performance optimizations.

"Just works" in your favorite editor.