Ah, but if you have specifications, you should have the ability to generate unlimited numbers of tests. Handpicked examples aren't needed. The great advance in testing with increase in compute power was the realization that carefully handcrafted tests are silly; just blast huge amounts of randomness at the system and use cheap compute to save expensive human effort.

I think it's a common experience to implement some well-defined data structure or algorithm and use the clear specification of its behavior to randomly test it, to then discover this flushes out all the bugs.

It sounds like you're asking something nebulous, like does it have a soul.

Mass generation of conjectures and proofs/disproofs could AI to discover objectively mathematically useful things. For example, it might discover shortcuts, lemmas, even abstractions that are useful in the proofs of these things -- and judge that utility by how much they improve the ability of the AI to prove things in this mass of problems. It wouldn't say whether the things are useful for non-mathematical human problems, but then human mathematicians, as you say, can't really judge that either.

Or maybe this is just a thin veneer over anti-techbro antipathy.

If destroying a book is such an evil, then isn't not printing a book also a huge net negative? Are you going to call on publishers to make endless print runs to churn out books that then get warehoused? I mean, if these lumps of cellulose are such inherently valuable objects, wouldn't we create endless value by piling up the unread copies?

Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).

It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.

The problem here is that more compute also helps testing. So it's not clear verification will pull ahead over just doing more testing, especially if there's any manual part of the verification workflow. The bugs that remain after testing become more and more difficult to stimulate.

> That's a test for the test suite - you make some random change to the program and see if the test suite catches it. Fuzzing is related to that concept.

Mutation testing is kind of orthogonal to random input testing or fuzzing. In fact, one can use the latter to automatically kill mutants in the former, which is very useful in automatically constructing enhanced test suites. You still need to determine what the correct behavior is for each new test input.

No it isn't.

> execution of a Turing machine can't be expressed as a Gödel number

Yes it can.

Proofs also enable AIs to direct search and generate knowledge. Verifiability is immensely useful for keeping AI grounded.

One might imagine AI generating enormous numbers of hypotheses and then trying to prove or disprove them, and then mine that data for new abstractions and heuristics.

Books are lumps of cellulose carrying information. Destruction of excess copies is no more outrageous than discarding excess packets off the internet.

> Gödel number encodes a paradox

WTF do you mean by this?

An additional related theorem is Rogers' recursion theorem, which is how we get programs that, when run, print their own source code (by the theorem this can be done in any Turing complete programming language.)

If there's more than one implementation, there better be a standard, and it's risky to assume any behavior not specified in the standard will be shared by all implementations.

Even with one-implementation languages it becomes risky to assume behaviors will remain the same as the implementation evolves.

But I'm not doing that -- I'm saying it's a possibility that is consistent with evidence.

The claim that life is common is different. For that, you really need to present an argument that life being uncommon is ruled out.

In your last sentence there you've retreated from "life is common" to "it's plausible life is common". Sure (within the constraints of the Fermi Argument, but that has uncertainties.)