nothing like having dynamic types manage your money

In OO languages (Java, C#, C++, etc...), and functional ones (F#, Haskell, OCaml, etc...) types do not validate the correctness of logic, they evaluate the correctness of data structures and their access/mutation as they are manifested in the language.

OO languages consider data correctness as access patterns of encapsulated primitives (or other data structures) through defined behaviors on a "class".

Functional languages consider data correctness as access patterns which preserve previous version of data which a caller may still need to reference, or another part of the system references. Functional languages (in most cases) disallow direct mutation without some sort of immutability or persistence.

Types have little (or nothing) to do with program correctness, or data correctness as it relates to external storage engines and their concurrency guarantees (i.e. FoundationDB, PostgreSQL, MySQL, etc...).

Therefore, in this scenario, what matter's most is the correctness of underlying storage (including the rigor of validating expected behavior) and the event sourcing/messaging systems, not on the internal data structures and their idioms conveyed by the language.

lmm

> In OO languages (Java, C#, C++, etc...), and functional ones (F#, Haskell, OCaml, etc...) types do not validate the correctness of logic, they evaluate the correctness of data structures and their access/mutation as they are manifested in the language.

Nonsense. Types validate whatever you use them to validate, which can certainly include what we usually call "logic".

> Types have little (or nothing) to do with program correctness

On the contrary, they're still the most effective technique we've found for improving program correctness at low cost.

Jach

Agree that you can use types to express and prove logical properties via compiler; it can be a fun way to solve a problem though too much of it tends to frustrate coworkers in JavaLand. It's also not exactly "low cost"; here's an old quip I have in my quotes file:

"With Scala you feel smart having just got something to work in a beautiful way but when you look around the room to tell your clojure colleague how clever you are, you notice he left 3 hours ago and there is a post-it saying use a Map." --Daniel Worthington-Bodart

> On the contrary, they're still the most effective technique we've found for improving program correctness at low cost.

This is not borne out by research, such as there is any of any quality: https://danluu.com/empirical-pl/ The best intervention to improve correctness, if not already being done, is code review: https://twitter.com/hillelogram/status/1120495752969641986 This doesn't necessarily mean dynamic types are better, just that if static types are better, they aren't tremendously so to obviously show in studies, unlike code review benefit studies.

My own bias is in favor of dynamic types, though I think the way Common Lisp does it is a lot better than Python (plus Lisp is flexible enough in other ways to let static type enthusiasts have their cake and eat it too https://github.com/coalton-lang/coalton), and Python better than PHP, and PHP better than JS. And I prefer Java to PHP and JS. Just like not all static type systems are C, not all dynamic type systems are JS. Untyped langs like assembly or Forth are interesting but I don't have enough experience.

I don't find the argument that valuable though, since I think just focusing on dynamic vs static is one of the least interesting division points when comparing languages or practices, and may be a matter of preferred style, like baseball pitching, more than anything. If we're trading experience takes I think Clojure's immutable-by-default prevents more bugs than any statically typed language that is mutable by default; that is, default mutable or default immutable (and this goes for collections too) is a much more important property than static types or dynamic types. It's not exactly a low cost intervention though, and when you really need to optimize you'll be encouraged by the profiler to replace some things with Java native arrays and so on. I don't think changing to static types would make a quality difference (especially when things like spec exist to get many of the same or more benefits) and would also not be a low cost intervention.

Some domains also demand tools beyond type proofs. i.e. things like TLA+. I think adding static types on top of that isn't very valuable, similar to adding static types on top of immutable-by-default isn't very valuable.

Last quip to reflect on. "What's true of every bug found in the field? ... It passed the type checker. ... It passed all the tests. Okay. So now what do you do? Right? I think we're in this world I'd like to call guardrail programming. Right? It's really sad. We're like: I can make change because I have tests. Who does that? Who drives their car around banging against the guardrail saying, "Whoa! I'm glad I've got these guardrails because I'd never make it to the show on time."" --Rich Hickey (https://www.infoq.com/presentations/Simple-Made-Easy/)