Sleight: A Language for LLMs

Slides for a talk on Sleight, a programming language with restricted dependent types whose proofs erase at compile time, designed for LLMs to write, and on an agent runner that tests whether models can write it. In the main task, models write a fast, in-place heapsort certified correct against a supplied specification; 25 of 28 runs across 10 models passed, and their sorts run in about the time of handwritten C and OCaml. The talk also covers what the models found hard, an attempt to have agents prove False, and the language itself: erasure and uniqueness declared on every binder, zero-cost coercions, memory locations tracked separately from values, termination by first-class levels, Type : Type with no positivity check, Kernel-style first-class special forms, and three implementations (an OCaml reference interpreter, a self-hosted compiler, and a Lean 4 model with a machine-checked soundness proof for a fragment). An appendix gives further examples, the soundness sketch, and the full benchmark tables. Code: https://doi.org/10.5281/zenodo.23361871