You can reason and prove code to be correct in a dynamic language. What static typing gives you is compiler assisted proving. The cost of the compiler assistance is that you have to express the code in a way that often makes it more difficult for a human to understand.

> often makes it more difficult for a human to understand. Does it though? I guess it depends on the type system.

For example, when I find it hard to understand Haskell code, it's not because of the type system, it's usually that the compiler is doing too much magic for me (with type classes, and automatically lifting things into monads).

I find that having the types actually makes the code itself easier to understand, because I can ask the compiler (usually through the REPL) to tell me what kind of thing can go where. It makes that kind of information more local.

You can do it, but you don't. It's not a language thing, it's a culture thing.

Language like Haskell forces you to do it. It is more effort, but this effort pays off in getting composability and edge cases right. The end result is not actually harder to understand, it's rather that you did not fully understood the problem in the beginning (by glossing over technical details).

Ah but the thing is that the payoff is simply assumed. Nobody has actually shown this claim to be true. You spend more effort and you hope that there is a payoff. Yet you have things like Cabal that's as flaky as anything written in PHP. Clearly static typing isn't some magic pixie dust that all of a sudden makes all your code work correctly.

> Clearly static typing isn't some magic pixie dust that all of a sudden makes all your code work correctly.

Static typing itself - no. What is important about Haskell is the equational reasoning (algebraic thinking, if you will) you can do, not static typing. Static typing is just a vehicle to be able to pull it off.

There is a payoff already - see my comment to Lisp guy above. We could also talk about how monads made LINQ great, or how streams in Java have to be more complicated than necessary because the language wasn't very well formally defined.

And there will be bigger payoff in the future, when we will learn for example how to type a whole big software component correctly (like a web service). So far, it's an art driven by engineering intuition; but formalization will help to make more robust systems.

The payoff is also assumed based on experience with other branches of mathematics (as I was alluding in my first comment), where historically, the formalization always paid off. It doesn't mean you cannot get things right informally, but it's usually fiendishly difficult.

Again, you're making a lot of assertions in absence of any evidence to support them. One would think that this would be easily demonstrable seeing how long Haskell has been around, and yet no such evidence exists to my knowledge.

I think there is plenty of evidence (of how types help to design better APIs), you just don't want to accept it. I already mentioned LINQ and lens, another could be parser combinators and FRP (Observables in particular).

Recently there was an article about a whole application: http://abailly.github.io/posts/cm-arch-design.html

I can also recommend book Functional Programming in Scala, which talks about how FP helps develop good API in more detail.

Should I do Physics without units?

No, but nor do dynamic type advocates suggest using languages without types. They just suggest a slightly different notion of type.

The analogy is more "Should I do Physics without computer-verified usage of units?", in which case the answer is "It depends."