LLMLL: a language for agent-written code, with a Haskell compiler that emits liquid-fixpoint constraints directly

LLMLL is a language I’ve been building to experiment with AI (LLMs) writing code. A function starts as a contract with a typed hole for the body. The contract is a typed signature, optionally refined with predicates (`(where [x: int] (> x 0))`), plus a precondition and a postcondition. When an agent attempts to fill the hole, the fill must type-check, and then the compiler checks it against the predicates and conditions with Z3 before the patch is integrated into the AST. A body the solver can’t...