>no tests?

Earlier this week my slopservant implemented several comprehensive changes to a codebase.

It also wrote extensive tests to verify the correctness of the changes.

A few days later I was working on something else and realized, everything had been implemented backwards, in a way that was nonsensical and also completely pointless.

The many tests it had written were just confirming the LLM's idea of correctness, which turned out to be... completely incorrect.

I laughed when I realized, if I had been using Rust, or indeed, formal verification, that wouldn't have helped at all — it would have just written a mathematical proof, proving the correctness of the wrong thing!

Not sure what lesson to take from that (except read the damn diffs, obviously — it was a hobby project okay ;), but it seems like the more reliable this stuff gets, the more we expect it to work properly, the more risky it becomes.

https://en.wikipedia.org/wiki/Normalization_of_deviance

The solution is a skill that explains to the LLM, with a fresh context, to NOT read source files, and to only use XYZ tooling to extract documentation and function signatures, etc. without implementation details.

Then it can write tests based on the interface, and that is usually a lot more solid.

I'm struggling with this on a hobby project now. I'm torn between continuing the fast pace of development and taking a pause and checking the entire codebase.

The more features I add now will likely make the inevitable refactor much harder, but adding new features is so easy that I want want extend this illusion of productivity just a little bit longer!

> if I had been using Rust, or indeed, formal verification, that wouldn't have helped at all — it would have just written a mathematical proof, proving the correctness of the wrong thing!

This is a well-known issue in formal methods, often referred to as the "formalization gap". It's pretty much an intractable problem, i.e. all we can do is manage it, not solve it.

In fact this issue exists in many fields, often under the name "specification gap" or "specification problem". You'll find versions of that discussed inv economics, architecture (of buildings, not software), etc. In architecture and construction, a high percentage of mistakes that result in lawsuits turn out to be due not to construction, but to specifications that were incorrect in some way.

The bottom line is that there's no perfect formal/mathematical way to go from intent to proof.

write the tests yourself. Or at least the sketch of the test (to get filled in later). Make a commit of what you do so you can then look at the changes.

If you write the tests the agents have an easier time writing the code!

The lesson is: write your own code, it's not that hard.