Why convert C to Rust
C will let a program read and write memory it doesn't own. That single property sits behind thirty years of serious security vulnerabilities: buffer overflows, use-after-free, data races between threads. Rust's compiler refuses to build code that can do those things, and gives up almost nothing in speed to manage it.
The abstract argument is fine. What convinced me were two lines in the original.
The subject was Craft, Michael Fogleman's small open-source voxel game — a Minecraft in miniature, about 5,700 lines of C.
In one place it normalises a vector by handing three separate pointers into the same array to one function. It reads all three values to compute a length, then divides all three by it — correct only while no two of those pointers refer to the same float. Nothing states that requirement and nothing checks it. Pass one address twice and the second division silently operates on a value the first has already changed: no crash, no warning, just geometry that is quietly wrong. Rust will not compile the direct translation, because it cannot prove the three borrows are disjoint.
Elsewhere, a queue entry is declared without initialising its fields, then copied wholesale into a buffer shared with four worker threads. Whatever happened to be on the stack travels into the queue with it. Nothing reads those fields today, because every consumer checks the entry's tag first — but that is a convention, not a mechanism. It also means the queue's contents are not a function of the program's inputs: two identical runs can leave different bytes in it, so inherently unreproducible. In Rust the entry is an enum, and a variant has no spare fields to leave unset.
C compiled both without a word of complaint. That is the case for Rust, in two lines.
I gave away the good part
Writing the Rust was the fun bit — the puzzle a professional would want to keep for themselves. I handed all of it to Claude.
What I kept was the question I actually cared about: how would I know?
A model can produce beautiful, plausible Rust indefinitely. My laptop has no C compiler, no Rust toolchain and no Linux, so it could equally have no idea whether any of that Rust compiled, let alone whether it behaved like the original. An agent that cannot run anything can only assert, and a confident assertion is worse than a blank page.
The machine that made proof possible
This is the gap Islo closes. You ask for a computer — four cores, 8 GB of memory, 20 GB of disk — and a few seconds later there is a microVM. Install anything. Run anything. Delete it.
That bought something better than “the tests pass”. Both programs — original C and new Rust — were made to narrate every value they computed into an enormous log, in the same order and format, every number printed as raw binary rather than a rounded decimal so no real difference could hide behind rounding. Then the two logs were compared character by character.
Getting there meant discovering that GCC fuses multiply-and-add into a single instruction by default and Rust does not, which makes the two legitimately disagree in the final bit. One compiler flag. Found by running it, not by reasoning about it.
(To take the left-hand pictures at all, the thirteen-year-old original had to be given a headless screenshot mode it never had — it draws to a window, forever, with no way to ask it for a single frame on disk. Patching one in, building it and photographing it took a machine that lived for under two minutes.)
Failure got cheap
The full check is a pipeline: run the tests, run the strictest style checker available, render the scenes, confirm the images are not blank, drive 120 frames of the interactive loop, dig a block, place one, light one, write on a sign, grow a tree from a typed command, then cross-compile a Windows executable. About five minutes, start to finish, on a machine that did not exist beforehand.
It ran 31 times. Nineteen of those runs failed.
That is the statistic I would put on the wall. 52% of all the machine time this project used went to runs that failed — and that was the process working properly. One of those failures revealed that the check confirming screenshots were not blank had never worked at all: it was reading each image four bytes past its start, so decompression failed on every picture it had ever been handed, and it had been reporting success by accident. Reasoning about that code would never have caught it. Running it caught it at once.
Compiling a stranger's code
Every one of those runs downloaded source from GitHub and then compiled and executed it. Routine — and, if you stop and think, an odd thing to do on a laptop holding your credentials. In a disposable microVM it is a non-event: the blast radius is a machine about to be thrown away regardless. As agents take on more unattended work, that stops being good hygiene and becomes the precondition.
The bill
42 machines. 192 minutes of compute. At Islo’s 7¢ per core-hour, 4¢ per GB-hour of memory and 0.07¢ per GB-hour of disk:
The other ledger
The compute cost $1.96. The model work behind it came to roughly 494 million tokens — 467.1M for the port itself, across two August sessions, and 27.3M for the token analysis, the screenshot harness and this post.
That headline needs a caveat. 98.9% of it (488.7M) is cache reads, which scale with how deep into a conversation a turn sits rather than how hard that turn was, and which bill at a fraction of the base input rate. Output tokens — 1.29M in total — are the better measure of work done.
Two things fall out of the breakdown. Only about 301M of the 467M (64%) is
attributable to the Rust work at all; the rest belongs to a TypeScript
playbox, some Islo SDK exploration and the c2rust-demo-* jobs
that shared those sessions. And within the Rust work, writing versus
verifying split 41:59 by billed tokens and 51:49 by output — roughly half
the generative effort went to testing and correcting rather than authoring.
The half of this project that felt expensive — thirty-one full verification runs, nineteen failures, ten million characters of differential proof, a cross-compiled Windows build — came to less than a cup of coffee. I would have paid a hundred times that for the same confidence. What I bought, for $1.96 in Islo credits, was the ability to stop guessing.
