If you redefine what others mean to fit your particular point, you will obviously be correct, yet you'll have failed to be correct to the intended meaning used by other people.

Using your definition of bug, take for example a function in an untyped language. Assuming a bug free implementation of the language, I can say that no matter what code I write, it will always be bug free, because the code will always do exactly what the code specifies, and the function made no statement to any particular behavior.

So if you define your "sort" to be a function that does what your Idris type specification defined it to do, yes your sort will be correct to it, assuming a bug free implementation of Idris and its type system, and that the type checker asserted it to be correct.

And yet, for the intended behavior to the users of the program and the objective it was meant to achieve it's very possible that your sort function doesn't work.

Or in other words take this Python code:

    def sort(array):
      return array

    print(sort([2,1,3]))
    [2,1,3]

Is this a bug? Or did I just mislabel the name of this function?

I feel like that's the gist of your argument. You're saying: it behaved correctly to the extent that I have formally specified it, which in the case of Python I have not formally specified anything so all behavior are valid and correct.

But what good is that?

As good as you can get without being able the read the programmer's brain to figure out what they really wanted in the first place. To talk about correctness formally in the first place, you need to specify what you want and when you do that there is no guarantee that that is actually what you want.

In Python, a function named "sort" could take an array and return an integer. Or None. Or crash. So knowing that it returns an array of integers is an improvement over the untyped case.

Types like "returns an array" or Java's checked exceptions are attempts at narrowing the possible behaviors from a function.

Though if you allow duplicates, that should be non-decreasing order instead of increasing order?

I think the argument of OP would be that this wouldn't be a bug, because Idris has proved increasing order, which means that if the function allowed duplicate that could result in non-increasing order Idris type checker would have told you your function is incorrect.

Basically, the proof is the spec, and a bug is defined as "not behaving as defined by the spec".

And assuming Idris is itself bug free in its language implementation and type checker implementation and is powerful enough to prove your given spec, then OP says your function is guaranteed bug free.

The difference is that he defines bug as:

> When the function behaves outside what Idris has proven.

While I think most people define a bug as:

> Doesn't do what it should have to provide the correct intended user behavior.