Lanius

A general-purpose programming language that makes compilation, optimization, and formal reasoning scale with compute.

fn main() {
  let x: i32 = 3;
  let y: i32 = 4;
  print(x * x + y * y);
  return 0;
}

A four-part plan

Build the fastest compiler in the world

A compiler that lexes, parses, type checks, and emits code entirely on the GPU compiles orders of magnitude faster than traditional compilers.
Design expressive, explicit language features

Algebraic data types and a powerful type system encode complex ideas directly and precisely.
Define the language formally

Formal proofs establish behavioral guarantees far beyond that of fixed-purpose static analyzers.
Build the optimizer that scales

An optimizer that uses learning and search efficiently outcompetes any other optimizer, given enough scale.