That's a pretty strong take! I don't think there are many things that I feel similarly about... maybe if someone suggested that they don't need test environments and can just deploy changes to prod without testing or CI/CD and just see what happens, when it'd be my employment on the line, but even that's a pretty contrived and out there example.

> The amount of pre-existing respect for someone I'd need to have before I engage in a good-faith discussion on "are types good" is pretty high.

My problem is that not all type systems and the way you use them are equal.

When working with back end code, I really like .NET or even Java having a type system there for me. I know that people suggest that they have their own shortcomings (type erasure, NPEs, no multiple inheritance, even smaller things like C# enums not supporting methods) and that there are better options out there, but generally you can turn off the part of your brain that'd worry about the language too much and just deal with the domain problem at hand. Something like JetBrains are also excellent, because with the type system suddenly the tool also can reason about the language constructs you're using and give you all sorts of good suggestions and refactoring options.

Whereas with something like TypeScript in combination with React, there are times where you fight the type system instead. That's just the impression that I got working on a few projects for a while, in comparison to React with JS (perhaps the code was also a bit too clever), while with Angular it felt more coherent to me (despite Angular being more complex otherwise and not really my first choice). In the end, I gravitate towards Vue with JS for my personal stuff, but it's not like you can just say no to TypeScript when you need to maintain something long term.

I can't actually remember who said that they ditched TypeScript for similar reasons, but the argument was basically that a non-insignificant part of their codebase was there just to satisfy the type system. TypeScript does what it's supposed to... but it feels like it could be easier.

Not even one of my spicier takes, just one of the few that I simply don't care to engage with further.

> My problem is that not all type systems and the way you use them are equal.

We agree. Some type systems suck so badly that I can see why people would be tempted to believe that all type systems suck.

But that's my point: people say that exact thing about Java and .NET, while I find them usable. Meanwhile TypeScript has cool stuff like union types and other stuff to the point where you can get pretty clever with it (https://codegolf.stackexchange.com/questions/237784/tips-for...), which many would describe as the type system being objectively better, yet it's also more difficult for me to use.

In my mind, a good type system would let you do both basic stuff easily without too much work (to make sure that refactoring doesn't make you shoot yourself in the foot) and also encourage you to write the simplest code that you can get away with, while allowing you to get clever in the select few places where that is actually needed.

Which is funny, because adjacent to that, Java and .NET (web) frameworks can be a masterclass in incidental complexity, even though for me the type systems don't get in the way too much.

Edit: actually, I think I'll migrate a JS project to TS, this time in Vue. Perhaps Vue 3 will be a pleasant experience and if it won't, then I'll have a concrete list of things that caused me to feel this way.

That's pretty much my take. I don't hate anyone for having different ideas about it. But if you're going to use Typescript, don't use 'any'. At all. Unless you really don't know and the next step is figuring out what type you've got.

That's actually not hard, you need to be able to run in dry mode, and run the same in an existing instance (in parallel), then compare the results. If you are happy you can continue with the roll up, disabling the dry mode.

> I can see both side of the arguments on many topics, such as vim vs. emacs, tabs vs. spaces, and even much more controversial ones. Though in this case, the costs are so low compared to the benefits that I just don't understand why anyone would ever choose not to use types.

> I'd love to know what I'm missing, but until then: Strong typing is a hill I'm willing to die on.

I genuinely want to know what I'm missing. I also outlined in the post all of the arguments I usually see in favor of not having types and why I disagree with them.

I'm happy, willing, and excited to hear what I'm missing.

Is there a language out there that gives you that choice?

I expect you mean choose not to use strong static typing as per the original piece? Compatibility is a pretty good reason. I'd like to see Javascript die in the fiery pits of hell as much as the next guy, but its positioning means it is almost inevitable that some system will make it the only reasonable choice for you to choose if you want to build for that system.

Typescript doesn't help. It adds static typing, but not strong typing.

Usually: A strong type system does not allow types to change after being established. A weak type system allows types to change. This is also described in the original article.

so... like in c++?

Generally "strong" vs "weak" typing[1] is an ill-defined an mostly useless definition.

[1] as opposed to static vs dynamic or safe vs unsafe.

https://en.cppreference.com/w/cpp/language/explicit_cast

edit: I guess what you want to say is that implicit casts make a type system weak. But even there there is plenty of wiggle room: I think that everybody agree that implicitly converting the string "1" to an integer is bad (which is not allowed in C++). Narrowing conversions are arguably bad (they are sometimes allowed in C++), but some other implicit conversions are hard to argue against (int to long for example, or derived to base).

For dynamic types, sure, that's a reasonable enough definition. But it doesn't really make sense for static types: they're attached to expressions in your source code, not runtime values.

In order to have that, you need static typing of variables and constants, like most statically typed imperative languages have. But you also need a method to specify required input types and expected output types of all functions.

In a purely functional language like Haskell where there are only functions, and functions are first class and can be both inputs to or outputs from other functions, then the entire operation of the program is encapsulated in its function type signatures.

The entire flow of data and logic through the program can be type-checked by the compiler, and function implementations checked against their type signatures.

Or do you mean that the C-based escape hatches like casting pointers make the type system inherently weak? You don't have to use them though...

Said UB is observationally indistinguishable from miscompilation under some toolchains under some optimisation controls.

It also has various bolt on weirdness like const doesn't mean the thing won't be changed by some other pointer so you can't constant propagate based on it, unless it's written on the global, at which point attempts to mutate it anyway may succeed under the usual UB challenges.

Maybe that's a "strong" type system, but you'd only define it like that if you started by taking C++ as axiomatically reasonable.

> I'd like to see Javascript die in the fiery pits of hell as much as the next guy

Part of the problem is that some of those "next guys" don't have the experience and/or vision to realize that it needs to die. Perhaps we should emulate Cato in our subsequent HN posts:

And furthermore, I consider it necessary that Javascript be replaced with WebAssembly so that we can use well-designed languages in the browser.

As soon as there's any complexity at all or another person involved that exception stops.

Now, in general, I agree with you. If it's a one-off (or if it's really never going to need maintenance), and if it's small enough that you don't need types while writing it, then sure, do whatever is easiest at the time. But "never going to need maintenance" often turns out to be a lie, and when that time comes, you may be happy for some types as signposts to give a hint of what you were thinking all those months or years ago.

Otherwise, if you're unable to source another script, you could just have another script return a normal result in addition to a JSON blob of the environment variable changes the caller should make, which is probably worse than just allowing sourcing.

Pipes allow arbitrarily complex networks of communicating sequential processes. In some cases, networks of tiny CSPs are cleaner, but without discipline, they can rapidly become worse than huge monoliths.

Particularly as programs start out simple and organically grow, once they start hitting length limits, they're going to start evolving into locally-distributed computation. Maybe you get something nice like composable small unix-like utilities. However, I suspect there's a large overlap between the set of developers who would do that well and the set of developers who would still keep things nice and modular within a single process if they didn't have size limits.

The C runtime, on the other hand, will gladly (with UB nasal demon caveats) allow you to treat an int as a pointer. There are static type checks, but no hard limits on the type-confused nonsense it will attempt to execute. C is weakly statically typed.

Java, C#, etc. are strong statically typed. There are static checks at compile time, and the runtimes do their best (modulo escape hatches) to use dynamic runtime type checks to plug the gaps in the static type systems. (For any sufficiently complex sound/consistent type system, as per Godel, there will be some type-correct programs that cannot statically type-check. So, in practice, there will always be escape hatches in the type system. Hopefully most of these escape hatches are backed by dynamic runtime checks.)

Of course, these categories are a partially-ordered continuum, not clear binary distinctions. Also, type weakness is more a property of the runtime than the language, but for those languages with specifications, the language specification usually also specifies a large amount of behavior for a compliant runtime.

https://github.com/coalton-lang/coalton

What Lisp are you using that doesn't have types?

The vast majority yes, that's why I was a bit confused :D

There some languages that have no types. The only thing I can think of though is a POSIX shell minus arrays.

> Most Lisps do not have a static type system

True

> and even fewer have a "strong" type system.

Common Lisp, Emacs Lisp, Scheme, Hylang, Clojure, and Racket all feature strong typing. I'm curious where you have found this trove of weakly typed Lisp dialects

I think that interpretation of the "strong" vs "weak" scale is a valuable one within the context of the blog post. The post is at least partially about how type systems can help the programmer by making them aware of certain kinds of errors (it is also about when: static vs dynamic).

My understanding of the terms covariance and contravariance are a bit shaky. Could you provide an example in another language that you think cannot be expressed using the provided utilities of most Lisp's?

You also mentioned that you don't think most Lisp's have "expressive" type systems. What do you mean by that? When I think of a type system as being expressive, I think of it as having explicit rather than implicit types, which is unrelated to the issue of strongly vs weakly typed and static vs dynamic types. Do you mean more like how you can describe / constrain the relationships between types in certain strongly typed languages?

Sure, agree. That's also the real point: type systems primarily exist to make semantically impossible computations unrepresentable in the language (at least, without some extra song and dance). To this end, Lisps have rather lackluster type systems, but they don't try to encode much of the languages semantics into a type system.

> My understanding of the terms covariance and contravariance are a bit shaky. Could you provide an example in another language that you think cannot be expressed using the provided utilities of most Lisp's?

The wikipedia article on the topic is a great source: https://en.wikipedia.org/wiki/Covariance_and_contravariance_...

I'm actually mostly concerned with type invariants (ex. List[int]), which don't really have much for representation in Lisps from what I've seen. Further, see above about using types to make compile-time assertions/checks about the behavior at runtime.

> You also mentioned that you don't think most Lisp's have "expressive" type systems. What do you mean by that? When I think of a type system as being expressive, I think of it as having explicit rather than implicit types, which is unrelated to the issue of strongly vs weakly typed and static vs dynamic types. Do you mean more like how you can describe / constrain the relationships between types in certain strongly typed languages?

"Expressive" is a nothing word that doesn't have concrete meaning in-context, similar to "strong" type system. That being said, I would say Rust, OCaml, and TypeScript have expressive type systems: the behavior of the language is largely encoded as types. The implicit vs explicit nature of types is not super consequential IMO, it has more to do with how you primarily represent semantic meaning. In lisp, it's symbols. In Rust, it's traits, enums, and structs (+ the affine types, but that's not relevant here).

That makes inheritance-based covariance and contravariance largely moot.

You have substitutability-based covariance and contravariance (you can't get away from those) but they cannot be subdued declaratively.

E.g. if you're passing a callback function somewhere, which you know will pass widget objects to the callback, it's okay to use a function that was written to handle gadget objects, if widget objects are designed to substitute for gadget objects.

That's contravariance of substitutability.

Substitutability is the only thing that matters in the end. Declared inheritance doesn't ipso facto guarantee substitutability, and therefore declared covariance or contravariance, which are inheritance based, do not guarantee actual substitutability-based covariance or contravariance.

Having an order of magnitude more unit tests is another option, but that undermines the alleged "less code" benefit of weak typing.

In [0] in particular there're slides 22/23, here is part of the transcript but makes more sense with the slides on:

> And you can call them problems, and I'm going to call them the problems of programming. And I've ordered them here [...] I've ordered them here in terms of severity. And severity manifests itself in a couple of ways. Most important, cost. What's the cost of getting this wrong? At the very top you have the domain complexity, about which you could do nothing. This is just the world. It's as complex as it is. > > But the very next level is the where we start programming, right? We look at the world and say, "I've got an idea about how this is and how it's supposed to be and how, you know, my program can be effective about addressing it". And the problem is, if you don't have a good idea about how the world is, or you can't map that well to a solution, everything downstream from that is going to fail. There's no surviving this misconception problem. And the cost of dealing with misconceptions is incredibly high. > >So this is 10x, a full order of magnitude reduction in (?) severity before we get to the set of problems I think are more in the domain of what programming languages can help with, right? And because you can read these they'll all going to come up in a second as I go through each one on some slide so I'm not going to read them all out right now. But importantly there's another break where we get to trivialisms of problems in programming. Like typos and just being inconsistent, like, you thought you're going to have a list of strings and you put a number in there. That happens, you know, people make those kinds of mistakes, they're pretty inexpensive.

[0] Video: https://www.youtube.com/watch?v=2V1FtfBDsLU

[1] Slides and transcript: https://github.com/matthiasn/talk-transcripts/blob/master/Hi...

[2] Video https://www.youtube.com/watch?v=YR5WdGrpoug

[3] Slides and transcript https://github.com/matthiasn/talk-transcripts/blob/master/Hi...

The reality is I never get to choose. I prefer strong typing. But the projects I am on that ship sailed long ago 2 developers back who used this project as a resume builder.

> We should not categorically denounce people who prefer it as lesser developers

I don't think you've justified this point. I'm comfortable with my position on this.

It seems reasonable to argue that statements that you won’t even discuss X any more and would rather judge the person as less competent professionally are unproductive. Not saying I agree, btw. But it does seem like a pretty basic point. One of you is talking about preserving your sanity and the other about output. It’s not necessarily a disagreement even.

That is absolutely NOT what the other poster said. They said they _MAY_ judge them that way.

I still think it's reasonable to argue that's not a "productive" approach, but like I said, that's not my own opinion, I just think it's a reasonable argument.

I don't necessarily think it makes someone a "lesser developer" if they prefer untyped languages, but I DO think they've either had to maintain anything long term or it stayed relatively small.

Whether that makes them lesser or not isn't really for me to say, but I can say I'm definitely on board with the idea that types increase productivity the longer a system is maintained. Unless used poorly, types don't automatically mean you use them well, but they make it a hell of a lot easier to do the right thing.

Some issues are settled enough that there is no need to discus them any further. It is okay to automatically mark people on the wrong side of such issues… let’s say ill-informed.

Static typing, I believe, is close to being one of those issues.

Imagine someone is working in a relatively niche new programming language ecosystem which is dynamically typed, allowing the language to have some richness that modern type systems don't support. I don't have an example because I don't know of any such language in 2023... BUT back in the 70s and 80s this would have been Lisp. Lisp couldn't have been strictly typed back then because, AFAICT, type systems hadn't advanced enough to express the sort of metaprogramming that made Lisp unique and awesome. This was at a time when most popular languages were strictly typed.

I would hope that you would keep your mind open to whatever that maps to in the 2020s.

Now, if someone says "I like JS over TS because types are annoying and slow me down", then yeah, I don't have much patience for that either.

The thing is, I've yet to encounter a single instance of such an argument today. Every single time it ends up being "I like JS over TS because types are annoying and slow me down". It hadn't even occurred to me that laziness and sloppiness weren't the the only reasons to write in dynamically typed language.

I suppose what I'm saying is I'm quite interested in seeing what kind of evolution some dynamically typed language could offer in the future. Although with no signs of its coming, I'm going to stick to TS because it's objectively better for anything but very small projects.

At best it's a form of documentation that enables some simple linting rules and a bit of jump-to-definition magic. Like, that's a benefit (mostly -- I tend to think that type signatures implying more guarantees than they provide is a recipe for inadvertently relying on falsehoods), but it's not as clear-cut of a win as you see in other statics/dynamic tradeoffs.

I don't mean to be unnecessarily contentious, but isn't that the point of undiscovered territory?

We haven't encountered it yet, when we do then as awareness grows that pattern, idiom, theorem or concept will be picked up by mainstream statically typed languages.

It's enough to believe that the properties of (for example) JavaScript might lead to an as yet undiscovered pattern that is not possible in current statically typed languages.

Unlikely, but still possible.

The type system enforces those permissions: writing to an impermissible destination is a type error. The types applicable to an entity are not necessarily knowable at compile time; some of them might change at any time.

I had a job working on such a system. It supported a type system implemented in Haskell with both static and dynamic type disciplines, where values were tagged with base types designed to be checked dynamically in hardware.

Was the programming language dynamically typed? Yes. Was the programming language statically typed? Yes.

You can't honestly believe no one who likes to develop in a dynamically typed language has nothing interesting to say about software development?

But that wouldn’t be a wise use of time in my opinion. And that’s what they’re ultimately driving at: we all have limited time to expend, so do it in things that matter to you. I believe “matters to you” is a bias.

Beliefs inform decisions and other beliefs

I disagree with them on a huge number of fundamental things in software. Most of their fundaments are claims with no evidence. Due to that, I simply do not care about what they have to say most of the time.

It is both useful and allowed to have a certain level of belief that won’t be crossed without heavy effort. The OP didn’t even say they were closed to the conversation completely, but that a random person with no pre built trust isn’t going to get the time of day from them to rehash the same settled argument.

from memory Matz -> ruby, Valim-> elixir, Van Rossum -> python, and 'the creators of Julia' -> julia

Not 'random persons' then

This confused me for a moment, but I think you mean annotating the types of the fields in your `struct`s, right?

An addition to that: any non-constant global variables (if you must have those) should also be type annotated.

Dynamic types are nice for quick & short scripts, and actively detrimental for anything long and complex. Why not enforce that? As soon as it gets so long it doesn't run you know it's time to rewrite in a statically typed language. Instead all existing scripting languages allow unlimited growth in code size, making it easy for programs to grow beyond the point where the language is useful.

A long list of big products and companies are there to disagree with this. I am not saying that dynamic is better or worse. But saying that dynamic languages are only good for quick short scripts is a wrong generalization that has not one exception but many exceptions.

But people regularly say the sky is blue, and it's clear as day that it's not when the earth has turned and your side isn't facing the sun.

Only due to Rayleigh scattering do we perceive it as blue, but that’s not due to the absorption and reflection of different wavelengths we associate with innate color. Note that the color changes depending on the angle of the sun, even to the point that it’s purple and red at a few times during the day.

Our perception of the important colors (sky blue, ocean blue, vegetation green, …) probably evolved along with our physical needs.

Don't venture into tornado country; your doubt may be your downfall.

But he's just being honest. Many developers have been making that judgement for many months or even years.

For the very rare cases where a lack of strong typing is needed, most languages with strong typing offer ways to handle that (i.e. the Object and Dynamic types in C#)

It's like if you met a builder who refused to use a hammer and insisted on bashing nails in with the back of their drill. It's not "personal" to say you'd respect that person less as a builder, regardless of how much you'd enjoy having a drink with them.

TS has a very complex type system in exchange for relatively weak guarantees about correctness. That's a tradeoff you can choose to take or leave depending on the problem at hand, and holding that position is not the same as believing types have no value.

Unless you're talking about elm or rescript or something then sure sure. But usually when people say things like this they mean typescript.

I still have hopes that Kotlinjs can fix the distribution size and the tooling around binding to js libraries.

Sure it can be an adventure to express something fully in it - but this is true for any type system I've seen.

And I haven't seen another type system that's integrated into a dynamic ecosystem as well (IMO python is 5 years behind in terms of type checking experience) and that lets you chose the level of type sophistication that makes sense.

Static typing, code analysis, automated testing, etc. are all great tools that become counterproductive past a certain point. Where that point is highly depends on what you're doing and typescript is one of the most flexible type systems at letting you make that choice. I'd say a lot of people are terrible at recognizing when they went too far with it for no practical gain.

My only problem with it is that they can't fix the shit JS semantics.

I'm just pointing out that having an opinion about typescript is not the same thing as having an opinion about types. Something I think people are (intentionally?) conflating in these comments.

Too many web developers, basically, I don’t think the conflation is intentional

But all of that makes plenty of sense because in the early days it was rare to work on a real life production JS project that was pure TS from day one in addition to having TS only libraries.

These days it's everywhere and the work has been done to move away from rampant anys in popular libraries. The tooling is also mature and it's rare to find major JS libraries not already packaged with types or a @types import. Turbo moving away from TS was the rare exception.

Well:

  % cat a.ts
  console.log('Hello, world!')

  % time tsc a.ts
  tsc a.ts  2.39s user 0.10s system 232% cpu 1.066 total

esbuild is not an alternative as it doesn't check types.

What I want is "GET /foo.js" to "just" compile TS "on the fly" in dev; it's a simple "just works" kind of setup, but not possible with TS.

Or for a simple system, just "roll your own":

  for f in *.ts; tsc $f >|$f:r.js

  watch-files *.js --run tsc

  (for f in *.ts; tsc $f) | minify >production.js

What exists now is an explosion of complexity to deal with all this and I guess these systems are "mature", kind of, but for a lot of systems it's massive overkill (and even for larger systems it's not particularly great IMO). Besides, it's really a bad fix for more fundamental problems.

Personally I wouldn't call TypeScript mature until compile times are roughly within the range of literally ever other compiler that has ever seen wide-spread adoption. It doesn't need to be fast: just not a huge outlier.

Explosion of complexity and "bad fix for fundamental problems" sounds a lot like you just have an axe to grind.

Many other popular languages have multiple build systems and tools to choose from as well; it isn't a particularly novel challenge.

"You just have an axe to grind!"

Hmkay.

I just want things to compile, with errors, like literally everything else works. It's really not a huge ask. I don't want complex bespoke setups with multiple compilers and background processes and whatnot. The classic JS/TS response is "here is the happy path with all this tooling, but if you want something outside of that then there is something wrong with you".

`tsc --noEmit a.ts` (possibly flipping the position of the flag, I forget if it is sensitive).

That'll check the types without spending unnecessary time compiling with the slower tooling.

From there, esbuild or swc binaries compile the code as desired. They use the same tsconfig file that tsc does, so no need for any extra complexity. They build so fast that you'll not mind having a separate command, I promise.

You could even combine the two into a simple one-liner if you wanted.

Compared to, say, java where you have to fight over maven or Gradle or ant, plus endless config options in XML or groovy or whatever, typescript really isn't much to complain about.

Hell, trying to set up a clojure full stack project is a nightmare of conflicting opinions over tooling between lein and shadowjs or whatever.

Of the big languages, C# is about the only one with a "one true way", and of the smaller ones, they simply haven't yet developed a big enough base to grow contentious enough to have divergent solutions.

The raw output speeds aren't a very good 'practical real world example' as the OP described it.

If anything in dev ESLint (+ Copilot) is the slow ones that I sometimes noticed, but there is already Rust driven replacements maturing in the pipeline as we speak.

I looked in to this some time ago, because I couldn't believe it was this slow, and tsc just has a huge startup cost. Once it gets going it's alright (I think? Don't quote me) but to get started takes a long time. It's actually already improved because not too long ago it was more like 3 seconds (probably because of the parallelisation, which is kind of cheating IMO).

I don't know about Java as I never really used it, but complex build systems are not unique to TS of course, but what they are in TS is mandatory for any reasonable experience because it works around the fact the compiler is so damn slow. That's a huge difference you can get started without too much effort, and you can do "smart" things fairly easily as I mentioned in my earlier comment.

> they simply haven't yet developed a big enough base to grow contentious enough to have divergent solutions.

C, C++, Go, Rust, Python, Ruby, PHP don't have a "big enough base"? Ehhh

And my entire point is that TS LACKS "divergent solutions". Because it's so slow lots of solutions are simply not practical.

IMHO these are markedly different scenarios: the first is essentially just a difference of opinion, the second is a rather myopic attitude.

This applies to much more than static typing as well. Anything built, can be built well or it can be built quickly.

Although I often have to make trade-offs for immediate gain at work, there is a big difference between the quality of my work over time vs the quality of other devs who default to immediate returns. I will say in their defense, they play a role in the team. But I wouldn't want to work on a team where avoiding upfront costs was the expectation rather than the exception.

"I've worked with my fair share of vanilla JS devs who refuse to acknowledge the benefit of testing. Most of them bemoan the upfront cost of testing everything without realizing the benefits of it. I absolutely think less of them as developers."

The really issue with compile-to-Javascript languages is debugging. Have fun stepping through your incomprehensible generated code in dev tools.

(Except Dart which has really good Dev tools support; I guess they can poke the right people to make it work.)

So, how often is poorly tested code out there? From the popularity of strong static typing, it must be ubiquitous.

Static verification (what includes static types) is the real deal.

That said, WTF is there with people insisting that types must be either static or dynamic, and that dynamic types are useless?

Whoever said you can only pick one of the two approaches?

If a developer can jump into an unknown part of a codebase and quickly see that following a certain structure will automatically make their code work for them without needing to read all the code first and double checking if it's just a random convention versus a strict interface so they don't reinvent the wheel or build code that doesn't fit in with the existing structure, then that's worth a lot and something you cannot simply cover with tests.

If anyone can think of something a unit test could test for that an arbitrarily* complex/strong type system couldn't I'd be interested to hear it. It's possible, I just can't think of any.

An arbitrarily complex type system, with dependent types, could detect any bug, since it's formally equivalent to requiring the program be proved correct. But using such a type system is so onerous that I don't know anyone who realistically does it in production.

If you wrote such types, you're basically giving a formal specification of what the program is supposed to do. That could then be used, and likely much more easily, for high volume property-based testing.

More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

if you have a type system expressive enough to do things like that, you've basically got another turing-complete layer on top of your existing language, which is itself ... dynamically typed.

So, how often is poorly typed code out there? From the popularity of test coverage tools, it must be ubiquitous.

In a situation where extreme levels of testing occur, the extra assurance from strong typing is minimal. In a situation where strong typing is enforced, extra testing is still very useful.

Consider a finite state machine with N states. There are a priori NxN possible transitions. In many cases however most of them are impossible, and you really have only O(N) feasible transitions.

Sure if you make O(N^2) tests you don't need typing... but typing could have made many of those transitions literally impossible. You don't need to test the impossible. For a sufficiently large codebase, you want to limit as much as possible the amount of tests you need.

Also I have more than once identified issues in our testing framework because when I made stronger types I uncovered bugs that escaped our tests. Non-deterministic concurrency bugs are extremely hard to test for. So yes, testing can uncover type bugs, but typing can uncover untestable bugs.

Ok, but it's cheaper to not have to write those tests than it is to write those tests.

That's quite clearly not what I'm saying.

It is like the things you already trust when you code. Let's say, that the file system works, that the network stack of your OS works, or that the cpu works. You can rely on them to use your time for the things that matter. This is a much better model than simply testing everything yourself since, as the tests number increase, any change to the codebase involves more and more test changes.

> Strong static typing is useful in the environment where the code is not adequately tested. That's because tests adequate to make the code bulletproof will also detect the problems strong static typing could detect, rendering SST superfluous.

Your logic is the same as follows: seat belts are useful in an environment where drivers are not driving adequately. That's because adequate drivers will drive in a way to avoid any danger that the seat belt would prevent, rendering seat belts superfluous.

Ultimately, the problem is adequate drivers (as in described above) or bulletproof tests do not exist, they are just a concept. A test can prove the presence of an error, not the lack of errors, and the argument only works in absolutes.

The analogy with driving doesn't make much sense. After all, accidents sometimes happen without the driver being to blame, and the marginal cost of putting on a seat belt is very low.

Apart from an analogy is a template of your argument. It is the logic of the argument itself.

Errors also happen sometimes without type systems being to blame (they only catch a subset of errors).

The marginal costs of a type system is usually very low too, so it seems to be a great fit.

When you use a typed language, you can use your integration tests to actually verify business logic, exception handling, etc. instead of having to write a dozen test cases to make sure that doThing(table, index,*kwargs) doesn't blow up when 'table' is a list or 'index' is bytes...

(It won't find latent bugs that can't currently be exercised, so the testing can't be one and done.)

if you use a static type system you can guarantee there will be no type errors at runtime. why on earth wouldn't you choose that? you can still write logic tests!

and when you leverage the type system to make illegal states unrepresentable, you can make certain classes of logic error impossible as well. some of your tests become tautologies and you can delete them.

What testing cannot find are latent errors not exercised by the program. Do I care about these, though? Arguably these would be found by testing internal interfaces and elimination of code not reachable by tests.

The general argument I am trying to make is that the marginal value obtained by strong static typing declines as testing increases, and that in the limit goes to zero. If a program is adequately tested, is it still worth doing? This is not clear to me, and the arguments given here have not convincingly demonstrated that it is worth it.

Also: if you find yourself in a situation where strong static typing seems useful, you should be alarmed. It means you aren't testing your code very thoroughly.

I am not assuming that.

honest question: what language do you have in mind when you think "static types"? your perspective is so starkly different to mine, you seem to be operating under totally different assumptions about what types can and can't do.

I mean this sentence:

>Also: if you find yourself in a situation where strong static typing seems useful, you should be alarmed. It means you aren't testing your code very thoroughly.

is just baffling to me. it's so self-evidently absurd that I can't even argue against it. what is there even to say?

have you even used a modern statically typed language, with type inference, generics, null safety, algebraic data types, pattern matching, etc? I cannot imagine trying to maintain a big codebase without them. they don't slow me down, they speed me up. they aren't just about catching trivial int-instead-of-string bugs, they are are core tool for modelling data and business logic. they let me define problems out of existence (see e.g. this series of posts https://fsharpforfunandprofit.com/posts/designing-with-types... for an introduction).

and then there's rust and newer-generation languages with borrow checkers and affine/linear types, ruling out entire classes of memory and concurrency bugs ... your test suite cannot rule out data races, but rustc sure can.

you are making the same arguments people were making in the 2000s when most static languages sucked because they didn't have these features. I don't want to go back to a time before sum types.

>What testing cannot find are latent errors not exercised by the program. Do I care about these, though?

you should, because in production your program must endure orders of magnitude more variety in inputs, uptime, and runtime conditions than the test suite can exercise. it can and will get into weird states you didn't anticipate. yes, you can fuzz, yes you can property test, I know all about that. those things are good. but I don't get why you wouldn't also use a static type system to provably rule out classes of problem across all possible code paths. why settle for less?

Because type errors in unit tested code are basically non existent. It's a fictional problem and as such there is no point in spending real resources chasing fictional problems.

There is plenty of research that shows that static typing gives no benefits (statistically insignificant) when it comes to software correctness.

What you are asking is why shouldn't the local government spend money on a Yeti patrol to protect the general public against Yeti's? The Yeti patrol will eliminate an entire class of problem (Yeti attacks).

this is short-sighted. I am not talking about trivial string-instead-of-an-integer errors here. powerful type systems let you encode far more sophisticated constraints on the program. safe rust makes data races into a compile-time error via its type system, for example. unit tests can't do that.

I think you're greatly underestimating what types can do for you. you seem to have this mental model where you would write the exact same kind code with a type checker as without one, and the only difference is whether you have to convince some pedantic bureuacrat that your code is correct when you already know it is.

but when you have a powerful type system, you don't write the same kind of code. the type systems helps drive design, similar to how tests can drive design. you have probably seen code that is bad because it wasn't written with testing in mind. there wouldn't be much value in adding unit tests to the code right away -- you probably need to do some highly invasive re-architecting to make it testable.

so, is it really such a stretch of the imagination that code can also be deficient because it's untypeable? perhaps the reason you don't see much benefit to types is because you didn't write the code with types in mind, as a design tool.

there is a learning curve to writing testable code. the same is true for types.

read this if you haven't, about type-driven design: https://fsharpforfunandprofit.com/series/designing-with-type...

No, my mental model is removing the type checker allows me to write shorter, more concise and higher quality code. Dynamic typing enables much better code styles than static typing.

> the type systems helps drive design

Ahh you are an complexity merchant, if only I made my code more complicated all my problems would be solved. I'm afraid not, the more complicated your code the worse it is.

No I'm afraid, I have actual real commercial experience of doing both styles of software development, the dynamically typed code is the better approach by far.

It's not that I don't understand you, it's just what you are saying is a load of rubbish. :p

I'm currently responsible for a very large system built in raw javascript where function definitions like this one in the article: function birthdayGreeting1(...params)

...are the religion.

It's awful. I hold the people responsible in very little regard.

- Use notepad for development (don't laugh, I've actually encountered a dev who's choice IDE was notepad).

- Never worked with more than 1 person on a project.

- Never worked on anything but tiny projects.

- Never re-opened a project after having worked on a different project for several weeks.

And then, kind of orthogonal to that, there’s also static typing and dynamic typing.

I think strong, dynamic typing is just as good as strong static typing (weak typing is objectively bad)

As long as the types of your variables don’t change from under you, that’s good, but I’m also okay with the compiler / runtime figuring out what those types are for me.

A side (but many would also say critical) benefit of types is that they act as a form of documentation that can never go stale (because they are enforced by the compiler). "Dynamic typing" does not offer this benefit whatsoever.

That’s the crux of why I’m not all in on static typing all the time. (Especially for networked programs that expect a wide range of different kinds of input)

Having to prescribe the types I need before I actually need them goes against how I tend to build.

Almost all static type systems have escape hatches that let you go dynamic when you really really need it. Also, I bet that most of your use cases for dynamic typing could be solved with a simple tagged union. Most people bemoaning the lack of flexibility of static typing just don’t know about how tagged unions can easily emulate dynamic typing when we need it, such that we rarely even need to reach for the actual escape hatches.

> (it’s impossible to know exactly what data structure you need at the start of a project)

Thankfully data structures are even easier to change with static typing: change it, gets a ton of type errors, fix them, done. With dynamic typing you run the risk of missing a call site.

> Having to prescribe the types I need before I actually need them goes against how I tend to build.

There’s type inference for that. I personally take advantage of it any chance I get.

JS will convert types under your butt if you're not careful, Python won't.

Sure, static typing (when done well) is superior to that, but the title talks about strong typing.

In Common Lisp, it's common practice to not accept code unless all such warnings are gone.

Every argument I’ve seen in favour of dynamic typing is some variation of “I like it this way.” They’re not technical arguments because dynamic typing is a strict subset of a statically typed language, equivalent to passing a flag to turn the type checker off.

Sure, not every compiler offers such a flag, but that is an argument against one particular static language (or group of languages), not an argument against static types itself.

Types are not exclusively for verification, and even if you decide it is, you can do a lot more with a type error than exiting the program.

That stance most people keep repeating is actually ridiculous. The most common usage of static type systems is to verify badly-written ad-hock dynamic ones that handle user errors.

This is just incorrect. Plenty, if not most, dynamically-typed languages are compiled. Indeed even the idea that there's a clean dichotomy between compiled and interpreted is an outdated idea: I'm not aware of any production languages which run tree-walk interpreters entirely without compilation. Modern "interpreters" typically compile to bytecode but in some cases even can compile to native code, they simply do so in a just-in-time manner. These compilation steps are quite capable of applying type systems.

For example, if you run a Python script, you can see the results of compilation cached in .pyc files (these will be either in the same directory as the source files, or in your __pycache__ folder, depending on your configuration).

> The whole point of types is to be able to check things without running the program, because exercising every possible code path becomes increasingly untenable at scale.

Is it? I would argue that the point of types is to report errors at the place where they occur, rather than doing the wrong thing silently and reporting an error elsewhere, or simply behaving incorrectly.

If a tree falls in a forest and nobody hears it fall, does it really fall at all? If a bug happens on a code path, and nobody exercises that code path, is there really a bug?

I would never want a statically typed, compiled awk for example.

I generally think large, production, multi-developer software should be written in a statically typed, compiled language.

Strong vs Weak typing is a closer to a debate about having a name spacing system or not. There is really no great reason to have weak typing or not use a name spacing system.

Mainstream dynamically typed languages are moving in statically typed direction. Python (Mypy, Pyright and others), Ruby (Sorbent, Rbs), JavaScript (Typescript, Flow). How many statically typed languages optionally removed types?

Personally I think Python moving in the direction of static typing is a mistake, dynamic typing is very useful for domains where python is strongest: modeling, statistics, scientific computing etc. It's also part of the basic design of Python to be a dynamic language. Likewise Ruby, with it's heavy use of metaprogramming, also benefits tremendously from a lack of types.

But let me be clear: I do think statically typed languages are a very good idea for large production systems, I just personally do a lot of programming that's not for these systems.

> How many statically typed languages optionally removed types?

I wouldn't say "removed" types, but I've been in software along enough to remember when dynamic typing was the big hot thing and crusty old Java devs complained that we couldn't possibly live without static type annotations. I distinctly remember when C# introduced `var` (which is of course really type inference, not dynamic typing) to appeal to devs that were growing weary of types.

There's a great example in SICP of implementing a full object system in just a few lines of code that would not be possible to implement as elegantly in a statically typed language. Do I want that for a production system? No. But there is, or at least used to be, a world of computation being done for reasons other that quickly getting PRs pushed out to prod.

> edit: To clarify, I am on the "types good" side of things

I agree. Python 1 would have been worthless if it didn't have types.

Dynamic typing also makes a ton of optimizations basically impossible and even after monumental efforts languages like Javascript are still quite slow, inconsistent and memory inefficient outside of trivial benchmarks.

I thought this meme was dead already. Of course, you might not be able to squeeze out the same amount of performance compared to a brilliantly written C or Rust program, but for what it is, JavaScript is pretty damn fast already.

DOM manipulation on the other hand, is still a very common bottleneck people come across when writing typical JavaScript code.

It's fast compared to other dynamically typed language implementations but it's still very slow compared to basically all of the popular statically typed languages.

true

> it's still very slow compared to basically all of the popular statically typed languages.

Not true.

The main slowdown for javascript (AFAIK) is the checks the optimizer has to put into place to ensure the assumptions it's made about the type are still valid. If, however, those assumptions are valid then javascript ends up emitting pretty much the same assembly that you'd see for and highly optimized statically typed language. In fact, there are some circumstances where it can beat a language like C++ or Rust due to the fact that it has to incorporate runtime information into optimizations.

With C++ or rust, if you add dynamic dispatch, unless you are doing PGO and whole program optimization, you are pretty much sunk with 2 memory lookups on every function call. This is the case where javascript can end up beating C++/Rust.

(All of this is talking about hot code after warmup. During the initial execution javascript will almost certainly always be slower).

Part of the proof of this was asm.js, the precursor to wasm. V8 at the time it was introduced could execute asm.js nearly as fast as what firefox could do with it's optimized asm.js compiler. That is, when you stripe out all the actions that make javascript slow, it very often ends up being just as fast as a compiled language.

What stuff ends up making it slow? Generally speaking, stuff that makes the types unpredictable (adding fields, removing fields, sending in a number and a string and expecting the VM to be able to handle both).

You can see a lot of this writeup around the discussions about why Dart was originally "optionally typed". Basically, the entire selling point to make dart fast was simply to remove the abilities to dynamically change types like you have in javascript. With that, the VM authors at the time were capable of making a VM that's every bit as fast as what Java has.

GCC at least is capable of speculative devirtualization by using local heuristics, without PGO. And of course it is capable of devirtualizing in many cases when the knowledge actual type can be constant-propagated.

Also note that the vast majority of calls are not dynamic in C++ (as opposed to most dynamic languages), so devirtualization is significantly less impactful.

ok...

> In fact, there are some circumstances where it can beat a language like C++ or Rust due to the fact that it has to incorporate runtime information into optimizations.

People used to make the same claim about Java and in every single example I've ever seen the Java/Javascript is extremely optimized, performance isn't consistent across VM versions, and the C++/Rust is extremely naive (usually allocating unnecessarily and not using arenas in hot paths that are allocation heavy).

It never happened.

And, you can look at the code yourself, most of the examples read pretty much exactly the same as their C++ counterparts.

Mind you, this is also a test that looks at execution start to finish and doesn't give warmup time (which will always favor statically compiled languages).

> performance isn't consistent across VM versions

That's true for C++ compilers, so why would you expect performance to remain constant with a JIT compiler?

[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

Notice that in the Java, C#, Go, Rust, Swift or Ocaml examples almost all of the underlying data structures and much of the networking stack are built in the respective language. This is not possible with Javascript, Python, Ruby etc. because it would be ludicrously slow and extremely memory inefficient.

There's a certain segment of the developer population that I don't think realizes just how fast C and C++ are. Javascript is _relatively_ fast when compared to other dynamic languages, but not when compared to C, C++, FORTRAN, etc.

I write Clojure in my day job and it’s insane how often we have issues where it would have been immediately caught by a static type check.

How have you experienced using Type Clojure, spec, Malli, etc. to determine correctness?

I've only worked on solo projects with Clojure, with most of it fitting into my head. I imagine with teams of size N > 1 things can change quite a bit.

Can you describe your usecase for which JavaScript is slow? There are many languages that are slower than js like python or elixir, but they are doing just fine, that's why I won't agree that js is slow, but sure there are cases for which js just wasn't designed, and any CPU intensive task will be slow, but there are ways to get around it as well.

Please provide evidence for this extreme claim. I can point to benchmarks[1] where JavaScript is competitive with or even better than compiled static-typed languages like Java.

(any argument that those are "trivial benchmarks" is automatically invalid without actual empirical evidence)

[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

Nowadays, the static typing is much nicer, with both higher benefits and lower costs, and it makes the costs/benefits analysis much more likely to come out in favor of static types.

In the late 1990s when I was cutting my teeth, I did a lot of Python, and I was almost 100% dynamic language until ~2015. In hindsight, I might do the same again even if thrust back in time. There just isn't a great static option back then. (I'm not saying 2015 is the year it became practical, I'm saying that's when I finally moved into static languages. 2010-2015 or so I was in Erlang, doing things that most other languages couldn't do at the time, so that forced me into a dynamic language. C# was looking pretty good in that time frame too, it just wouldn't have run the systems I had on anything like the resources I had at the time. It could probably easily do it in 2023 though.)

Now I even prototype in static systems, and it's a better experience than prototyping in Python was. Like, by quite a lot, honestly. In the end, I don't find it that much of an impediment to make sure that if I want to call a method on a thing, that the method actually exists.

Dynamic typing will never disappear; there's a certain small size of task for which it'll always be more advantageous than static typing, and while said tasks may be small, there's a lot more of them than there are large tasks, so it's a completely valid and sizable niche. But I do think over the next 10-20 years we're going to see the "scripting" languages return back to "scripting" and away from "systems".

I think that in the end, the dynamic scripting languages being used for large tasks will be seen as a reaction to a misdiagnosis of the problems in the 1990s. The code was atrocious in the 1990s not because it was statically typed, and therefore the solution is to go dynamically typed. The code was atrocious in the 1990s because it was poorly statically typed, and the solution was to get better. That said, "getting better" did take a long time, and for many legitimate reasons.

(Much ink is spilled on the so-called rapid pace of technological innovation in our industry, but programming languages move on decadal scales. Programming languages still have only barely grappled with a multicore world, and haven't grappled with a heterogenous computing world at all (GPUs on one end, efficiency cores on the other). Things are not always in as much motion as we fancy.)

[1]: Particularly, Hungarian notation is supposed to supplement the type, not just reiterate it. If you're in a language where you can't easily declare "a width is an int", then Hungarian notation suggests calling a width variable something like "wdthDialog", so that you stand a chance of noticing that you passed a "hghtDialog" in the wrong place. But the way it was used a lot of the time is you got "u16Width" instead, where u16 meant unsigned 16 bit int... but that's already in the type. Using it that way just adds an extra layer of hierglyphicness to the already ugly code. One of the several innovations that made static typing languages more feasible is that in most languages designed in the last couple of decades, you can declare something like this with something like "type Width int", and then you don't need to label any variables with it at all, the compiler enforces it.

1. It's simple. Let's not lie, let's not pretend. It's CRUD. You can put in K8S, you can add AI, it can be behind an API Gateway, you can make it all Event Driven, you can use CQRS for every entity because you really, really want to feel clever. But it's still CRUD.

2. Other people are working on it, many other people.

3. People from other companies are interfacing with it.

So knowing what to expect trumps everything. Types help with that. They help a lot.

To be clear: people have tried to show the long-claimed safety benefits for a long time, and they just refuse to appear.

What have you built or added to the field that justifies such a lack of tolerance of those who don’t subscribe to your point of view?

That said, yes, of course my post is arrogant and dismissive. I am outright saying I won't engage in a conversation. I'm comfortable with that.

It's actually arrogant and dismissive because you say that in a way clearly intended to spark a conversation.

Also, pretty much all arguments for explicit typing suffer from mechanistic bias (see, https://www.youtube.com/watch?v=NmJsCaQTXiE&t=143s). I'm comfortable saying I just enjoy tinkering with a formal description of a data structure, because I'm a type enjoyer, not a type fan.

I don't follow at all. Why would it be arrogant or dismissive to say something in an attempt to discuss it? I commented in good faith to an article that has a strong opinion ("willing to die on this hill") with a reflection of my own strong opinion ("unwilling to discuss").

At most you could say it was inflammatory, which wasn't intentional although looking at the insane number of child comments it apparently ways.

Types are integral part of standard programming languages. If you mean "types bad" as in BASIC/Javascript variables, then yes I fully agree. These languages were never meant to be a solution for professional software engineering.

Once a language has proper types, it can be "weak typed" by not forcing "strong typing" by being dynamically typed in nature. If the language has normal preprocessor support, the static type system can be added on the project level. And then in essence you get a strong typed environment in a very thin programming language such as C.

Let's take a big C or C++ software project, the process behind it. Of course, the project is in those languages because it requires native opaque pointers and hardware access. The project has coding style, it has arbitrary rules. Although there is little to stop anyone from making a mess in C or C++ code there is entire code infrastructure and CI/CD chain around it. Lets say the rule is no void pointers without encompassing struct that's a type that can be checked via macro system. If you wrongly use the type struct, you get stopped by the project build. If you go around the rule, you get stopped by a code analysis after commit (and get in trouble for doing that).

I think that says more about the strength of your zeal than of your argument.

if you get the static type system wrong once, there's no going back

Take for example, Rust: mut, Send, Copy, Drop, Debug, dyn have all their warts because they are special and you can't fix them because you'll break previous code.

In a gradual typing language you could potentially bolt-on your own type system as a package where it just runs the type checker if you want one. It just so happens people who favor these gradual typing systems don't do a good job of creating those typing systems because they are not that into types in the first place.

But in theory, this kind of a system would let you not worry about types when prototyping the system, then put some bounds later based on your requirements.

SML or Haskell? Yep, like those ones. The languages would not be so useful without their compile time type checking.

C? Not worth the trouble. C++? Not worth the tarpit or the trouble.

Python? Definitely not keen, that language was much better without the annotations.

Typescript people really like but I haven't played with. I'm pleasantly surprised that unsound static + sound dynamic works well.

Type annotations are not inherently good. Some type systems add a lot of value, some really don't.

The OP said strong static type system, so C and C++ are out of the question.

People who say they prefer dynamic languages are really just saying ‘no’ to all these free benefits.

Otherwise the cost is merely being unable to write anything that the type checker does not understand, and however long your compiler takes to do the checks on what it does understand.

Also a fair chance the whole program must type check before you can see the results of changing a subset. In the worst case you get to hunt down all the unused variables before it'll run the test suite.

I prefer dynamic languages. That makes me a heathen on these boards, to be ignored or chastised for my stupidity. Regardless, those benefits do not come for free.

- having a compile step in between writing and running your code. This drastically slows down the feedback loop of development. The more your compiler has to check for you, the slower it gets.

- being able to run your program in a half-broken state. This may not seem like much of an advantage, but sometimes it is good to just be able to run a broken piece of code to see how it crashes. This is especially important when learning to program, but is still very beneficial when learning a new language or framework, or sometimes for debugging.

- As someone who has contributed to the main Haskell compiler, I can definitely confirm that a more complicated type system can slow down development of the language itself too. It takes significantly more effort to grok all the possible interactions as the codebase of the compiler grows.

Don't get me wrong, I think encoding and enforcing program properties with types is a great idea that will grow further in the future. But the dynamic languages gained popularity for good reasons, and some of those reasons are still valid today.

Not strong enough.

If you are proponent of strong typing, you need something that is effectively a theorem prover. I.e when you define a type, you define the scope of the data it can hold, operations on that data, and the resultant types of those operations. That way, when you code compiles, it is by definition "correct".

When you accept anything less then that, you are basically making a statement that you are willing to forgo some of that correctness for convenience, which is fine, but that means that no language out there is really good or bad.

That said, your position is also just weird to me. Yes, theorem provers have nice type systems that are wonderfully expressive. The trade-off is that some common programming patterns become difficult to use or are even impossible.

When it comes to everyday programming, I don't think theorem provers are at a point where they are particularly useful. Not everything needs to be proved formally, and I don't think this position is at odds with the belief that static type systems are generally "better" than dynamic ones.

Not really. Strong and expressive typing at its core is simply creating data packaging containers that have defined operations on them. It says nothing about logic. You may be referring to the functional programming aspect that comes with strong typed languages, which is related but not the same as strong typing.

The point is that typing is just a tool that a programer can use, whether its built into the language or ran statically like MyPy. You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. However, in the case of strict+explicit typing, the idea is that you wouldn't need tests in the first place, because your code would be correct by nature of compilation.

Some theorem provers, such as Coq, are not Turing-complete. This means you cannot write some programs, and in particular you cannot write infinite loops in Coq. Infinite loops are a common pattern (e.g., a REPL or a GUI display waiting for input).

This is a trade-off, as I said. You gain the expressive type system, but lose the ability to implement certain programming patterns. It has nothing to do with the strength of the type system.

---

> whether its built into the language or ran statically like MyPy.

All (true) type-checking is static, so MyPy "running statically" is not a noteworthy feature to distinguish it from other type checkers. I guess this point may seem trivial to some, but the broader context of this conversation involves conflation of the terms "static type system" and "strong type system", so your misuse of the word "statically" here seems worth pointing out.

That said, whether you use an external tool to check your types or the type-checker is built into the compiler is irrelevant, and I'm not sure why you brought it up at all.

---

> You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes.

Depending on the perspective, this is factually incorrect.

Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time. Writing tests to check for the absence of such errors is not equivalent, because you have not proved anything; you merely gain confidence. They are semantically distinct, even if you write many tests to gain a lot of confidence.

You are talking about languages, Im talking about the concept. The modern theorem provers aren't up to the task. Due to Rices theorem, you cannot "fully prove" a program, so a language that does this couldn't even exist. The strict typing however can be applied to subsets of the programming space, namely the data processing pipeline, whereas higher level stuff like the actual server code that does have an infinite loop to listen to requests can be written in whatever.

The point is that no language recommended for strong type safety today is anywhere fully complete to include the rigor of something like a theorem prover, and anything less then that is basically your own opinion on what is "good enough".

>Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time.

Run time errors are no different than compile time errors as far as testing is concerned. Its not like the computer blows up when you have a seg fault. And you absolutely can prove what you need for operation.

Say your input to your code is an HTTP request of length x. And output is some data processing on that request. You can write a test suite that is basically like this

1. Ensure that code returns a well defined error for x values outside of given range.

2. For all valid ranges in x, test all possible values of every byte in that range, and ensure correct behaviour.

While overkill, this will absolutely exercise every single piece of your code and prove correctness. You can also couple this with checking things like memory access

I'm not going to argue that these features are only possible because of dynamic typing, but regardless, statically typed languages tend not to have them.

Elixir may get "some form" of typing, but it likely won't be traditional static typing.

For Elixir, the concurrency model and supervisor trees. It's a perfect fit for some problems, and in general as a small company, the projects we use Elixir on greatly simplifies our production environment which is always a win.

Most of my focus when designing a project is to enable people with less experience than me to contribute in a bug-free fashion in the face of concurrency and parallelism. Sometimes that involves picking a funny language, sometimes it doesn't.

I've been writing code for 40 years, I can't estimate how many loc I've written, but likely over a million. One of my personal projects is currently over 65k loc vanilla js, and I never once had a problem with not knowing what type a function took. If you're so bad at naming things and knowing what a function does, I guess maybe types can help you. But not everyone needs it.

I think such a debate is largely unproductive. Like anything else, types have value (ha) and successfully capitalizing on that value depends on the context of the project, which includes things like developer experience, tooling, project complexity, requirements, deadlines etc.

The only productive outcome of these debates is that each developer gets to slowly and frustratingly build a list of pros and cons as they go through the arguments presented by either side debating this topic. In addition, developers who completely disregard either the cons or the pros are necessarily making subjective decisions with incomplete data, and the project gets to pay the price. Just because the developer is personally OK with all of their projects paying that price, doesn't mean it's the best decision for a project.

My experience has been that when starting out, projects get the most value out of not having types, and as they grow in scope and size, and the cons of not having types start creeping up, that's the point when gradually transitioning the code to being strongly typed allows the project to maintain its velocity _and_ quality.

Many years ago I thought that it's a good idea for a game math library to have separate strong types for 'point' (a location in 3D space) and 'vector' (a direction and magnitude in 3D space), and allow/disallow certain operations (e.g. 'point + vector => point' 'vector + vector => vector', 'point - point => vector', while 'point + point' is illegal).

Sounds absolutely great in theory, but in practice it was a royal PITA to work with, but it took me much too long to realize this (how can it be such a hassle when in theory it's such a good idea!)

I soon went back to a general 4D vector class (where a 'point' is defined by .w = 1.0, and a 'vector' by .w = 0.0), and some debug-mode runtime validation (which catches things like trying to add a point to a point).

Of course strong typing also often makes perfect sense, for instance in a 3D rendering API it should be a compilation error to provide a texture-handle where a buffer-handle is expected, but after this experience with points vs vectors (which should've been a classic showcase for strong typing) I would never again "die on that hill" :)

TL;DR: static typing: yes! strong typing: it depends.

Those help you more if you do a lot of math involving both them, but that’s also when it becomes a nightmare in most programming languages because of an explosion in the number of types.

Let’s say your code computes

  3km × 4hours

In many languages, you also have to write code to make that happen, and to make it have the same type as

  4hours × 3km

And that’s ignoring that you may

- encounter minutes, meters, yards, etc.

- want to use algorithms that compute exp(3km) or log(4hours). What types do these have? Here, you probably want to forget about string typing values.

The good thing about stricter typing systems is that it forces you to handle all the cases when you're doing a refactor like this before it compiles.

When changes to the data model happen in large codebases of dynamic code, it frequently gets shipped in a non complete state and turns into a production runtime error later down the line.

cries at the thought of insanitybit not respecting me

The feeling is mutual.

discussions are a two-way street. if you aren't getting it, then how do you expect someone else to "get" your position?

    "The whole problem with the world is that fools and fanatics are always so certain of themselves, and wiser people so full of doubts"

[edit: To clarify, i am on the "i like strong static typing most of the time but also understand their pros/cons wrt. dynamic languages" side of things]

I probably love assembly language more than C#, or C++, or any of the strongly typed languages I use.

Assembly language has no types. It doesn't pretend types even exist.

Are you going to look down on me because I like to write assembly language?

Nope.

Say you can do the project in 2 ways.

First way is to use a strongly typed language, think about the data, and design your code in the appropriate way. You code it up, go through the loop of compiling and fixing errors, and get your code to run.

The second way is to write your code in Python, without worrying about strong types. You complete the code quite a bit faster, but since you also want your code to be correct, you spend time writing an end to end test suit for your code.

The second approach is not only faster (since you are writing tests in both cases), its overall better. Spending time writing tests allows you to essentially validate things that modern mainstream strongly typed languages can't catch at compile time (for example, what happens when the input is unicode strings?). It also forces you to think about end to end behavior and making sure that is correct, rather than just the behavior within your code.

Strong typing is a simply hand-holding tool for programmers. If you cannot write correct code without it, you are on a fast track to being replaced by AI eventually. The future of programming is not going to be designing data structures and types, its going to be using English to generate large chunks of code in most likely Python, and then tweak fine details in those.

This is, in fact, MUCH easier to do with a strong test suite that only cares about input and output rather than internals.

The most common approach to starting a refactoring project is write or enhance a test suite to the point where there is no undefined behavior, either the program works or handles the appropriate errors.

You don't need to aim for 100% test coverage either, you just need your tests to cover all possible inputs (including fuzzing).

I honestly don’t know if we’ll still program by hand or not, but I do look skeptical at people who are very certain we won’t. Don’t think that’s the first time in history people make that prediction…

As far as adoption, there is a reason why dynamic type languages that feature a lot more natural syntax (Node, Python) are used WAY more than others.

also it's pretty ridiculous to say "static type systems are handholding" and then say the remedy is to write your code with AI ..

There's only explicit typing and implicit typing.

So the only real argument you're having with someone is when writing a piece of code, do they want the caller of the code or the input of the code's data type to be known or they want the data type to be a mystery to be figured out, occasionally in production when shit hits the fan.

> That said, yes, of course my post is arrogant and dismissive. I am outright saying I won't engage in a conversation. I'm comfortable with that.

This is an extremely toxic attitude. I wouldn't be interested in working with you in any professional capacity, on an open-source project, or having you as a friend, and as a matter of fact if someone expressed this attitude at work I would complain to HR.