Applying effect systems and type theory to infrastructure.
nix-effects embeds a Martin-Löf Type Theory proof checker in pure Nix. Dependent functions, dependent pairs, identity types with J, cumulative universes, verified extraction of plain Nix functions from proof terms. The whole system runs at nix eval time.
Nix has no loops and no tail-call optimization. builtins.genericClosure, the package dependency primitive, doubles as a general-purpose trampoline once you break the thunk chain.
AI agent sessions are distributed processes: private state, independent failure, concurrent access to shared resources. Event sourcing gives sessions durable history; CRDTs give them convergent merge, with correctness guarantees that are purely algebraic, requiring no network model.