We could have something similar with full dependent types a la Idris: you could write a proof and search for a function that satisfies it. If such a thing were popular and huge amounts of Idris code were written, you could write only proofs for your program and the Idris system could go download and piece together your program!

That would be very cool, but I'm not sure how much easier it would actually turn out to be. Also to do anything useful you'd probably have to restrict the language to be non-Turing-complete.