Completely agree on the importance of the harness.

The problem I see is the same problem Evolutionary Algorithms had: you can generate potential solutions until you run out of cash, but you still need to evalulate those solutions. You need a fitness function, and that means you need to at least know the general shape of the solution. If anyone knows of any work towards more open-ended fitness functions, I'd love to read it.

Seems to a layperson like myself that in Math they're using Lean and in programming contexts they're using compilers, such that the models themselves tend towards embedding that determinism "intuitively".