No one is saying there is no cost. The cost of using static types is (1) you have to think about type info when writing the code and (2) you have to fix compile-time type errors while you are developing. The poster is claiming that, over time, as code bases tend to grow large, this small investment yields increasing (not diminishing) returns; a claim I would agree with.

Well, the easy answer is that dependently-typed languages like Agda and Idris aren't very mature yet. They're still missing many commonly-needed libraries, compile times are slow, the tooling isn't great, etc etc.

Getting a language to the point where it's workable for serious projects is a lot of work. Rust is getting there with the backing of Mozilla, Haskell has made some decent strides too (but still has a way to go, and I think has some pretty fundamental flaws entirely apart from the type system). It'll be probably another decade at least before we see any dependently-typed languages getting a serious foothold, but I do think they're going to become a lot more common eventually.

Have you used them? Switching to a language like Agda or Idris is entering the realm of formal verification because the types are so expressive. It's completely different to what most programmers are used to.

Essentially the types being used as so complex the type checker cannot automate the decision about two types being compatible so you have to write maths proofs to help. The types used in mainstream languages are simple enough that the type checker never needs help like that.

The cost of formal verification right now is immense but the benefit is close to bug free code. Mainstream strong statically languages require nowhere near the same amount of effort and give clear benefits over dynamic types.

While this is a valid point, it's also worth remembering that if you have a data structure of sufficient complexity that writing out its type is cumbersome, then your data is still in that structure whether you choose to be explicit about it or not. Any code reading or modifying some element within that data still needs to correctly find that element, and if writing out the types is a burden then probably finding the correct location every time is also difficult. So if anything, when you have more complicated data structures flying around, and particularly if you work with several similar but different complicated structures, that could make having the types explicit much more useful for ensuring correctness and maintainability.

Highly templated C++ is the highway to hell. If you haven't heard C++ templates are turing complete and so can also have the halting problem.

Semi-automatic refactoring tools is just one part of what a type system enables. A much bigger benefit in my opinion is that it immediately highlights issues in your code while you are refactoring. Basically answer "What do I still need to change to finish the refactoring?". Unit testing also gives you some of this, but is typically much slower - both in execution time, and the additional time it takes to figure out where the issue is.

When using languages with static typing amount of refactoring of that type is disproportionately large, so people notice how much the ide helps, without noticing that most of the help wouldn't be even necessary without the complexity added by static types.