5 ms·

> Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs I think the article has this

> Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs I think the article has this a little wrong. The theorem in programming terms I think simply means that there are some programs for which another program can't prove certain properties. But in theory you can restrict yourself to writing programs that can be proven completely. Even then though, you won't eliminate all bugs, and I think that's the part the article gets wrong. Type system don't prevent bugs, they help you prove properties, but the programmer still needs to come up with all properties and edge cases themselves and set things up for the type system to prove those, and there's a lot of opportunity for the programmer to forget about a lot of properties or to have a bug in how they're trying to prove it. Finally, there are only so much you can prove in a general way, in that there are only so many properties you can try to prove. Just think about it, you can't go listing all possible inputs and asserting all possible outputs because as a programmer that would take way too long. So you try to come up with shortcuts, which will be properties, maybe you say alright so for even inputs I'd expect even outputs. Now maybe you use a type system to prove that. But you can still see how you've not proven that it returns the right output for every single input, just the property that even should return even. And that still leaves gaps for bugs. But none of those have anything to do with Godel's incompleteness theorem, those exist even if you restrict yourself to programming only in a language for which type systems can fully operate in. Disclaimer: I'm no expert in this though.

barrenko 5y ago
Is this in a way related to something called "property-based testing"?
- formerly_proven 5y ago
  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.
- didibus 5y ago
  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.
davidgrenier 5y ago
> 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.
- MichaelBurge 5y ago
  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.
- jdmichal 5y ago
  Though if you allow duplicates, that should be non-decreasing order instead of increasing order?
  - didibus 5y ago
    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.
rocqua 5y ago
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.
- didibus 5y ago
  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.
- coldacid 5y ago
  This is essentially Gödel's first incompleteness theorem.

barrenko 5y ago

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

formerly_proven 5y ago
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.
didibus 5y ago
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.

davidgrenier 5y ago

> 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.

MichaelBurge 5y ago
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.
jdmichal 5y ago
Though if you allow duplicates, that should be non-decreasing order instead of increasing order?
- didibus 5y ago
  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.

rocqua 5y ago

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.

didibus 5y ago
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.
coldacid 5y ago
This is essentially Gödel's first incompleteness theorem.