[kazinator]

> I 've done a little playground-style OCaml coding and the feeling you get with OCaml is that once your program compiles, it most likely also runs correctly.

This is only a feeling. Without carefully testing the code to exercise its cases, all you know is that they are properly typed.

For instance, suppose we write a complicated function (or group of functions) which goes through a block of intermediate code (output of a compiler) and assigns registers to all the temporaries, introducing memory spills in situations where more variables are live than the available registers.

We might have a feeling that because this code compiles, it must be free of problems such as accidentally assigning the same register to two variables which have overlapping lifetimes.

That feeling is poorly supported by reality; it is the "safyness" of static typing.

Untested code is garbage. And thorough testing is difficult to impossible, so there is a bit of garbage in almost all software, unfortunately.

Statically type checked code has all of its code paths effectively tested by the compiler, but those tests have only the limited point of view of trying to show that the program contains a trivial type mismatch, a close cousin of the syntax error. These "tests" are not actually feeding values into the code and trying to make it fail or behave incorrectly with respect to its specification.

[cle]

I mostly agree. In an increasingly distributed, decoupled, non-monolithic, service-driven world, where service interfaces are dynamically-typed and applications are data-driven, static typing doesn't add much value. And the sophisticated type systems, that can provide better guarantees than relatively primitive type systems like Java, are quite difficult to understand and use correctly. I expect that we'll see more and more type modeling bugs as static type systems become more feature-rich and complicated.

Static typing is extraordinarily useful in large company settings, where you may own a library that is used across the company, and you can quite easily understand how your library is used in other codebases and can confidently make cross-cutting emergent patches.

I'm pretty optimistic in the direction that Clojure is heading with clojure.spec. The ideal that I hope it reaches is "inductive" type safety, where you can prove your program is typesafe with a certain probability. And the tradeoffs you get by relaxing the deductive properties and timeliness of static typing are vastly simpler expressiveness, composability, testing, etc.

[rkrzr]

> Statically type checked code has all of its code paths effectively tested by the compiler

The type checker just ensures that a program is well-typed (i.e. free of type errors).

The better the type system the more program properties can be encoded in it and the more errors it can catch (up to the point of proving correctness of your program).

But you are right that type checking alone is no substitute for testing. They are orthogonal concepts and both should be employed to ensure that your programs behave correctly.

One nice thing of statically typed languages is that they can automatically generate some tests for you, like e.g. the QuickCheck library for Erlang and Haskell.

[marcosdumay]

They are not orthogonal at all. Both verify your code against invariants. While the typing system tries to prove an invariant holds, a test tried to prove that it does not hold.

That means that false positives are the problem for typing systems, while false negatives are the problem for tests. But that's the biggest difference you will find.

One does even replace the other.

[jeremiep]

Clojure has quickcheck as well: https://github.com/clojure/test.check

[rkrzr]

Good point. Of course you have to specify the type of the values that you want to test in the test itself then, so you have to specify some types one way or the other.

[jeremiep]

You can feed those types from clojure.spec now :)

[jxm262]

I've actually felt this same way for a while now. This past year or so I've worked hard (imo) to "get" the benefits of strong typing, but can't shake the feeling that the tradeoffs just aren't worth it. I was hoping the verbosity, complexity, etc (strong types), would give me more confidence and security in my code. It always seems like a false sense of security though and I'm currnently on the fence as to whether or not it's worth it.

Is there any studies done showing that strong typing is actually a disadvantage? I've seen some stating the opposite, but nothing really stood out to me. Sorry for the long rant, but at this point I can't find anything empirically stating one is better than the other.

[kazinator]

Static typing (and other static checks) will reduce the round trips between editing and running. Some of your typos that are not syntax errors get caught and reported to you. Of course, you were going to test that code anyway. But you avoided a bit of wasted time. However, this advantage can be eroded by the trade offs.

Interesting experience recently: I added static checks to a Lisp dialect which report warnings for all occurrences of unbound variables and functions. (Not type checking, but a very basic static check). According to static proponents, bugs of this type should exist left and right if we don't have the check.

Only one instance of an unbound variable was found in the dialect's standard library: and that was a function that was added as an afterthought and never tested. The problem reproduced 100% when calling the function in any correct manner whatsoever; the function was completely broken. If it had been called just once after having been written, the problem would have been caught.

I fixed the problem so that the warning went away and caught myself almost starting to think about commit the fix, when I realized: what am I doing? I still haven't called the function. Gee, it now passes the one feeble static check that was added, so it must be correct? Haha.

[justinhj]

For me the only downside of strong typing is that code takes longer to write. It's reminiscent of my years writing C++ where often fiddling around with header files, type declarations and templates would seemingly take up more time than the actual logic of the program. For the last few years I've been working in Scala and compared to Clojure it can take longer to knock out working code. That said with the help of type inferencing and IntelliJ it is nowhere near as slow as C++ was, and now I find that the benefits of strongly typed code greatly outweigh the costs in terms of syntax and development speed.

[yawaramin]

> ... type declarations and templates would seemingly take up more time than the actual logic of the program....

Just a small point: type declarations are part of the actual logic of the program. In type theory, types are logical propositions and values are proofs of those propositions.

[Nekorosu]

This is really interesting idea. It feels obvious when you get it but I've never thought about it and I've never seen it before.

[mpweiher]

> That feeling is poorly supported by reality; it is the "safyness" of static typing.

Has that become a thing now? :))