| > My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one. Sure, it's possible to prototype in the untyped lambda calculus too, or in Brainfuck. Why would you want to though? > I am not arguing against their use, just what seemed to be your assertion that it is impossible to prototype/develop software without an automatic type checker. I never said it was impossible, I merely implied that it was bizarre to even want to do so (among other things). Programming is hard enough as it is, why waste your time and mental energy checking properties that can be checked for you? > I was talking about a programmer with a type theory, not implementing an automatic type checker from scratch. A type theory in their head, in the intuitionistic sense, that they check as they're programming, not one that's actually checked by a tool is what I assumed. And certainly you're working within limitations dictated by your language, but you can take typically it further than most think. See for instance, the paper lightweight static capabilities. |