Hacker News Reader

I suspect that, given any type system / proof system for correctness, there will be well behaved programs that cannot be proven correct in the proof system, nor can they be refactored to equivalent programs that can be proven correct.

I think perhaps the challenge 'write a doubly linked list in Rust' is an example of this, but I am not sure.

What you say is possible, and my knowledge stops short of it.

I know this is true:

> given any type system / proof system for correctness, there will be well behaved programs that cannot be proven correct in the proof system

But I'm not sure if this is as well:

> nor can they be refactored to equivalent programs that can be proven correct

If so, then there will be some programs whose behavior simply cannot be proven by a type system. Though I wonder if for those programs there could be another type system that could prove it? So maybe with a combination of type systems it can still be achieved?

Either way, what I meant to say was that even for programs that can, the problem of "bugs in a program" has not been completely solved. Since there can be bugs in your proof, and there are often missing assertions in it as well, in that you'll generally prove a property of it, but not directly assert precisely what you expect of each and every inputs, and you might also simply forget to prove certain key properties.

This is essentially Gödel's first incompleteness theorem.

> Type system don't prevent bugs, they help you prove properties

From a certain perspective, I disagree.

If I write a function, let's call it sort. It takes an array of integers and returns an array of integers. I call the function with an array and it so happens that the array returned isn't sorted.

Is there a bug?

I would argue there isn't because the function makes no such statement that the array returned should be sorted, or that it should be a permutation of the input array.

How could any programming language/type system "catch all the bugs" if no statements are made as to what constitutes a bug?

If I create a function in Idris and specify in the type signature that the returned array will be a permutation of the original and that it will be in increasing order, then yes Idris will catch all the bugs.

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.

Is this in a way related to something called "property-based testing"?

Property-based testing is not proof-based, but stochastic; you define the input space for a property fairly well, then the testing framework samples random points within that space. They also generally have reducers, which try to create small failing inputs iteratively after finding one failing input. The difference with fuzzing is mostly that fuzzers are largely black box; the input space is left largely undefined (e.g. AFL: bag of bytes), and the property under test is usually "well, uh, does it explode?". I don't think the popular property-based testing frameworks use instrumentation to guide exploration of the input space.

It is and isn't.

The type system will try to prove that a program will behave in some specific ways without needing to run the program. The "specific ways it behaves" is what I call "properties".

Property based testing will run the program and check as it is running that it behaves in some specific ways.

In the end, they both can be used to demonstrate that some properties of a program execution hold, but they go about it differently.

The type system will use logic over the code semantics and structure to assert that in all possible cases (combination of inputs) the property will hold.

The property based testing will use sampling to assert that in a lot of cases (combination of inputs), the property will hold.

Unless you can sample the entire input range in a property based test, you don't prove that it holds for all inputs, just for a large number of them. While type systems tend to prove for all inputs.

Also generally the type system will take less time to execute its reasoning over the code, than the property based test will take to run its sample set.