Interesting experience and perhaps not entirely surprising given that type-hole driven development was already a thing prior to LLMs. Like how many ways are there to implement "[a] -> [b] -> [(a,b)]", let alone when you provide a vague description of what that is supposed to do.

minikanren folks were already experimenting with program synthesis given a test suite that needs to be fully satisfied.