<story><title>Where do type systems come from? (2017)</title><url>http://blog.felipe.rs/2017/07/07/where-do-type-systems-come-from</url></story><parent_chain><item><author>yuchi</author><text>Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude!&lt;p&gt;Now I want to understand in a similar fashion &lt;i&gt;why&lt;/i&gt; the incompleteness theorem makes type systems incapable of preventing all bugs!</text></item></parent_chain><comment><author>didibus</author><text>&amp;gt; Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs&lt;p&gt;I think the article has this a little wrong.&lt;p&gt;The theorem in programming terms I think simply means that there are some programs for which another program can&amp;#x27;t prove certain properties.&lt;p&gt;But in theory you can restrict yourself to writing programs that can be proven completely.&lt;p&gt;Even then though, you won&amp;#x27;t eliminate all bugs, and I think that&amp;#x27;s the part the article gets wrong.&lt;p&gt;Type system don&amp;#x27;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&amp;#x27;s a lot of opportunity for the programmer to forget about a lot of properties or to have a bug in how they&amp;#x27;re trying to prove it.&lt;p&gt;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.&lt;p&gt;Just think about it, you can&amp;#x27;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&amp;#x27;d expect even outputs. Now maybe you use a type system to prove that. But you can still see how you&amp;#x27;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.&lt;p&gt;But none of those have anything to do with Godel&amp;#x27;s incompleteness theorem, those exist even if you restrict yourself to programming only in a language for which type systems can fully operate in.&lt;p&gt;Disclaimer: I&amp;#x27;m no expert in this though.</text></comment>
<story><title>Where do type systems come from? (2017)</title><url>http://blog.felipe.rs/2017/07/07/where-do-type-systems-come-from</url></story><parent_chain><item><author>yuchi</author><text>Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude!&lt;p&gt;Now I want to understand in a similar fashion &lt;i&gt;why&lt;/i&gt; the incompleteness theorem makes type systems incapable of preventing all bugs!</text></item></parent_chain><comment><author>reuben364</author><text>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.</text></comment>