You Should Specify Your Code Unambiguously (and Prove That You Did)

I have a program that grants wishes, as long as I can state them precisely. Instead of implementing a Rust function, I describe what it should do, and the Djinn writes code that provably does exactly that. Suppose I want to sort a list. I write: djinn! { pub fn sort(v: &[i32]) -> r: Vec { // My sorted list is the same length… v.len() == r.len(); // … and it contains all the same elements … for x in v { v.iter().filter(|y| y == x).count() == r.iter().filter(|y| y == x).count(); } // … and it is sorted! for i in 0..r.len() - 1 { r[i] } } No sorting algorithm. Just explaining what I am looking for. My Djinn is not magic, but it is the manifestation of a dream. People have wanted something like this for a long time: humans write specifications, then have LLMs implement them and prove to a verifier that their implementations are correct. In theory, this LLM-verifier combination is powerful (thanks to the LLM), but still safe and reliable so you don't need to read the resulting code (thanks to the verifier). In practice, it's a bit harder than it sounds. While the verifier provides certainty that the LLM's code matches our specification, it’s easy to make specification errors or underspecify. Also, you have to set up verification software (and establish trust boundaries), juggle different languages, and babysit agents. For this to land, it needs to be tractable for normal SWEs, and currently, it’s a pain even for formal methods experts. What if there was an easy way for everyone t…