A programming language made for LLMs.

; Arr Body n is laid out struct-of-arrays by the compiler;
; the program only ever sees records.
type Body = { x : f64, y : f64, z : f64, vx : f64, vy : f64, vz : f64, m : f64 }
type Vec3 = { x : f64, y : f64, z : f64 }

fn accel (bs : Arr Body n, i : i64{0 <= i, i < n}) -> Vec3
  = let xi = bs[i].x in let yi = bs[i].y in let zi = bs[i].z in
    sum(j in 0..n)
      let dx = bs[j].x - xi in let dy = bs[j].y - yi in let dz = bs[j].z - zi in
      let d2 = dx * dx + dy * dy + dz * dz + 0.01 in
      let inv = bs[j].m / (d2 * sqrt(d2)) in
      Vec3 { x = dx * inv, y = dy * inv, z = dz * inv }

fn kick (bs : Arr Body n, dt : f64) -> Arr Body n
  = arr(i in 0..n) let a = accel(bs, i) in let b = bs[i] in
      b with { vx = b.vx + a.x * dt, vy = b.vy + a.y * dt, vz = b.vz + a.z * dt }

i : i64{0 <= i, i < n}

The refinement that makes bs[i] provably in range. Callers must prove it too.

arr(i in 0..n)

A comprehension: compiled as a parallel region and spread across cores.

Arr Body n

Seven field planes in one buffer, so the inner sum streams contiguous data and vectorises.

fn starts_with (a : Arr u8 n, b : Arr u8 m) -> bool
  = m <= n && loop (i : i64{i >= 0} = 0, ok = true)
                while ok && i < m
                next (i + 1, a[i] == b[i])
                yield ok

fn handle (req : Arr u8 n) -> Arr u8 _
  = if starts_with(req, "GET / ") then
      "HTTP/1.1 200 OK\r\nContent-Length: 13\r\n\r\nHello, World!"
    else
      "HTTP/1.1 404 Not Found\r\nContent-Length: 9\r\n\r\nNot Found"

; Sockets, framing, pipelining and workers belong to the runtime,
; which is written in Neo and talks to the kernel directly.
effect fn main (port : i64{port > 0, port < 65536}) -> i64
  = serve(port, handle)

handle

A pure function from request bytes to response bytes. The compiler keeps it free of effects.

serve

One worker per core, io_uring on x86-64 Linux, up to 64 pipelined responses per batch.

a[i] == b[i]

Proven in range from i < m <= n: no bounds check is emitted.