6 ms·

Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude! Now I want to unde

by yuchi 5y ago

Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude! Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs!

reuben364 5y ago
Not qualified to answer, but my thought is that if you have a statement that is true that cannot be proven, you could write a program whose correctness implies the statement, then proving the program correct amounts to proving something that can not be proven.
ashton314 5y ago
Here's a small attempted answer: 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. Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.) 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; https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... [^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- reuben364 5y ago
  I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?
- barrenko 5y ago
  Can I ask in a very "noob" way - are types and theory underneath something that runs in parallel to Turing machine and they together enable modern computing OR is Turing completeness and Turing machine stuff also part of type / lambda calculus theory? Thanks.
  - reuben364 5y ago
    Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs. 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.
- the_french 5y ago
  > Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
  - ashton314 5y ago
    You’re right. My bad. Thanks!
didibus 5y ago
> 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.
shikoba 5y ago
>Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs! You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
- reuben364 5y ago
  A more degenerate argument: a type system that rejects all programs will prevent all bugs.
  - Koshkin 5y ago
    I have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
- ProfHewitt 5y ago
  Theorems of a foundational system are not computationally enumerable (in fact they are not even countable). See the following article: https://papers.ssrn.com/abstract=3603021 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.
  - shikoba 5y ago
    >there are true propositions that cannot be proved 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.
tel 5y ago
It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statements about e, what does the system look like? 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.
jerf 5y ago
It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of complications for computing itself in your type system. There are type systems sufficiently complicated to declare "the type of Turing Machines that halt in a finite amount of time" as a type; this causes obvious problems. 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 https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833 .
ProfHewitt 5y ago
[Gödel 1931] proposed the proposition I’mUnprovable (such 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’mUnprovable. Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because I’mUnprovable:Proposition is a propositional variable in the definition ⊬I’mUnprovable. Consequently, I’mUnprovable:Proposition⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.

by yuchi 5y ago

reuben364 5y ago

Not qualified to answer, but my thought is that if you have a statement that is true that cannot be proven, you could write a program whose correctness implies the statement, then proving the program correct amounts to proving something that can not be proven.

ashton314 5y ago

Here's a small attempted answer: 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. Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.) 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; https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... [^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

reuben364 5y ago
I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?
barrenko 5y ago
Can I ask in a very "noob" way - are types and theory underneath something that runs in parallel to Turing machine and they together enable modern computing OR is Turing completeness and Turing machine stuff also part of type / lambda calculus theory? Thanks.
- reuben364 5y ago
  Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs. 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.
the_french 5y ago
> Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
- ashton314 5y ago
  You’re right. My bad. Thanks!

didibus 5y ago

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

shikoba 5y ago

>Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs! You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.

reuben364 5y ago
A more degenerate argument: a type system that rejects all programs will prevent all bugs.
- Koshkin 5y ago
  I have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
ProfHewitt 5y ago
Theorems of a foundational system are not computationally enumerable (in fact they are not even countable). See the following article: https://papers.ssrn.com/abstract=3603021 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.
- shikoba 5y ago
  >there are true propositions that cannot be proved 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.

tel 5y ago

It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statements about e, what does the system look like? 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.

jerf 5y ago

It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of complications for computing itself in your type system. There are type systems sufficiently complicated to declare "the type of Turing Machines that halt in a finite amount of time" as a type; this causes obvious problems. 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 https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833 .

ProfHewitt 5y ago

[Gödel 1931] proposed the proposition I’mUnprovable (such 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’mUnprovable. Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because I’mUnprovable:Proposition is a propositional variable in the definition ⊬I’mUnprovable. Consequently, I’mUnprovable:Proposition⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.