I have habitually measured the "strength" of type systems by feeling. My feeling is roughly based on how often I see type verification discussed in the communities.
My ranking is (from weakest to strongest):
Assembly
< C
< Perl = Python = Ruby = JavaScript = Lisp
---- Dynamic above vs. Static below ----
< Java = Go = SQL
< Scala = OCaml = Haskell = C++ = Rust = TypeScript = Elm
< Idris = Lean = Coq = Isabelle
Just as you point out that types are for people, I think most of type system is about culture. After all, one language's compile time is just its compiler's language's runtime, and a Turing complete runtime is capable of any checking. Lean prover is written in C++, but rarely do C++ users put as much care into their types as Lean prover users (who are mathematicians).
That care translates to better ergonomics, and better ergonomics in turn lead to more people caring. I have heard rumors about some C++ programmers writing their templates in Haskell first so that they don't have to suffer the C++ template error messages.
In my opinion, TypeScript really offers a unique window into the intersection of the two cultures. I am really surprised by some complicated type signatures necessary in TypeScript to accommodate dynamic JavaScript code. It is probably the first time that a static type system of a dynamic typed language is adopted widely enough to demonstrate such a direct contrast and provoke such confrontation, which I believe will ultimately lead to more awareness and improved quality.
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
XD I quivered at the mention of "categories".
I have habitually measured the "strength" of type systems by feeling. My feeling is roughly based on how often I see type verification discussed in the communities.
My ranking is (from weakest to strongest):
Assembly
< C
< Perl = Python = Ruby = JavaScript = Lisp
---- Dynamic above vs. Static below ----
< Java = Go = SQL
< Scala = OCaml = Haskell = C++ = Rust = TypeScript = Elm
< Idris = Lean = Coq = Isabelle
Just as you point out that types are for people, I think most of type system is about culture. After all, one language's compile time is just its compiler's language's runtime, and a Turing complete runtime is capable of any checking. Lean prover is written in C++, but rarely do C++ users put as much care into their types as Lean prover users (who are mathematicians).
That care translates to better ergonomics, and better ergonomics in turn lead to more people caring. I have heard rumors about some C++ programmers writing their templates in Haskell first so that they don't have to suffer the C++ template error messages.
In my opinion, TypeScript really offers a unique window into the intersection of the two cultures. I am really surprised by some complicated type signatures necessary in TypeScript to accommodate dynamic JavaScript code. It is probably the first time that a static type system of a dynamic typed language is adopted widely enough to demonstrate such a direct contrast and provoke such confrontation, which I believe will ultimately lead to more awareness and improved quality.