[naasking]

> Is in inconceivable that a programmer can check their types manually, using an ad hoc intuitive type system?

Sure, if you don't mind an ad-hoc, informally specified, bug-ridden, slow implementation of half of a type checker that no one but you knows (and so is "intuitive" only to you... until you read this same code 3 months later).

[kmill]

What are you addressing? My position is that automatic type checkers are nice to have but not essential, and it is possible to prototype software without one. 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. Anyway, I understand the pitfalls of not using one, but I also understand how type systems tend not to capture everything. There is no reason to be dogmatic about it: use whatever works as a tool for thought.

As I said before, "intuitive" is in the sense of intuitionism; not "easy to understand" or "obvious." A point of view: formal type systems comes from explaining what we see with mental perception (intuition). What do you do if your automatic type checker doesn't check every possible thing you want to verify is correct? Surely you aren't just blind to the types they "should" be. Seeing the invariants which must hold is seeing the intuitive type.

> if you don't mind an ad-hoc, informally specified, bug-ridden, slow implementation of half of a type checker that no one but you knows

I can't tell if I was understood or if you just wanted to quote Greenspun's tenth rule whether it completely worked or not: I was talking about a programmer with a type theory, not implementing an automatic type checker from scratch.

[naasking]

> 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.