Skip to content

Miloworks hard to keep your memory safe so you don't have to

Safe systems programming language with formal verification built-in

Milo

Milo is a memory-safe systems language that guides you to simple, correct, readable programs. Contracts are built in, enabling formal verification that guarantees correctness across your codebase, no matter how large. People and AI ship with confidence that their code is correct. Learn more or see how it measures up to Rust.

milo
fn main() {
    let name = "world"
    print($"hello, {name}")
}
milo
fn clamp(x: i64, lo: i64, hi: i64): i64 {
    if x < lo { return lo }
    if x > hi { return hi }
    return x
}
milo
fn clamp(x: i64, lo: i64, hi: i64): i64
    requires lo <= hi                       // the caller's obligation
    ensures result >= lo && result <= hi    // proven, for every input that meets it
{
    if x < lo { return lo }
    if x > hi { return hi }
    return x
}
milo
from "std/math" import { sqrt }

struct Point {
    x: f64,
    y: f64,
}

impl Point {
    fn dist(self: &Self): f64 {
        return sqrt(self.x * self.x + self.y * self.y)
    }
}

fn main() {
    let p = Point { x: 3.0, y: 4.0 }
    print($"{p.dist()}")   // 5
}
milo
fn main() {
    let name = "milo"
    let greeting = name   // `name` moves here. It is no longer yours

    print(greeting)       // "milo"
    print(name)           // error: use of moved variable 'name'
}
milo
from "std/net" import { fetch }
from "std/runtime" import { Promise }

fn main() {
    let a = Promise<i32>.run(() => fetch("https://example.com")!.status)
    let b = Promise<i32>.run(() => fetch("https://httpbin.org/get")!.status)

    print($"{a.await()!} {b.await()!}")   // 200 200
}

Built with Milo

We build the language by building things with it. We dogfood Milo to get a feedback loop that helps us continuously improve the safety and ergonomics of the language.