Wait a minute! What the hell is ‘automatic program search’? Is it like with Malbolge where the first working programs had to be written through brute-force search?
You define some test-unit cases, input-output pair.
You define some elementary blocks like in scratch (Blockly). And you try to randomly assemble the blocks so that they respect the type constraints. And you score your program based on the number of test case it got right.
For this simple problem, naive random search was all that was needed. (less than 100k programs evaluations)
But for more advanced cases you could use something like Genetic Programming with Koza's Automatically Defined Functions where you build an intermediate library of useful blocks.
Now one would use deep learning and produce source code directly with some tool like Copilot and run it until it passes all tests. Or if you want to get your hands dirty, you can re-implement the old school methods and use a neural network to make the pick decisions instead of a random pick.
Once you have programs that pass all test cases, you can try to prove correctness (that's more something like HOL-Light would do) and whether or not they are equivalent (and equivalent to a formal specification) and optimize them further by transforming the program.
