Stable State

Aela Programming Language

Aela is a compiled systems language. It checks arithmetic, makes borrowing explicit, treats errors as values, and runs async and parallel code safely. Its compiler is written in Aela, uses no C, and makes native programs for Linux, macOS, Windows and bare-metal AArch64.

6 Reasons to Use Aela

01
A small language

Aela has one clear way to do most things. There are no macros, no inheritance, no exceptions, no overloading and no implicit conversions. Code reads the same from one author to the next, so it is easy to review.
02
Formal verification, built in

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. No extra tools are needed.
03
Async you can trace and check

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.
04
A 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. On bare metal, a module that needs an operating system is refused when you compile.
05
No hidden control flow

There are no exceptions, no unwinding and no operator overloading. Every error 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.
06
A toolchain you can verify

The compiler is built from a small seed of 8,600 lines of assembly. Each release is built two separate ways, and both must give the same result. You can build the compiler yourself from its assembly source, and every program records what built it (aec provenance).

Hello

Verification

Parallelism

Failures

Regions

HTTPS

hello.ae

// Build and run it: aec hello.ae && ./hello
fn main() -> i32 {
    let name = "world";
    println("Hello, \(name)!");
    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.
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.
Seven targets

Linux, macOS and Windows on x86-64 and AArch64, plus bare-metal AArch64. The compiler does not use LLVM. It writes plain assembly that any assembler can build.
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.

Download Aela 2.2.1

The compiler, the runtime and the standard library, under the MIT license. To build programs you also 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-2.2.1-macos-arm64.tar.gz
sh aela-2.2.1-macos-arm64/install.sh
aec --version
# Windows, in PowerShell: unzip the archive and run its install script.
#   powershell -ExecutionPolicy Bypass -File aela-2.2.1-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.

Highlighting, errors as you type, and go to definition in VS Code, Neovim, Vim and IntelliJ, through aec lsp. Builds and errors in Xcode.

Aela Programming Language

6 Reasons to Use Aela

A small language

Formal verification, built in

Async you can trace and check

A large standard library

No hidden control flow

A toolchain you can verify

More About the Language

Checked arithmetic

Types that know values

Regions and arenas

Memory safety without lifetimes

Seven targets

C when you need it

Download Aela 2.2.1

macOS

macOS

Linux

Linux

Windows

Windows

Source