←back to thread

Type checking is a symptom, not a solution

(programmingsimplicity.substack.com)
67 points mpweiher | 1 comments | | HN request time: 0s | source
Show context
guerrilla ◴[] No.45141819[source]
This is silly. Types are specifications of programs and data. The only reason that isn't obvious is because most of our type systems are rudimentary. It becomes obvious once you pick up anything with a bit more power (Haskell with extensions or any dependently typed programming languages). A type system is not just another ad-hoc solution, it's fundamental and essential to what we're doing. This is obvious if you know the (pre-computer) history of type theory: Types specify sets of objects intensionally. Types describe what our program should do and are also a very clear form of documentation. On top of that, you can't even get rid of types if you wanted. The best you can do is make them implicit. You have to make a decision about how to interpret data in the end, and that's typing. Even assembly language and machine code has types. Even electronics have types, we just don't think of it that way (but look at the 7400-series ICs if you want explicit examples).

This post is written by someone rather naive of computer science. Their description of a "function" betrays that. The failure to recognize UNIX pipelines as function composition also betrays that and so does the whole "black boxes" paragraph.

replies(4): >>45142293 #>>45142585 #>>45142633 #>>45142905 #
motorest ◴[] No.45142293[source]
> This is silly.

Yes, the article is deeply unserious and perhaps even in "not even wrong" territory. The poor blogger tried to put up a strawman on how type checking was a cognitive load issue, completely ignoring how interfaces matter and comply with them is a necessary condition for robust bug-free code.

replies(2): >>45142532 #>>45142635 #
kace91 ◴[] No.45142532[source]
Sorry if this is off topic, I have a language-related question:

Over the last year I’ve seen people on the internet using “unserious” as an adjective to criticize people. Is it just an expression that became common, a frequent literal translation from another native language…?

Not at all judging, I am not a native speaker and I never saw the word used that way before, but this is the kind of question that’s pretty much impossible to get an answer for without a direct question.

replies(2): >>45142581 #>>45142696 #
1. guerrilla ◴[] No.45142696{3}[source]
It's an old word from the 1650s, just becoming more popular now for zeitgeist reasons. https://www.etymonline.com/search?q=unserious