As I'm losing my faith in organized peer review, I've decided to take matters in my own hands and I'm doing distributed, post-publication peer-review.
Today's paper is Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler by Simon Henniger, Stephen Chong and Nada Amin.
In a time that people are relying on LLM agents to implement and verify their code, it is natural that people think of implementation source code as the new assembly: it will never be read, just produced by the new compilers, LLMs.
Djinn takes this approach: users only write specifications, and the compiler will write the source code and verify it. This part is not news.
The part that I found interesting that hadn't occurred to me is the unambiguity property of the specification (not the code's). If a specification allows for two implementations that return different values, the specification is wrong. Of course, if two implementations (say quick and merge sort) yield the same results, then the specification is correct and the compiler will produce a working implementation and verify it. If it can, because LLMs produce no guarantees, unlike classical compilers.
The paper then goes on to separate functions, procedures and relations, similarly to how Lean has partial, liquid types have measures and handle monads. These are details that are interesting only to those implementing a similar system, but not crucial to the main idea.
Overall, I think the idea of functional determinism is interesting for a specification. We actually need more techniques to validate the consistency of specifications, since that's how a lot of programming might be done in the near future.
But as someone who has been implementing a language that allows users to only write specifications, I'm not sure we only care about functional correctness, and that mainstream developers will write specifications as opposed to natural language. Despite my language supporting expressing logic-based requirements, examples, tests, property-based testing, and optimization metrics, I'm more and more convinced no one will read them. In the whole Requirements-Archicture-Design-Implementation-Testing/Verification-Validation, I think humans will stay at Requirements and Validation level, and everything else will be automated.
Overall impression: excellent idea of making specification unambiguous as a requirement. I would probably reduce the paper to two pages (intro and Figure 1 focused on the max_is_unambiguous). I don't see much value for the overall audience in the rest of the paper. It can be a technical annex or documentation in the repo for those of us implementing these approaches. Shorter and more focused papers are better and take nothing away from the core idea.