# How useful is program search in the field of programming-language theory?

I've been thinking: computing systems such as the Lambda Calculus and its variations are usually very simple and can be implemented in as few as ~80 lines of Haskell code. There is a self-interpreter for the Binary Lambda Calculus in 210 bits.

Considering PL research mostly consists of the search of similar systems with desirable characteristics (such as being supercompilable, or capable of expressing proofs), and taking in account how information-starved those systems are, wouldn't it be interesting to use automated search techniques such as genetic programming or just breadth-first search to find those?

Has that been tried already?

• Given that Tromp's inefficient self-interpreter already takes 210 bits (i.e. lives in a naive search space of size $2^{210}$), how likely is it that interesting programs can be found by brute force search such as generic algorithms? For example supercompilation techniques today only work on extremely short programs (e.g. < 10 commands). – Martin Berger May 8 '14 at 4:54
• The question is, what is the specification of the program you are looking for? If you have an equational description, then higher-order unification is your friend. In more generality, you might be interested in program synthesis. – cody May 8 '14 at 21:39