Aela Programming Language
Aela is a safety-critical language with native formal verification, dependent types, and structured concurrency, engineered for embedded systems and optimized for deterministic, high-assurance software.
6 Reasons to Choose Aela...
1
Eliminate memory-safety risk at the source
Unsafe constructs cannot compile, removing buffer overflows, data races, and use-after-free errors before they can even enter mission software.
2
Guarantee correctness with built-in formal methods
Native formal verification and dependent types enable mathematically provable behavior required for DAL A, SIL 4, and ASIL D-level systems powerd by Z3.
3
High assurance without high complexity
A reduced, Rust-derived surface area makes Aela deterministic, teachable, and engineered specifically for embedded and safety-critical development.
4
Automated certification artifacts, every build
Traceability matrices, test evidence, and verification reports are produced automatically during compilation, cutting documentation work by 60–70%.
5
Accelerate DO-178C, ISO 26262, and IEC 61508 approvals
By eliminating unsafe code and generating compliance artifacts automatically, Aela reduces safety certification timelines from years to months.
6
AI-assisted development and compliance
An integrated AI assistant explains errors, guides proofs, validates requirements, and optimizes performance paths across the entire development lifecycle.
1
pure
fn
sum_range
(
a
:
int
[
]
,
start
:
int
,
end
:
int
)
-
>
result
:
int
{
2
var
acc
=
0
;
3
var
i
=
start
;
4
while
(
i
<
end
)
{
5
acc
=
acc
+
a
[
i
]
;
6
i
=
i
+
1
;
7
}
8
result
=
acc
;
9
return
;
10
}
11
12
#requires for (let i in 0..std::length(a)) {
13
std
:
:
assert
(
a
[
i
]
>
=
0
)
;
14
}
15
#ensures result == sum_range(a, 0, std::length(a));
16
fn
sum
(
a
:
int
[
]
)
-
>
result
:
int
{
17
18
#let originalLength = std::length(a);
19
#let originalArray = a;
20
21
var
total
=
0
;
22
var
i
=
0
;
23
24
#invariant 0 <= i && i <= originalLength;
25
#invariant total == sum_range(originalArray, 0, i);
26
#variant originalLength - i;
27
while
(
i
<
originalLength
)
{
28
total
=
total
+
a
[
i
]
;
29
i
=
i
+
1
;
30
}
31
32
result
=
total
;
33
return
;
34
}
1
pure
fn
sum_range
(
a
:
int
[
]
,
start
:
int
,
end
:
int
)
-
>
result
:
int
{
2
var
acc
=
0
;
3
var
i
=
start
;
4
while
(
i
<
end
)
{
5
acc
=
acc
+
a
[
i
]
;
6
i
=
i
+
1
;
7
}
8
result
=
acc
;
9
return
;
10
}
11
12
#requires for (let i in 0..std::length(a)) {
13
std
:
:
assert
(
a
[
i
]
>
=
0
)
;
14
}
15
#ensures result == sum_range(a, 0, std::length(a));
16
fn
sum
(
a
:
int
[
]
)
-
>
result
:
int
{
17
18
#let originalLength = std::length(a);
19
#let originalArray = a;
20
21
var
total
=
0
;
22
var
i
=
0
;
23
24
#invariant 0 <= i && i <= originalLength;
25
#invariant total == sum_range(originalArray, 0, i);
26
#variant originalLength - i;
27
while
(
i
<
originalLength
)
{
28
total
=
total
+
a
[
i
]
;
29
i
=
i
+
1
;
30
}
31
32
result
=
total
;
33
return
;
34
}
0
import
io from "io"
;
1
import
{
Mutex
}
from "sync"
;
2
3
struct Account
{
4
balance
:
i64
5
}
6
7
var
g_account_lock
:
&
Mutex
(
Account
)
=
new
{
}
;
8
9
task
fn
worker
(
id
:
int
,
iterations
:
int
)
-
>
int
{
10
io
:
:
println
(
"
[
Task
{
}
]
Starting
.
.
.
"
,
id
)
;
11
12
var
i
=
0
;
13
while
(
i
<
iterations
)
{
14
let
guard
=
g_account_lock
.
lock
(
)
;
15
16
var
temp
=
guard
.
data
.
balance
;
17
std
:
:
sleep
(
1ms
)
;
18
guard
.
data
.
balance
=
temp
+
1
;
19
i
=
i
+
1
;
20
}
21
io
:
:
println
(
"
[
Task
{
}
]
Finished
.
"
,
id
)
;
22
return
iterations
;
23
}
24
25
fn
main
(
args
:
string
[
]
)
-
>
int
{
26
var
r1
:
int
;
27
var
r2
:
int
;
28
let
iterations_per_task
=
100
;
29
30
io
:
:
println
(
"
[
Main
]
Starting two tasks to race
for
{
}
total increments
.
.
.
"
,
iterations_per_task
*
2
)
;
31
32
work
{ // work-stealing scheduler
33
let
h1
=
worker
(
1
,
iterations_per_task
)
;
34
let
h2
=
worker
(
2
,
iterations_per_task
)
;
35
36
io
:
:
println
(
"
[
Main
]
Both tasks are running concurrently
.
"
)
;
37
38
r1
=
await
h1
;
39
io
:
:
println
(
"
[
Main
]
Awaited h1
,
got result
:
{
}
"
,
r1
)
;
40
r2
=
await
h2
;
41
io
:
:
println
(
"
[
Main
]
Awaited h2
,
got result
:
{
}
"
,
r2
)
;
42
}
43
44
io
:
:
println
(
"
[
Main
]
Work block finished
.
"
)
;
45
46
var
final_total
:
i64
=
0
;
47
48
let
guard
=
g_account_lock
.
lock
(
)
;
49
final_total
=
guard
.
data
.
balance
;
50
51
io
:
:
print
(
`
52
Task 1 increments
:
\
(
r1
)
53
Task 2 increments
:
\
(
r2
)
54
Final Total
(
Mutex test
)
:
\
(
final_total
)
55
`
)
;
56
57
if
(
final_total
=
=
(
r1
+
r2
)
)
{
58
io
:
:
println
(
"SUCCESS
:
Mutex worked
.
Final total matches expected
{
}
.
"
,
r1
+
r2
)
;
59
}
else
{
60
io
:
:
println
(
"FAILURE
:
Race condition occurred
.
Expected
{
}
but got
{
}
.
"
,
r1
+
r2
,
final_total
)
;
61
}
62
63
return
0
;
64
}
0
import
io from "io"
;
1
import
{
Mutex
}
from "sync"
;
2
3
struct Account
{
4
balance
:
i64
5
}
6
7
var
g_account_lock
:
&
Mutex
(
Account
)
=
new
{
}
;
8
9
task
fn
worker
(
id
:
int
,
iterations
:
int
)
-
>
int
{
10
io
:
:
println
(
"
[
Task
{
}
]
Starting
.
.
.
"
,
id
)
;
11
12
var
i
=
0
;
13
while
(
i
<
iterations
)
{
14
let
guard
=
g_account_lock
.
lock
(
)
;
15
16
var
temp
=
guard
.
data
.
balance
;
17
std
:
:
sleep
(
1ms
)
;
18
guard
.
data
.
balance
=
temp
+
1
;
19
i
=
i
+
1
;
20
}
21
io
:
:
println
(
"
[
Task
{
}
]
Finished
.
"
,
id
)
;
22
return
iterations
;
23
}
24
25
fn
main
(
args
:
string
[
]
)
-
>
int
{
26
var
r1
:
int
;
27
var
r2
:
int
;
28
let
iterations_per_task
=
100
;
29
30
io
:
:
println
(
"
[
Main
]
Starting two tasks to race
for
{
}
total increments
.
.
.
"
,
iterations_per_task
*
2
)
;
31
32
work
{ // work-stealing scheduler
33
let
h1
=
worker
(
1
,
iterations_per_task
)
;
34
let
h2
=
worker
(
2
,
iterations_per_task
)
;
35
36
io
:
:
println
(
"
[
Main
]
Both tasks are running concurrently
.
"
)
;
37
38
r1
=
await
h1
;
39
io
:
:
println
(
"
[
Main
]
Awaited h1
,
got result
:
{
}
"
,
r1
)
;
40
r2
=
await
h2
;
41
io
:
:
println
(
"
[
Main
]
Awaited h2
,
got result
:
{
}
"
,
r2
)
;
42
}
43
44
io
:
:
println
(
"
[
Main
]
Work block finished
.
"
)
;
45
46
var
final_total
:
i64
=
0
;
47
48
let
guard
=
g_account_lock
.
lock
(
)
;
49
final_total
=
guard
.
data
.
balance
;
50
51
io
:
:
print
(
`
52
Task 1 increments
:
\
(
r1
)
53
Task 2 increments
:
\
(
r2
)
54
Final Total
(
Mutex test
)
:
\
(
final_total
)
55
`
)
;
56
57
if
(
final_total
=
=
(
r1
+
r2
)
)
{
58
io
:
:
println
(
"SUCCESS
:
Mutex worked
.
Final total matches expected
{
}
.
"
,
r1
+
r2
)
;
59
}
else
{
60
io
:
:
println
(
"FAILURE
:
Race condition occurred
.
Expected
{
}
but got
{
}
.
"
,
r1
+
r2
,
final_total
)
;
61
}
62
63
return
0
;
64
}
1
import
io from "io"
;
2
import
{
Test
,
Tap
}
from "test"
;
3
4
struct Vec
(
T
,
N
:
int
)
{
5
data
:
T
[
N
]
6
}
7
8
impl Vec
(
T
,
N
)
{
9
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
10
return
self
;
11
}
12
13
fn
head
(
self
:
&
Self
)
-
>
T
{
14
return
self
.
data
[
0
]
;
15
}
16
}
17
18
struct Vec2
(
T
,
N
:
int
)
{
19
data
:
T
[
N
]
,
20
length
:
int
,
21
typeSize
:
int
22
}
23
24
impl Vec2
(
T
,
N
:
int
)
{
25
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
26
self
.
typeSize
=
std
:
:
size
(
T
)
;
27
var
i
:
int
=
0
;
28
while
(
i
<
std
:
:
length
(
data
)
)
{
29
self
.
data
[
i
]
=
data
[
i
]
;
30
i
+
=
1
;
31
}
32
33
return
self
;
34
}
35
}
36
37
38
fn
get_first
(
T
,
N
:
int
;
v
:
&
Vec
(
T
,
N
)
)
-
>
T
{
39
return
v
.
data
[
0
]
;
40
}
41
42
enum
Result
(
T
,
E
)
{
43
Ok
(
T
)
,
44
Err
(
E
)
45
}
46
47
fn
test_create_specialized_struct
(
t
:
&
Tap
)
-
>
bool
{
48
let
v
:
Vec
(
int
,
1024
)
;
49
v
.
data
[
0
]
=
42
;
50
let
fa
:
int
=
v
.
head
(
)
;
51
let
fb
:
int
=
get_first
(
int
,
1024
,
&
v
)
;
52
t
.
ok
(
v
.
data
[
0
]
=
=
42
,
"the first item
in
the vector data is
'a'
"
)
;
53
t
.
ok
(
fa
=
=
42
,
"the first item
in
the vector is
'a'
"
)
;
54
t
.
ok
(
fb
=
=
42
,
"the first item
in
the vector data is
'a'
(
via
function
interface
)
"
)
;
55
56
let
v2
:
&
Vec2
(
string
,
1024
)
=
new
[
"xyz"
]
;
57
t
.
ok
(
v2
.
data
[
0
]
=
=
"xyz"
,
"partial initialization worked
,
the first item is a match"
)
;
58
t
.
ok
(
v2
.
typeSize
=
=
16
,
"type size of vec2 is correct"
)
;
59
return
true
;
60
}
61
62
fn
test_create_specialized_enum
(
t
:
&
Tap
)
-
>
bool
{
63
let
r
:
Result
(
int
,
string
)
=
Result
:
:
Ok
(
42
)
;
64
t
.
ok
(
"Ok
(
42
)
"
=
=
std
:
:
format
(
"
{
}
"
,
r
)
,
"result contains the expected valaue"
)
;
65
return
true
;
66
}
67
68
export
fn
runner
(
)
-
>
Tap
{
69
io
:
:
print
(
"# Testing Dependent Types
70
"
)
;
71
let
tests
:
Test
[
]
=
[
72
test_create_specialized_struct
,
73
test_create_specialized_enum
,
74
]
;
75
76
let
t
:
Tap
=
{
}
;
77
t
.
run
(
tests
)
;
78
return
t
;
79
}
1
import
io from "io"
;
2
import
{
Test
,
Tap
}
from "test"
;
3
4
struct Vec
(
T
,
N
:
int
)
{
5
data
:
T
[
N
]
6
}
7
8
impl Vec
(
T
,
N
)
{
9
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
10
return
self
;
11
}
12
13
fn
head
(
self
:
&
Self
)
-
>
T
{
14
return
self
.
data
[
0
]
;
15
}
16
}
17
18
struct Vec2
(
T
,
N
:
int
)
{
19
data
:
T
[
N
]
,
20
length
:
int
,
21
typeSize
:
int
22
}
23
24
impl Vec2
(
T
,
N
:
int
)
{
25
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
26
self
.
typeSize
=
std
:
:
size
(
T
)
;
27
var
i
:
int
=
0
;
28
while
(
i
<
std
:
:
length
(
data
)
)
{
29
self
.
data
[
i
]
=
data
[
i
]
;
30
i
+
=
1
;
31
}
32
33
return
self
;
34
}
35
}
36
37
38
fn
get_first
(
T
,
N
:
int
;
v
:
&
Vec
(
T
,
N
)
)
-
>
T
{
39
return
v
.
data
[
0
]
;
40
}
41
42
enum
Result
(
T
,
E
)
{
43
Ok
(
T
)
,
44
Err
(
E
)
45
}
46
47
fn
test_create_specialized_struct
(
t
:
&
Tap
)
-
>
bool
{
48
let
v
:
Vec
(
int
,
1024
)
;
49
v
.
data
[
0
]
=
42
;
50
let
fa
:
int
=
v
.
head
(
)
;
51
let
fb
:
int
=
get_first
(
int
,
1024
,
&
v
)
;
52
t
.
ok
(
v
.
data
[
0
]
=
=
42
,
"the first item
in
the vector data is
'a'
"
)
;
53
t
.
ok
(
fa
=
=
42
,
"the first item
in
the vector is
'a'
"
)
;
54
t
.
ok
(
fb
=
=
42
,
"the first item
in
the vector data is
'a'
(
via
function
interface
)
"
)
;
55
56
let
v2
:
&
Vec2
(
string
,
1024
)
=
new
[
"xyz"
]
;
57
t
.
ok
(
v2
.
data
[
0
]
=
=
"xyz"
,
"partial initialization worked
,
the first item is a match"
)
;
58
t
.
ok
(
v2
.
typeSize
=
=
16
,
"type size of vec2 is correct"
)
;
59
return
true
;
60
}
61
62
fn
test_create_specialized_enum
(
t
:
&
Tap
)
-
>
bool
{
63
let
r
:
Result
(
int
,
string
)
=
Result
:
:
Ok
(
42
)
;
64
t
.
ok
(
"Ok
(
42
)
"
=
=
std
:
:
format
(
"
{
}
"
,
r
)
,
"result contains the expected valaue"
)
;
65
return
true
;
66
}
67
68
export
fn
runner
(
)
-
>
Tap
{
69
io
:
:
print
(
"# Testing Dependent Types
70
"
)
;
71
let
tests
:
Test
[
]
=
[
72
test_create_specialized_struct
,
73
test_create_specialized_enum
,
74
]
;
75
76
let
t
:
Tap
=
{
}
;
77
t
.
run
(
tests
)
;
78
return
t
;
79
}
1
pure
fn
sum_range
(
a
:
int
[
]
,
start
:
int
,
end
:
int
)
-
>
result
:
int
{
2
var
acc
=
0
;
3
var
i
=
start
;
4
while
(
i
<
end
)
{
5
acc
=
acc
+
a
[
i
]
;
6
i
=
i
+
1
;
7
}
8
result
=
acc
;
9
return
;
10
}
11
12
#requires for (let i in 0..std::length(a)) {
13
std
:
:
assert
(
a
[
i
]
>
=
0
)
;
14
}
15
#ensures result == sum_range(a, 0, std::length(a));
16
fn
sum
(
a
:
int
[
]
)
-
>
result
:
int
{
17
18
#let originalLength = std::length(a);
19
#let originalArray = a;
20
21
var
total
=
0
;
22
var
i
=
0
;
23
24
#invariant 0 <= i && i <= originalLength;
25
#invariant total == sum_range(originalArray, 0, i);
26
#variant originalLength - i;
27
while
(
i
<
originalLength
)
{
28
total
=
total
+
a
[
i
]
;
29
i
=
i
+
1
;
30
}
31
32
result
=
total
;
33
return
;
34
}
1
pure
fn
sum_range
(
a
:
int
[
]
,
start
:
int
,
end
:
int
)
-
>
result
:
int
{
2
var
acc
=
0
;
3
var
i
=
start
;
4
while
(
i
<
end
)
{
5
acc
=
acc
+
a
[
i
]
;
6
i
=
i
+
1
;
7
}
8
result
=
acc
;
9
return
;
10
}
11
12
#requires for (let i in 0..std::length(a)) {
13
std
:
:
assert
(
a
[
i
]
>
=
0
)
;
14
}
15
#ensures result == sum_range(a, 0, std::length(a));
16
fn
sum
(
a
:
int
[
]
)
-
>
result
:
int
{
17
18
#let originalLength = std::length(a);
19
#let originalArray = a;
20
21
var
total
=
0
;
22
var
i
=
0
;
23
24
#invariant 0 <= i && i <= originalLength;
25
#invariant total == sum_range(originalArray, 0, i);
26
#variant originalLength - i;
27
while
(
i
<
originalLength
)
{
28
total
=
total
+
a
[
i
]
;
29
i
=
i
+
1
;
30
}
31
32
result
=
total
;
33
return
;
34
}
0
import
io from "io"
;
1
import
{
Mutex
}
from "sync"
;
2
3
struct Account
{
4
balance
:
i64
5
}
6
7
var
g_account_lock
:
&
Mutex
(
Account
)
=
new
{
}
;
8
9
task
fn
worker
(
id
:
int
,
iterations
:
int
)
-
>
int
{
10
io
:
:
println
(
"
[
Task
{
}
]
Starting
.
.
.
"
,
id
)
;
11
12
var
i
=
0
;
13
while
(
i
<
iterations
)
{
14
let
guard
=
g_account_lock
.
lock
(
)
;
15
16
var
temp
=
guard
.
data
.
balance
;
17
std
:
:
sleep
(
1ms
)
;
18
guard
.
data
.
balance
=
temp
+
1
;
19
i
=
i
+
1
;
20
}
21
io
:
:
println
(
"
[
Task
{
}
]
Finished
.
"
,
id
)
;
22
return
iterations
;
23
}
24
25
fn
main
(
args
:
string
[
]
)
-
>
int
{
26
var
r1
:
int
;
27
var
r2
:
int
;
28
let
iterations_per_task
=
100
;
29
30
io
:
:
println
(
"
[
Main
]
Starting two tasks to race
for
{
}
total increments
.
.
.
"
,
iterations_per_task
*
2
)
;
31
32
work
{ // work-stealing scheduler
33
let
h1
=
worker
(
1
,
iterations_per_task
)
;
34
let
h2
=
worker
(
2
,
iterations_per_task
)
;
35
36
io
:
:
println
(
"
[
Main
]
Both tasks are running concurrently
.
"
)
;
37
38
r1
=
await
h1
;
39
io
:
:
println
(
"
[
Main
]
Awaited h1
,
got result
:
{
}
"
,
r1
)
;
40
r2
=
await
h2
;
41
io
:
:
println
(
"
[
Main
]
Awaited h2
,
got result
:
{
}
"
,
r2
)
;
42
}
43
44
io
:
:
println
(
"
[
Main
]
Work block finished
.
"
)
;
45
46
var
final_total
:
i64
=
0
;
47
48
let
guard
=
g_account_lock
.
lock
(
)
;
49
final_total
=
guard
.
data
.
balance
;
50
51
io
:
:
print
(
`
52
Task 1 increments
:
\
(
r1
)
53
Task 2 increments
:
\
(
r2
)
54
Final Total
(
Mutex test
)
:
\
(
final_total
)
55
`
)
;
56
57
if
(
final_total
=
=
(
r1
+
r2
)
)
{
58
io
:
:
println
(
"SUCCESS
:
Mutex worked
.
Final total matches expected
{
}
.
"
,
r1
+
r2
)
;
59
}
else
{
60
io
:
:
println
(
"FAILURE
:
Race condition occurred
.
Expected
{
}
but got
{
}
.
"
,
r1
+
r2
,
final_total
)
;
61
}
62
63
return
0
;
64
}
0
import
io from "io"
;
1
import
{
Mutex
}
from "sync"
;
2
3
struct Account
{
4
balance
:
i64
5
}
6
7
var
g_account_lock
:
&
Mutex
(
Account
)
=
new
{
}
;
8
9
task
fn
worker
(
id
:
int
,
iterations
:
int
)
-
>
int
{
10
io
:
:
println
(
"
[
Task
{
}
]
Starting
.
.
.
"
,
id
)
;
11
12
var
i
=
0
;
13
while
(
i
<
iterations
)
{
14
let
guard
=
g_account_lock
.
lock
(
)
;
15
16
var
temp
=
guard
.
data
.
balance
;
17
std
:
:
sleep
(
1ms
)
;
18
guard
.
data
.
balance
=
temp
+
1
;
19
i
=
i
+
1
;
20
}
21
io
:
:
println
(
"
[
Task
{
}
]
Finished
.
"
,
id
)
;
22
return
iterations
;
23
}
24
25
fn
main
(
args
:
string
[
]
)
-
>
int
{
26
var
r1
:
int
;
27
var
r2
:
int
;
28
let
iterations_per_task
=
100
;
29
30
io
:
:
println
(
"
[
Main
]
Starting two tasks to race
for
{
}
total increments
.
.
.
"
,
iterations_per_task
*
2
)
;
31
32
work
{ // work-stealing scheduler
33
let
h1
=
worker
(
1
,
iterations_per_task
)
;
34
let
h2
=
worker
(
2
,
iterations_per_task
)
;
35
36
io
:
:
println
(
"
[
Main
]
Both tasks are running concurrently
.
"
)
;
37
38
r1
=
await
h1
;
39
io
:
:
println
(
"
[
Main
]
Awaited h1
,
got result
:
{
}
"
,
r1
)
;
40
r2
=
await
h2
;
41
io
:
:
println
(
"
[
Main
]
Awaited h2
,
got result
:
{
}
"
,
r2
)
;
42
}
43
44
io
:
:
println
(
"
[
Main
]
Work block finished
.
"
)
;
45
46
var
final_total
:
i64
=
0
;
47
48
let
guard
=
g_account_lock
.
lock
(
)
;
49
final_total
=
guard
.
data
.
balance
;
50
51
io
:
:
print
(
`
52
Task 1 increments
:
\
(
r1
)
53
Task 2 increments
:
\
(
r2
)
54
Final Total
(
Mutex test
)
:
\
(
final_total
)
55
`
)
;
56
57
if
(
final_total
=
=
(
r1
+
r2
)
)
{
58
io
:
:
println
(
"SUCCESS
:
Mutex worked
.
Final total matches expected
{
}
.
"
,
r1
+
r2
)
;
59
}
else
{
60
io
:
:
println
(
"FAILURE
:
Race condition occurred
.
Expected
{
}
but got
{
}
.
"
,
r1
+
r2
,
final_total
)
;
61
}
62
63
return
0
;
64
}
1
import
io from "io"
;
2
import
{
Test
,
Tap
}
from "test"
;
3
4
struct Vec
(
T
,
N
:
int
)
{
5
data
:
T
[
N
]
6
}
7
8
impl Vec
(
T
,
N
)
{
9
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
10
return
self
;
11
}
12
13
fn
head
(
self
:
&
Self
)
-
>
T
{
14
return
self
.
data
[
0
]
;
15
}
16
}
17
18
struct Vec2
(
T
,
N
:
int
)
{
19
data
:
T
[
N
]
,
20
length
:
int
,
21
typeSize
:
int
22
}
23
24
impl Vec2
(
T
,
N
:
int
)
{
25
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
26
self
.
typeSize
=
std
:
:
size
(
T
)
;
27
var
i
:
int
=
0
;
28
while
(
i
<
std
:
:
length
(
data
)
)
{
29
self
.
data
[
i
]
=
data
[
i
]
;
30
i
+
=
1
;
31
}
32
33
return
self
;
34
}
35
}
36
37
38
fn
get_first
(
T
,
N
:
int
;
v
:
&
Vec
(
T
,
N
)
)
-
>
T
{
39
return
v
.
data
[
0
]
;
40
}
41
42
enum
Result
(
T
,
E
)
{
43
Ok
(
T
)
,
44
Err
(
E
)
45
}
46
47
fn
test_create_specialized_struct
(
t
:
&
Tap
)
-
>
bool
{
48
let
v
:
Vec
(
int
,
1024
)
;
49
v
.
data
[
0
]
=
42
;
50
let
fa
:
int
=
v
.
head
(
)
;
51
let
fb
:
int
=
get_first
(
int
,
1024
,
&
v
)
;
52
t
.
ok
(
v
.
data
[
0
]
=
=
42
,
"the first item
in
the vector data is
'a'
"
)
;
53
t
.
ok
(
fa
=
=
42
,
"the first item
in
the vector is
'a'
"
)
;
54
t
.
ok
(
fb
=
=
42
,
"the first item
in
the vector data is
'a'
(
via
function
interface
)
"
)
;
55
56
let
v2
:
&
Vec2
(
string
,
1024
)
=
new
[
"xyz"
]
;
57
t
.
ok
(
v2
.
data
[
0
]
=
=
"xyz"
,
"partial initialization worked
,
the first item is a match"
)
;
58
t
.
ok
(
v2
.
typeSize
=
=
16
,
"type size of vec2 is correct"
)
;
59
return
true
;
60
}
61
62
fn
test_create_specialized_enum
(
t
:
&
Tap
)
-
>
bool
{
63
let
r
:
Result
(
int
,
string
)
=
Result
:
:
Ok
(
42
)
;
64
t
.
ok
(
"Ok
(
42
)
"
=
=
std
:
:
format
(
"
{
}
"
,
r
)
,
"result contains the expected valaue"
)
;
65
return
true
;
66
}
67
68
export
fn
runner
(
)
-
>
Tap
{
69
io
:
:
print
(
"# Testing Dependent Types
70
"
)
;
71
let
tests
:
Test
[
]
=
[
72
test_create_specialized_struct
,
73
test_create_specialized_enum
,
74
]
;
75
76
let
t
:
Tap
=
{
}
;
77
t
.
run
(
tests
)
;
78
return
t
;
79
}
1
import
io from "io"
;
2
import
{
Test
,
Tap
}
from "test"
;
3
4
struct Vec
(
T
,
N
:
int
)
{
5
data
:
T
[
N
]
6
}
7
8
impl Vec
(
T
,
N
)
{
9
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
10
return
self
;
11
}
12
13
fn
head
(
self
:
&
Self
)
-
>
T
{
14
return
self
.
data
[
0
]
;
15
}
16
}
17
18
struct Vec2
(
T
,
N
:
int
)
{
19
data
:
T
[
N
]
,
20
length
:
int
,
21
typeSize
:
int
22
}
23
24
impl Vec2
(
T
,
N
:
int
)
{
25
fn
constructor
(
mut self
:
&
Self
,
data
:
T
[
]
)
-
>
&
Self
{
26
self
.
typeSize
=
std
:
:
size
(
T
)
;
27
var
i
:
int
=
0
;
28
while
(
i
<
std
:
:
length
(
data
)
)
{
29
self
.
data
[
i
]
=
data
[
i
]
;
30
i
+
=
1
;
31
}
32
33
return
self
;
34
}
35
}
36
37
38
fn
get_first
(
T
,
N
:
int
;
v
:
&
Vec
(
T
,
N
)
)
-
>
T
{
39
return
v
.
data
[
0
]
;
40
}
41
42
enum
Result
(
T
,
E
)
{
43
Ok
(
T
)
,
44
Err
(
E
)
45
}
46
47
fn
test_create_specialized_struct
(
t
:
&
Tap
)
-
>
bool
{
48
let
v
:
Vec
(
int
,
1024
)
;
49
v
.
data
[
0
]
=
42
;
50
let
fa
:
int
=
v
.
head
(
)
;
51
let
fb
:
int
=
get_first
(
int
,
1024
,
&
v
)
;
52
t
.
ok
(
v
.
data
[
0
]
=
=
42
,
"the first item
in
the vector data is
'a'
"
)
;
53
t
.
ok
(
fa
=
=
42
,
"the first item
in
the vector is
'a'
"
)
;
54
t
.
ok
(
fb
=
=
42
,
"the first item
in
the vector data is
'a'
(
via
function
interface
)
"
)
;
55
56
let
v2
:
&
Vec2
(
string
,
1024
)
=
new
[
"xyz"
]
;
57
t
.
ok
(
v2
.
data
[
0
]
=
=
"xyz"
,
"partial initialization worked
,
the first item is a match"
)
;
58
t
.
ok
(
v2
.
typeSize
=
=
16
,
"type size of vec2 is correct"
)
;
59
return
true
;
60
}
61
62
fn
test_create_specialized_enum
(
t
:
&
Tap
)
-
>
bool
{
63
let
r
:
Result
(
int
,
string
)
=
Result
:
:
Ok
(
42
)
;
64
t
.
ok
(
"Ok
(
42
)
"
=
=
std
:
:
format
(
"
{
}
"
,
r
)
,
"result contains the expected valaue"
)
;
65
return
true
;
66
}
67
68
export
fn
runner
(
)
-
>
Tap
{
69
io
:
:
print
(
"# Testing Dependent Types
70
"
)
;
71
let
tests
:
Test
[
]
=
[
72
test_create_specialized_struct
,
73
test_create_specialized_enum
,
74
]
;
75
76
let
t
:
Tap
=
{
}
;
77
t
.
run
(
tests
)
;
78
return
t
;
79
}
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.