> it's just that the world is moving toward statically typed languages with sophisticated type inference
The billion lines of Javascript, Python, Ruby and R would like to differ.
Each of the first three has probably more users than all languages (ML family, haskell, scala) with an advanced type system combined.
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.
The billion lines of Javascript, Python, Ruby and R would like to differ.
Each of the first three has probably more users than all languages (ML family, haskell, scala) with an advanced type system combined.
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.