The issue here is that function definition doesn't tell what the function does. So you may have hundred implementations of sorting algorithms in different libra

The issue here is that function definition doesn't tell what the function does. So you may have hundred implementations of sorting algorithms in different libraries, and neither compiler nor the IDE know that they all do the same thing. So when you write sort(myCollection) you are still referring to one particular set of instructions. The system parent poster envisions (the way I understand it) would be along those lines: * User gives SPECIFICATION of sort, along the lines OP writes about in his blog. * Other contributors provide various implementations which satisfy the specification. Such system would either have to auto-prove that implementation meets specification or just trust contributors that it does. * Then in your code you can write sort(myCollection) and the system would pick the best implementation.