SOURCE-LINKED INTELLIGENCE

Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler

arXiv · AI, language, vision and robotics · article · Sep 21, 2026 · UTC

Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the new programming languages. We argue that an unambiguity constraint is key: in addition to proving that its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying it must produce the same outputs on the same inputs, i.e. that the relation formed by the constraints is deterministic. This leaves the LLM no leeway on program semantics: as with a conventional compiler, t

Read original source ↗ Open in workspace

recordType

paper

region

Global