I can use strong typing productively. I can use dynamic systems _way_ more productively.

When all things are equal, the impedance is not from lack of skill. It is staring at you straight in the face: it's a rules-based type prover that -- by definition -- significantly restricts the set of valid programs.

This is the definition of a type prover.

The argument should be that the value of this restriction outweighs the cost. But no one is yet making this claim. Which should make one wonder.