[chroem-]

He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

[sidlls]

I find that a significant fraction of the bugs introduced to the code bases I've worked on that have dynamic typing are due to issues that even a rudimentary static typing system would prevent at compile time. I'm struggling to grok how a language with no type system might look. Something post-modern and Picasso-esque? To use data in a meaningful way in a program it must be possible to reason about it, and that requires that it have at least some structure.

[krallja]

Assembly languages are untyped. Nothing prevents you from reinterpreting a memory address as a type it is not. (Except possibly alignment issues.)

[sidlls]

That's not quite right though, is it? Nothing prevents one from "creative" interpretation of memory in, say, C, either, but it would be difficult to argue C is untyped.

[krallja]

The C type system prevents you from accidental creative interpretation of memory. You wouldn't say Rust is untyped just because of the `unsafe` keyword either.

No such type safety exists in assembly, except that certain opcode-register combinations are prohibited.

[Jtsummers]

Types aren't new. As the article discusses they date back over a century at least in math and logic. Within programming, we've had them in every major language for decades. The first big push for strong and expressive type systems is from the functional programming work which led to the ML family and the work that made Pascal and Ada on the imperative (and later OO variants) side, which dates back some 40-50 years now.

[dpratt71]

What is "he" right about, exactly? You say "yes they can be useful", but that's not the impression I get from OP. I am also confused because the very quote OP is responding to states that "...type systems are not enough to prevent all the problems in logic and programming...". Do you consider that acting like type systems are a cure-all?

[Anderkent]

> Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

Are you? usually I find it to be the reverse - you're leveraging the type system to track some properties for you, so that you don't have to track them mentally. I.e. less mental overhead (though possibly more boilerplate-overhead)

[CraneWorm]

For me, the elaborateness of the type system and it's checker REMOVE the overhead. YMMV, obviously.

[aoeusnth1]

I think you misread OP, and also misread the comment he was replying to; or, you just needed an excuse to vent about type systems.