A computer science paper has Claude writing production Dart code from formal logic specifications — and the researchers say it works.
The paper introduces two new formal systems derived from an existing concurrent logic programming language called Grassroots Logic Programs (GLP). The first, dGLP, is a deterministic counterpart of cGLP, the language's concurrent semantics. The second, madGLP, is derived from maGLP — the multiagent semantics — and restricts agents to communicate only through asynchronous message passing rather than shared variables. Both are proven correct against their abstract counterparts. The authors also prove that madGLP satisfies the "grassroots" property, a decentralization criterion built into the language's design.
The practical hook is an AI-driven implementation pipeline the authors call "math → informal spec → Dart." Starting from dGLP, Claude produced a workstation-based GLP interpreter in Dart. Work is now underway to build a smartphone-based multiagent system from madGLP. The paper positions this as evidence that a sufficiently precise formal spec can serve as a reliable bridge to a working implementation — one that a language model can traverse without hand-holding at every step.
That's a meaningful claim if it holds up at scale, but the paper is careful not to overclaim: the Dart work is described as ongoing, not finished. The distinction between maGLP (the abstract multiagent semantics) and its deterministic derivative madGLP matters here — conflating them would misrepresent the paper's core contribution, which is precisely the derivation and correctness proof of these stricter variants. Whether Claude-as-compiler generalizes beyond a single research codebase remains an open question.