I've spent a lot of time hanging out with pretty hardcore type theory people, and have never seen any of them recommend a dependently-typed language to a new programmer. In other words, you're pretty blatantly fighting a straw man.
It's not about how experienced the programmer is. The problem is that people do a bate and switch when it comes to type theory, promising the benefits of dependent types even though there are no production languages that deliver these benefits.
I've similarly never seen anyone promise the benefits of dependent types when talking about simpler type systems. Why would they need to? Much simpler type systems already have more than enough benefits to be worthwhile.
I'm not actually looking to debate you, your mind is made up and there's very little chance I'll change it, not that it would matter if I did. I mainly just want to point out for others reading this that your arguments are blatant straw men.
>Much simpler type systems already have more than enough benefits to be worthwhile.
If that's your opinion, why did you ignore the fact that I addressed this in my original post? You accuse me of having a straw man argument, and yet you can't even engage with what I've written?
Anyway, you're right that neither of us is likely to convince the other, but I have really seen arguments that go like the one I described, and you're really doing me a disservice by ignoring the details of what I posted.
You "addressed" it by referring to "studies" that you didn't cite. There are studies that go both directions on the question, none of which have good enough methodology to be worth more than a tiny update in either direction. Most of the studies are about extremely weak type systems (C, Java, etc.), and therefore don't provide any evidence at all about type systems that are stronger than Java but weaker than dependent types (e.g. Swift, Rust, Haskell, etc).
Meanwhile we have a lot of people who have used both weak type systems and strong type systems who claim that strong type systems make their jobs dramatically easier, and we have a lot of people who have only used weak type systems who claim the opposite. Take a survey of people who have actually done non-trivial work using a language with a good type system, and you'll get very clear results about their view of the benefits. Clearly an RCT would be better, but given that training takes a long time, that just isn't feasible.
