Type checking is a symptom, not a solution

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.

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

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.

It's not a literal translation from another language. It's just a word that's taken off in popularity, presumably in response to the rising trend of anti-intellectualism.

> Types are specifications of programs and data. The only reason that isn't obvious is because most of our type systems are rudimentary.

One major limitation of almost all type systems: they fail to distinguish logical types from representation.

Exactly. Types are the theorems, programs are the proof. So types are necessarily linked to programs. I think the author in the article has a misunderstanding of what types are

Agreed. The article makes many references to how life would be better with explicit well-defined interfaces… but types are how we explicitly define interfaces.

For example, Rust borrow checking isn’t to add complexity, it is to make it possible to explicitly define lifetime bounds in interfaces.

It's an old word from the 1650s, just becoming more popular now for zeitgeist reasons. https://www.etymonline.com/search?q=unserious

The word ‘serious’ has several meanings, depending on what it’s used to describe. As a result it has a bunch of opposites: frivolous, funny, non-life-threatening…

When we are grading a person’s argument or their approach to a topic for seriousness, none of those seem to capture the sort of opposite we need. And that’s where ‘unserious’ comes up. How seriously should we take this? Is it serious or unserious?

I’m not sure why there would be a relatively recent surge in its use. Etymonline cites ‘unserious’ as having 17th century origins. Ngram shows increasing usage in the modern era but starting from the 1950s onwards.

If anything it probably reflects an increased use of ‘serious’ in the context of discussing intellectual opinions, as opposed to ‘consequences’ or ‘demeanor’ or ‘injury’ – which if anything is a reflection of increased public engagement with intellectual pursuits.

> Even assembly language and machine code has types.

I agree with the overall thrust of your argument, but on this specifically what's noticeable in an assembly language is that data doesn't have types, the operations are typed. That's usually not really a thing in programming languages. It does happen, but it's not common.

For example Rust's Wrapping<i8> is a distinct type from Saturating<i8>, and if we've got variables named foo and bar with the value 100 in them, if foo and bar have the type Wrapping<i8> the addition operation means the answer is -56 but for Saturating<i8> the exact same addition operation gets you 127

In assembly or machine code there's be Wrapping addition, and Saturating addition and they'd both work on integers, which don't themselves inherently care.

To clarify, I mostly see it in political comments, as in “trump is deeply unserious as a president” (substitute trump for whoever the poster dislikes).

That’s what weirded me, without context it sounds too literary for random internet comments, but my gut feeling in a second language isn’t really worth much.

No, the data is typed; it's just not type checked.

I don't buy it. Go look at the Godbolt assembly output when you write software with some floating point constants on a modern CPU. The assembly has no floating point constants, because why would it, the data doesn't have a type, those constants are just emitted as integers, because they're the same thing.

The 32-bit integer 0x3f000000 is literally the same thing as the 32-bit floating point value 0.5

Types are not data formats.

Sure, but what I'm getting at is that RAX does not have a type

If we write that Quake 3 "fast" inverse square root, the machine code does not have any casting or type changes, but the C does and the Rust does, because in machine code the operations were typed but in these high level languages the values were typed.

Types are also not type annotations.