How i would like to program:

Be able to create function specifications that completely describes the relationship between it's input and output.

function sort
Input: List of a
Output: List of a

Relationship:
- output's list must be sorted (not enough, [] is sorted)
- every a in input must be in the output's list (not enough, we might have duplicated elements)
in the same number as they appear in the input's list

That would be great... Now anyone could invent yet another sorting algorithm and prove it to follow these rules.

Btw, the function signature should make the compiler check if the specification makes it really a function, not a relationship or a partial function.