For fuck's sake. > For instance, it's impossible to write an executable program in Java that adds a string to a number. Wrong [0] and misleading and not a rea

For fuck's sake. > For instance, it's impossible to write an executable program in Java that adds a string to a number. Wrong [0] and misleading and not a reasonable summary of type-driven development. The article goes rapidly downhill from there. It tastes like an undergrad who has just learned about the very basics of things and is still trying to figure out how to put them all together. > So it is possible to statically verify that a function always returns the square of its input, it just needs a proof (aka its type). This is not sufficiently convincing. What exactly was that type, and which language was it written in? The type "int -> int" is not at all enough. This sort of handwaving logic seems to come up constantly with folks new to type theory. And each time it comes up, it seems that a massive argument must happen [1] in which folks who actually understand type theory have to remind folks that no, type systems do not automatically save us. Here are two analogies in the article. "I'm lying" is a reference to a famous paradox [2], and the barber story is a truncated part of an older set of stories told by Russell, Gardner, Smullyan, and others [3]. All fine and well. However, they then try to claim that types somehow fix the underlying paradoxes, but of course, they don't. This is because the underlying cause of the paradoxes is of course Gödel's first incompleteness, which works even in statically-typed environments [4]. Worse, the article author makes it sound like incompleteness is some barrier to be climbed over, when in fact it is a basic (if tough-to-prove) categorical property [5]. [0] https://hackernoon.com/java-is-unsound-28c84cb2b3f https://hackernoon.com/java-is-unsound-28c84cb2b3f [1] https://lobste.rs/s/yyhu4w/real_problems_with_functional_languages#c_4pbkan https://lobste.rs/s/yyhu4w/real_problems_with_functional_lan... [2] https://en.wikipedia.org/wiki/Liar_paradox https://en.wikipedia.org/wiki/Liar_paradox [3] https://en.wikipedia.org/wiki/Barber_paradox https://en.wikipedia.org/wiki/Barber_paradox [4] http://r6.ca/Goedel/goedel1.html http://r6.ca/Goedel/goedel1.html [5] https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore...