Sure - but the point is that there are /diminishing returns/ on type-systems. The question is then, /where/ should one draw the line when trying to prove certai

Sure - but the point is that there are /diminishing returns/ on type-systems. The question is then, /where/ should one draw the line when trying to prove certain properties of code; which properties are worthwhile proving? Are you /seriously/ suggesting that one should use Agda or Coq for most code? EDIT. The original comment was suggesting as though dynamic and static type-systems are a dichotomy. I was pointing out that it is a sliding scale from nominally-typed ala Go, all the way to dependently-typed languages; and that's not even including model-checkers!