[andoando]

Ive been thinking about something like this. A mathematical definition of a function such that we can search it. Imagine we had something like "Find a function that fits this signature -> Input arr[numbers] out-> for every x in arr, x2>x1.

[lupire]

That's https://hoogle.haskell.org/ plus dependent types (data constraints).

Without human provided dependent typing, the search engine would be almost as hard to write as a system to directly generate the code you need.