Earlier this year I was doing some major refactors of an old project. At the time coding agents were really taking off where you could increasingly trust them for more autonomous work, so I was excited to give it a go.

It did the refactor, running for several hours, and ended up volunteering an extensive test suite as well. All tests green!

I was very impressed, until I squinted a little. It had implemented the whole thing backwards, in a way which was not only pointless (didn't achieve any of the stated goals) but actually made things worse than before!

Until that moment I'd been quite bullish about the potential of formal verification in the AI age. But upon seeing that mess, I realized, it might as well have written me a mathematical proof for the code it wrote, and the proof would have passed, and the code would still be wrong!

▲

auggierose 2 hours ago | parent | next [-]

Because, people keep confusing proofs with theorems. The proof can be correct, while the theorem is the wrong one. And if you got the wrong theorem, you might not be interested in its proof (sometimes you are, anyway).

▲

hedora 2 hours ago | parent [-]

This.

Now, write a theorem describing a non-trivial piece of software. Is your theorem longer or shorter than the source code? Easier or harder to read?

	▲	miloignis an hour ago \| parent \| next [-]
		The nice thing is that a theorem doesn't have to completely describe the software, it can just describe some property you care about. Say, no crashes, no dead or livelocks, O(n log n) in the size of the input, same number of instructions executed & memory accessed no matter what the encryption key is, etc etc. These type of theorems are significantly smaller than the source code, pretty re-usable across different applications, and extremely useful properties.
	▲	konart 44 minutes ago \| parent \| prev [-]
		Well, property tests exist and in some cases they are better soslution than other types of test. Obviously you don't write "a theorem" describing a big piece, but just a fuinction, for example. Say you have a function that takes in 3 Points (x,y coords) and returns a Triangle (T) object. Than you can have a property test that will confirm that T is actually a triangle and not something else.

▲

mkoryak an hour ago | parent | prev [-]

This is why I think tests are useless if written by AI. They will always pass and look reasonable.