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 prove is rejected, and the program is left as it was.
The idea is that multiple, potentially specialized, agents work in parallel to fill all the holes at once.
All of the code, the Haskell compiler included, was written by LLM agents. My role was that of a technical director.
The parts this forum might find interesting:
Scope, so nobody has to ask: the solver covers linear integer arithmetic, booleans, non-recursive sums, pairs, fixed-size bytes, maps and string literals. Outside that, a postcondition is assumed and the tool says so by name. A proof shows the body matches the contract, not that the contract is right.
A two-minute demo, using Apple’s goto-fail bug as the invariant (a scripted wrong body rejected, then a guarded one accepted): LLMLL: a goto-fail body, rejected before the edit lands | LLMLL
You can try the rejection yourself: the demo page has a one-line Docker command.
Two questions I’d value opinions on from people who know this stack:
-
Emitting
.fqdirectly rather than generating Liquid Haskell annotations gave me control over the constraint shape, but it means maintaining my own VC generator. Is there a reason I’ll regret not going through LH? -
I’m pinned to liquid-fixpoint 0.9.6.3.1 on GHC 9.6. What’s the least painful way to keep up as Liquid Haskell and liquid-fixpoint move to newer GHCs?