&gt; it&#x27;s just that the world is moving toward statically typed languages with sophisticated type inference<p>The billion lines of Javascript, Python, Ruby and R would like to differ.<p>Each of the first three has probably more users than all languages (ML family, haskell, scala) with an advanced type system combined.<p>I love dependent typing, I truly do. But the right tool for the job, and a formally verified coq program is certainly suited for a rocket, but not for the high iteration and velocity environments most people program in.