> Bad point. Type checkers only check fairly simple properties of your program.<p>Bad bad point. There are statically-typed languages with fairly complex type systems. There are even dependently typed languages which check essentially <i>any</i> property of you values and can be used to prove your program correct.<p>> Most of the work in making sure that your program is correct [...] goes into developing comprehensive tests.<p>Tests can only show the presence of bugs, never the absence of them. This is not me speaking, this is Dijkstra.<p>It is ok to prefer one method over the other, but there's clearly an aura of opinion on the statements of this article. It would be better for the reader to explicitly differentiate fact from opinion there.
An important point of using dynamic types is not mentioned:
The actual workflow of coders: Compile, run, fail, repeat vs. eval, fail, repeat.<p>After over 35 years of coding - mostly with statically compiled languages -doing it REPL-style makes such an enormous difference in my enjoyment of the profession.
I'm not sure I can go back to a compiler.
I really hope that in the future gradual typing and dependent types can come together into an ergonomic to use system where we can let the compiler check/enforce proofs of correctness, but not require them. There's a ladder of correctness (simple type checks, unit tests, integration tests, proofs of different aspects of correctness) and each has a tradeoff vs effort. It would be really great to be about to be able to move around it without rewriting much code, but rather by adding more and more annotations as needed for your use.
A thread from 2014: <a href="https://news.ycombinator.com/item?id=8594079" rel="nofollow">https://news.ycombinator.com/item?id=8594079</a><p>2009: <a href="https://news.ycombinator.com/item?id=556794" rel="nofollow">https://news.ycombinator.com/item?id=556794</a>
I have some noob questions that I don't know how to ask:<p>What, if any, is the relationship between type systems and pattern matching?<p>Does structural typing reduce the need for instanceof style tests?<p>So if a language uses structure typing, is pattern matching not useful, applicable?<p>--<p>Thanks for humoring me. I'm mostly a Java programmer, self taught, no CS background. I've been reading wiki articles about type systems, trying to figure out what it all means, how to get started. Inference, structural vs nominal, linear types... But, honestly, my eyes glaze over pretty quickly.<p>Am planning on powering thru Appel's 2002 book, especially implementing the type system, but we'll see how far I get.
This is an implementation of something similar on Smalltalk:
<a href="https://www.youtube.com/watch?v=1b3RRE9a8NA" rel="nofollow">https://www.youtube.com/watch?v=1b3RRE9a8NA</a>