Finding a Proof of the Turing-completeness of Burro

A good way to prove that a language (let's call it L) is Turing-complete is to write a Turing-machine-to-L compiler, and then show the compiler is correct. Writing the compiler is straightforward if L is a "normal" language, but if L has pathologies or is otherwise "weird", the compiler can become very gnarly, as it needs to translate the workings of the Turing machine to something equivalent in L.

Some things can help. For example, the compiler doesn't strictly have to take Turing machines as its input; it can take any language that has already been proven Turing-complete. But even in the best conditions, writing the compiler can easily become a debugging exercise on some terribly fiddly code.

And this is where I have been with Burro. For a good long while, I've been pretty sure (but not 100% sure) that Burro is Turing-complete, and I've been trying, on and off, to write a proof of that fact.

Many artifacts that attest to this can be found laying around this repository. I worked out a re-usable idiom for conditionals, and a simplified language (called Kondey) which is basically Burro with syntactic sugar for that idiom.

But even with those, the details of the translation have been so fiddly, it's been hard to stick to it. I had only a partially-completed, and incorrect, compiler from Turing machines to Kondey, to show for my efforts.

But you know what's good at debugging fiddly, partially-completed, incorrect code?

Agentic coding tools.

So, as an experiment, in summer 2026, I asked Claude Code to "do a breakthrough" (as it were; not using those precise words) and find a proof. That is, to debug my compiler.

It took it a few tries. (Claude Code crashed a few times.) But in the end, it did it. It produced a proof that Burro is Turing-complete.

The compiler is in Language.Burro.TCProof.TM2Kondey. Claude also wrote a document about The Turing-completeness of Burro.md, and a very trying-to-be-helpful guide that explains How the Turmac-to-Kondey Backend Works.md.

Now you may well ask, how do I know it produced a valid proof. Actually, that is what you should ask.

If the proof was just prose, I wouldn't trust it. Claude did generate a bunch of extremely dense and jargon-y prose - I can barely follow it. I would need to study it for a long time, if I wanted to assure myself that it makes sense and there are no holes in it.

But the thing about having a compiler written in an implemented programming language is that you can run it and test it.

Now, a test is not a proof, but en masse, casting a wide net, they raise confidence that the code is not wrong. This is the idea behind "property testing".

And I have been able to run the compiler on a large number of randomly- constructed Turing machine, and compare the execution of the resulting Burro program to the execution of the Turing machine, using a "bisimulator" that compares the execution step-by-step, so that it doesn't require that the Turing machine be one that necessarily halts.

And the initial explorations with this bisimulator did expose bugs in the translation, which prompted Opus 4.8 to introduce fixes, which did remedy those observed mismatches.

And intentionally introducing a flaw in the compiler does cause the bisimulator to report mismatches.

Taken together, this makes a very persuasive empirical case that the compiler is correct.

Note

The parts of the reference implementation that were generated by Claude are conditionally compiled in. If you want to build a version of the burro binary without them, you can pass --disable-claude-proof to ./build.sh (and in this case you should also pass it to ./test.sh.) This allows you to build a binary that is uncontroversially open-source, under the BSD license, avoiding any questions about how Claude's output should affect the license.

Questions

Why did Claude Code crash? The desktop I was doing this on is woefully underpowered, and I believe it was because Claude kept trying to test its changes by generating Busy Beaver machines. I had to tell it to avoid doing that.

Is this cheating? That's a strong word. I think of it this way: it does suck all the fun out of it, but really, not many people find this kind of intricate fiddly programming all that fun in the first place. It's not like esolangers were racing to find a Turing-completeness proof for Burro before this happened. Afterwards, perhaps there is a deflated sense of the mystery simply having evaporated. But this is balanced by a sense of curiosity satisfied (see, I knew it was Turing-complete!)

What can we learn from this? Perhaps that there are uses for Claude Code other than just generating code. Agentic coding is a bit like evolutionary programming, where the "fitness function" is the tests - that is, the specification made mechanically checkable. The distance between generating code and formulating a machine-checkable proof is not great, and this seems like a good "off-label use" of agentic coding. And if proving an esolang Turing-complete is this easy for a modern generative AI tool, maybe we should be aiming higher, and trying to get them to prove harder open problems. To date, some long-standing (but maybe not hugely famous) conjectures have had counter-examples found for them by generative AI tools. This is a good fit, from the "evolutionary programming" perspective: checking if the counter-example is valid is the fitness function, and you just keep going until you find one. But the other direction is more difficult; you need to show that there are no counter-examples. The Burro TC proof is in this category. The property-testing-type bisimulation demonstration, buttressing a proof in prose, might work in this instance; if we wanted something rock-solid, we'd probably want to formalize the proof in Rocq or Lean. But a generative AI coding assistant can help do that too! Maybe the only thing missing right now, is finding more problems that are just the right level of hardness and unsolvedness to sic agents on.