Aela

A Modern Langauge For

High Integrity Software

Enter your customer Id to generate a compiler download

Formal Verification

Aela provides formally verifiable primitives for liveness and safty guarentees at compile time.

Cross Platform UI Library

Aela provides your a GUI framework that makes it possible to ship one codebase that runs on MacOS, iOS, Linux, Android, & Windows.

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 }
int { let loop: &io::AeEventLoop = io::getLoop(); initLoop(loop); fn App () -> &View { let onclick: EventCallback = fn (event: &Event) -> void { io::print("{}", event.eventType); }; return new View { children: [ WebView { url: "https://news.ycombinator.com" }, Button { label: "save" }, Button { label: "cancel", onclick } ], onclick }; } let window: &Window = new Window(WindowOptions { title: "Aela UI Test", width: 800.0, height: 600.0 }); window.show(); window.render(App()); runLoop(); return window.exitCode; } " class="content-b" id="5ddc7f51bce0f">
gui.ae
0 import io from "io" ;
1
2 import {
3 initLoop , runLoop , Event , Button ,
4 View , Window , WindowOptions , WebView
5 } from "ui" ;
6
7 async fn main ( ) - > int {
8 let loop : & io : : AeEventLoop = io : : getLoop ( ) ;
9 initLoop ( loop ) ;
10
11 fn App ( ) - > & View {
12 let onclick : EventCallback = fn ( event : & Event ) - > void {
13 io : : print ( " { } " , event . eventType ) ;
14 } ;
15
16 return new View {
17 children : [
18 WebView { url : "https : / / news . ycombinator . com" } ,
19 Button { label : "save" } ,
20 Button { label : "cancel" , onclick }
21 ] ,
22 onclick
23 } ;
24 }
25
26 let window : & Window = new Window ( WindowOptions {
27 title : "Aela UI Test" ,
28 width : 800 . 0 ,
29 height : 600 . 0
30 } ) ;
31
32 window . show ( ) ;
33 window . render ( App ( ) ) ;
34
35 runLoop ( ) ;
36 return window . exitCode ;
37 }

Type Safety

Prove correctness at compile-time with Dependent Types & Refinement Types, ensuring your code works as intended without extensive runtime checks.

Formal Verification

Encode mathematical proofs and invariants directly into the type system, enabling a high degree of confidence in critical applications.

Small Surface Area

No macros or complex metaprogramming. A minimal feature set reduces cognitive load and eliminates entire classes of bugs.

Small Compiler

One small, auditable compiler you can ship and trust—low memory use, ideal for audits and the safety-first ethos.

Fast Compile Times

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

JIT Enabled

With Just-In-Time (JIT) development mode, you get an edit-and-continue experience, producing fast and lean final artifacts.

LSP Enabled

Designed to support a first-class Language Server Protocol (LSP) experience, providing intelligent, real-time feedback in your editor.

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

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.