Comment by archibaldJ

This can be solved when the ARC puzzle is cracked (https://arcprize.org/play) so we can automate correctness-checking like in coq but for program synthesis.