A self-improving programming language.
Programs that evolve, verify, and optimize themselves. ML-like syntax, formally verified, multi-tier execution from tree-walker to JIT.
Why IRIS?
Self-Modifying
Your programs can inspect, rewrite, and evolve their own code at runtime. Graph introspection opcodes give programs direct access to their own structure -- swap operators, rewire edges, breed variants, and hot-swap improvements.
Verified by Construction
LCF proof kernel with 20 inference rules, zero unsafe Rust, and a Lean 4 formalization with 47 theorems (zero sorry). Refinement types and contracts verify functional correctness. A compiled Lean FFI bridge means the code that runs is the code that's proven.
Multi-Tier Execution
Programs run through a 4-tier execution cascade: tree-walking interpreter, bytecode VM, JIT-compiled x86-64, and AVX-512 SIMD containers. The right tier for the right job.
Familiar syntax, unfamiliar power.
-- Factorial with cost annotation
let rec factorial n : Int -> Int [cost: Linear(n)] =
if n <= 1 then 1
else n * factorial (n - 1)
-- GCD via Euclid's algorithm
let rec gcd a b : Int -> Int -> Int [cost: Unknown] =
if b == 0 then a
else gcd b (a % b)
-- Sum a list using fold
let sum xs : List Int -> Int [cost: Linear(xs)] =
fold 0 (+) xs
-- Filter, transform, and sum with pipes
let process xs : List Int -> Int [cost: Linear(xs)] =
xs |> filter (\x -> x > 0)
|> map (\x -> x * x)
|> fold 0 (\acc x -> acc + x)
-- Nested lambdas capture outer scope
let scale_all xs factor : List Int -> Int -> List Int =
map (\x -> x * factor) xs
-- Programs that rewrite themselves
let mutate program new_op : Program -> Int -> Program =
let root = graph_get_root program in
graph_set_prim_op program root new_op
Build it with IRIS
Get Involved
Read IRIS
Start with the language guide, explore the standard library, or dive into the architecture.
Build with IRIS
Install IRIS, run the examples, and start writing your own programs. A full library of example programs ships as references.
Contribute
IRIS is open source. Check out the GitHub repository to file issues, submit PRs, or join the discussion.