Stable State

Aela Programming Language

Aela is a safety critical systems programming language for domains like aircraft, vehicles, medical devices, factories and government systems, but it works just as well for general-purpose software, such as tools, servers and libraries, on Linux, macOS, Windows and bare metal.

What Aela Does

01
Proofs in the Compiler

Write what a function needs and what it promises with #requires and #ensures, and what a loop keeps true with #invariant. aec --verify proves them, and proves that every sum, index and cast stays in range. You need no other tool.
02
Nothing Hidden

No exceptions, no unwinding, no operator overloading and no implicit conversions. Every failure a function can return is in its signature, and the caller must handle it. Every place where async code can pause is marked with await.
03
A Toolchain You Can Check

The compiler is written in Aela, with no C and no LLVM, and writes plain assembly. It is built from a seed of 8,600 lines of assembly. Each release is built two separate ways, and both must give the same result. Every program records what built it (aec provenance).
04
Memory Safety Without Lifetimes

Every reference names the variable it borrows from. The compiler uses that to stop dangling references, use after move, and two writers changing the same data. You never write lifetimes in your code.
05
From Servers to Bare Metal

Linux, macOS and Windows on x86-64 and AArch64, plus bare-metal AArch64. For bare metal, a module that needs an operating system is refused when you compile. A target can set flash and RAM budgets, and the build fails if the program is over them.
06
Small Language

Aela has one clear way to do most things, so there are fewer patterns to learn. No macros, no inheritance and no overloading. Code reads the same from one author to the next.

Verification

Failures

Parallelism

Regions

HTTPS

Hello

verify.ae

// Contracts the compiler proves: aec --verify verify.ae
// A refinement type: an i64 that is always a valid percentage.
type Percent = { p: i64 where 0 <= p && p <= 100 };
#let before = n;
#requires before >= 0 && before < 1000;
#ensures result == before + 1;
fn bump(n: i64) -> i64 { return n + 1; }
// the average of xs, proven in range: every element is a Percent
fn average(xs: &Percent[]) -> Percent | Overflow | DivByZero {
    #let count = xs.len;
    var total: i64 = 0;
    var i: i64 = 0;
    #invariant 0 <= i && i <= count;
    #variant count - i;
    while (i < xs.len) {
        (total += xs[i])?;
        i += 1;
    }
    let mean: i64 = (total / xs.len)?;
    // without this check: error E0813, mean is not proven to be a Percent
    if (mean < 0 || mean > 100) { return 0; }
    return mean;
}
fn main() -> i32 | Overflow | DivByZero {
    let scores: Percent[] = [72, 95, 88];
    println("bump: \(bump(41)), average: \(average(&scores)?)");
    return 0;
}

https.ae

// An HTTPS server, and a client that trusts its certificate (TLS 1.3).
import http from "std/http";
import https from "std/https";
async fn hello(req: http::Incoming, mut res: &http::Responder) -> void {
    await res.send_text(200, "hello over TLS 1.3");
}
async fn get(port: i64, cert: u8[]) -> string | https::BadIdentity {
    var req = http::request("GET", "https://localhost:\(port)/");
    https::trust(mut &req, &cert)?; // pin the server's certificate
    match (await http::fetch(&req)) {
        res => {
            let status = res.status;
            let body: string = match (await res.text()) {
                t => t,
                e: http::BadResponse => "", e2: http::Lost => ""
            };
            http::close(res);
            return "\(status) \(body)";
        },
        e: http::BadRequest => { return "bad request: \(e.why)"; },
        e2: http::Unavailable => { return "no connection: \(e2.why)"; },
        e3: http::BadResponse => { return "bad response"; },
        e4: http::Lost => { return "lost"; }
    }
}
// the server until ctl says stop
async fn run(srv0: http::Server, ctl: Shared(http::Control)) -> void {
    var srv = srv0;
    await http::serve_with(mut &srv, hello, http::Options {}, ctl);
    http::close_server(srv);
}
async fn main() -> i32 | https::BadIdentity {
    let id = https::self_signed(["localhost", "127.0.0.1"])?;
    let srv: http::Server = match (http::listen_tls("127.0.0.1", 0, &id)) {
        s => s,
        e: http::ListenError => { eprintln("listen: \(e.why)"); return 1; }
    };
    let port = srv.port;
    let ctl = http::control();
    let server = std::spawn(run(srv, ctl));
    let said: string = match (await get(port, std::copy(id.cert))) {
        s => s,
        e: https::BadIdentity => "not trusted: \(e.why)"
    };
    println(said); // 200 hello over TLS 1.3
    ctl.stop = true;
    await server;
    return 0;
}

More About the Language

Checked arithmetic

Overflow, division by zero and indexing past the end stop the program instead of corrupting data. If you want numbers to wrap around, you say so with +%, -% and *%.
Types that know values

A type can limit its values, like { p: i64 where p <= 100 }, or carry a size, like Buf(N). Then the compiler can prove an index is safe and skip the check at run time.
Regions and arenas

Inside a reserve block, allocate as much as you like. Everything is freed at once when the block ends. The compiler makes sure nothing outlives the block. There is no garbage collector and no manual free.
Async and parallel tasks

async and await are part of the language. The compiler proves that parallel tasks cannot race, and every task you start must be awaited or detached. When async code fails, the report shows the chain of tasks that were waiting on it.
Large standard library

HTTP and TLS, JSON, regular expressions, compression, crypto, a terminal UI kit and more. It works on bare metal, inside a C program, and on Linux, macOS and Windows.
C when you need it

Call C functions with extern fn, and say what they touch, so the race checks cover them too. Aela code can also run inside a C program.

Aela 3.0.0 — Community Edition

The compiler, the runtime and the standard library, under the MIT license. To build programs you only need an assembler and a linker: as and ld on Linux, clang on macOS, or LLVM's clang and lld-link on Windows, where aec writes the assembly and you link it.

install.sh

# macOS and Linux: unpack the archive and run its install script.
# It puts aec in ~/.local/bin (or the folder you give it).
tar xzf aela-3.0.0-macos-arm64.tar.gz
sh aela-3.0.0-macos-arm64/install.sh
aec --version
# Windows, in PowerShell: unzip the archive and run its install script.
#   powershell -ExecutionPolicy Bypass -File aela-3.0.0-windows-x64\install.ps1
# The docs are in the compiler.
aec docs closures             # search the language docs
aec doc std/http              # show a standard library module
aec explain E0408             # explain an error code

Each package has a SHA256SUMS file and a signature, which you can check with ssh-keygen -Y verify -n aela-release. The assembly package has the compiler for every target as source code, so you can build it yourself instead of trusting our binary.

The Zap Editor, built in Aela.

What Aela Is Not

Not Rust

Aela looks superficially like Rust, but it is a different language. Rust code and habits do not carry over. aec fix rewrites common ones.
Not for 32-bit chips

The compiler makes 64-bit code only: x86-64 and AArch64. Small 32-bit microcontrollers are not supported.
Not a timing tool

The build checks a program's flash and RAM against its budgets. Stack, heap and CPU time are not measured yet, and there is no worst-case timing analysis.

Aela Programming Language

What Aela Does

Proofs in the Compiler

Nothing Hidden

A Toolchain You Can Check

Memory Safety Without Lifetimes

From Servers to Bare Metal

Small Language

More About the Language

Checked arithmetic

Types that know values

Regions and arenas

Async and parallel tasks

Large standard library

C when you need it

Aela 3.0.0 — Community Edition

macOS

macOS

Linux

Linux

Windows

Windows

Source

What Aela Is Not

Not Rust

Not for 32-bit chips

Not a timing tool