nemo1618

That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).

In essence this lets you verify any property you want for a given function, as long as it can be expressed as a fuzz test. Specifically, you can express your property with an assert, and then prove that it never fires. This is nice because it keeps everything in one language, rather than having to translate the whole program into Rocq and then express your desired property as a Rocq theorem.

I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.

Thank you for the kind words! It's funny how much staying power those blog posts have, haha. Michael has some arcane ability to consistently hit the front page of HN.

True, I expect models to be pretty correlated with each other as well. But you can at least attempt to quantify that correlation in a rigorous way, by running experiments (e.g. by pointing each model at a big project and comparing the sets of bugs they each find).

And yeah, the "double-edged sword" aspect of determinism is definitely the biggest bullet that you have to bite. For me, it's better than the alternative; without determinism, such jailbreaking attacks are still possible, just harder to detect. But I certainly would not want people to go around thinking "it's deterministic, therefore it's safe."

True, you can't do this with GPT or Claude, at least not today. But you can do it with a local model: vLLM supports deterministic inference out of the box! (If you have a MacBook, you can confirm this yourself; just point your agent of choice at the site. It will download a small open model and run it with vLLM Metal.)

Naturally, I hope that OpenAI and Anthropic will one day offer deterministic inference; see the "Weights" page for what this might look like.

I had a similar idea for Super Smash Bros Melee! There is a lot of very low-quality footage out there; surely you could train some sort of model to convert it to Slippi replays. A year or two ago this would have been a grad student project; a year or two from now, it will be a one-shot prompt.

Even at Burning Man, in the middle of the desert, there is a camp that hosts a StarCraft tournament every year (on the dustiest setups you've ever seen!) :)

Your assumption is mistaken (and a little rude).

I love programming. It's in my blood: my father and grandfather were programmers too. I have written everything from SIMD assembly to Hoon, and implemented several languages of my own. Believe me, I am intimately familiar with the phenomenon you are describing.

It's true, the devil is in the details. And I will grudgingly concede that, at present, humans are better at exorcising demons than AI. But I see no reason to believe that this will remain true. The gap is narrowing rapidly, and even today there are types of demons that AI can dispatch much more quickly and effectively than you or I can. The fact that vibe coding is possible at all (and that people are willing to pay for vibe-coded apps) is proof that an informal English prompt is sufficient to specify software to an acceptable degree. Not acceptable to everyone, naturally, but at least to the creator and the users.

I am not exactly happy about this. It is bittersweet. Much of my identity is bound up in being a programmer. The devil is in the details; but joy and whimsy and great beauty are in the details as well. For a glorious few decades, one could be an artist under the guise of producing economic value. Now, the economic aspect of producing software is being siphoned off, to be done by machines, leaving only the art. I think we will suffer for that, somewhat. But it is a small price to pay.

I am quite tired of this take, frankly. The implication is that if we continue iterating on prompt optimization, we're going to reinvent what, JavaScript? BASIC? Lisp?

English is not a programming language. Yet English is sufficient to communicate requirements to the degree that we actually care about. A programmer's job is to translate English into lower-level machine language. Necessary to this process is "filling in the gaps" -- that is, extrapolating the expressed intent to cover all the little details that were left unspecified. This system works because humans are at least minimally competent at predicting the preferences of other humans. If your prediction turns out to be wrong, you get feedback and iterate.

Well, guess what. LLMs are also competent at predicting the preferences of humans. LLMs can "fill in the gaps" like no one's business. LLMs can iterate on requirements like no one's business.

Product managers do not speak to programmers in a language that encodes exact requirements, and yet working software somehow gets shipped anyway. LLMs do not need exact requirements either.

After Christmas this year, I removed the tree from our living room, and in the process of being moved, it shed of needles everywhere. I swept them up, but I missed a few areas on my first pass. So I did a second pass, but when I looked again, I saw there were still a handful left. It struck me how removing >99% of the needles was nowhere near acceptable! Lots of cleaning jobs are like this, I suppose, because even a tiny mess can be visually distinct. In fact, as you approach 100%, the remaining mess stands out more.

I would love a crank-powered router. Would be a good way to curb internet addiction!