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 interesting in its proof (sometimes you are, anyway).

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?

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.

That’s true, but the theorem prover still needs a model of your code to check the theorem against. So how do we know it’s checking the theorems against an accurate model.

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.

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

ALL TESTS ARE GREEN, ALL GOOD.

And then you need to remind that it does not matter, if they are empty.

Oh it gets even stupider. When Claude web introduced the "computer" stuff last year, I had it port an interpreter to a different language. It did it in one shot, I was very impressed.

It even volunteered tests.

Then I read the tests. It was just a bunch of console log statements saying "Test passed!" and didn't actually test anything...