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.
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.
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.
Types like "returns an array" or Java's checked exceptions are attempts at narrowing the possible behaviors from a function.
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.
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]
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?
I think perhaps the challenge 'write a doubly linked list in Rust' is an example of this, but I am not sure.
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.
Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type.
From the Wikipedia article under "General Observations":
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization.
Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete.
Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem)
[^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-curren...
[^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Thanks.
One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus.
Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.
Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
It is a well-known phenomenon that it can take surprisingly little to turn a computation system Turing complete; witness, for instance, C++'s accidentally-Turing-complete templates. So it can wiggle in without you even realizing it at design time. Or, if you're using a type system with sufficient power like dependent types, it is surprisingly easy to put together four or five recursive types that, on their own, are all perfectly computable, but together turn out to create something that is Turing complete. Write a program with a few hundred of these and Turing completeness is almost bound to sneak in somewhere.
See https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 .
It turns out that if you have that system in code written as s and then try to assert certain properties of it G, then it’s possible to design G such that s: G is so twisty and self-referential that it can’t be verified. Something to that effect: strong logics have a tough time speaking completely about themselves.
So that’s at least one property for one program that’s unprovable no matter how powerful our type system is.
But that’s so long range. Practically we can make type systems that let us prove massive amounts of things using judgements like e: B. The real issue is that it’s just very hard and expensive to make those systems practically eliminate even a small subset of bugs.
You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
enumerable (in fact they are not even countable). See the following article:
https://papers.ssrn.com/abstract=3603021
In a foundational system, there are true propositions that
cannot be proved. For example, is true but unprovable that
an algorithm can enumerate the theorems of an order
abstracted from strings.
In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.
that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential
undecidability of Russel’s foundational theory, which had the
type-restriction on orders of propositions to prevent
inconsistencies. I’mUnprovable cannot be constructed in
foundational theories because strong types prevent
construction of I’mUnprovable using the following recursive
definition (see Diagonal Lemma [Gödel 1931]):
I’mUnprovable:Proposition<i>≡⊬I’mUnprovable.
Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because
I’mUnprovable:Proposition<i> is a propositional variable in
the definition ⊬I’mUnprovable. Consequently,
I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1>,
which is a contradiction.