[unshavedyak]

> People are far too obsessed with static type checking. A lot of this time would be better spent invested in live debugging tools.

I mean.. the two are tightly related. The type represents the outer bounds of values possible. Types will give you as much utility as you put into them (or as the language allows).

I agree in general, i just think you massively undersell types haha. It's not either or, it's AND. Always AND.

[steve_adams_86]

I agree. Even with excellent debugging, I think types will allow me to need to debug less. This seems ideal, because debugging means things are breaking.

Types also mean that I can describe my program in ways others can understand and trust. I don’t want to pass off potentially broken programs to other people and say don’t worry, the debugging experience is great.

[ohyes]

Types have always been a hard sell for me. I honestly never have issues with types being wrong when I write code, and I understand that this is missing the point. The point is that the types define a very concrete interface and we know up front when the interfaces break, and can statically check that the interface is correct everywhere.

I feel that mathematical types are so far distant from the type system of something like C or C++ that the term foot guns itself somewhat.

[hinkley]

I've worked with too many people who insist there's nothing wrong with the way they are coding, while I've had conversations with 4 different people who have gotten tired of having to clean up after them.

I can't take anyone's word anymore that a tool is useless because they don't need it. We as humans need tons of things we pretend that we don't. It's positively pathological.

[ohyes]

Yeah I don’t think that my point was that I don’t need types, but more closer to yours that I’ll never really have an objective way to know if I need types.

[Groxx]

it feels like a category error of sorts too.

types describe all possible values. a debugger observes one value.

they're fundamentally different things, and are useful in different ways. sure, sometimes they overlap, but not always.

[ahzhou]

Types are just human and machine readable documentation - orthogonal to debugging IMO.

Great typing, like great documentation or great design, helps with debugging - but that’s not the main goal.

[DonaldPShimoda]

> Types are just human and machine readable documentation

This is only possibly true in the context of languages with poor static typing ecosystems, and even then I don't think I fully agree.

When a type-checker admits a program, it is because it has proved the program to be free from certain classes of errors. The more expressive your type system, the more elaborate and precise your claims about your program's behavior can be. This is fundamentally distinct from providing documentation that tells your users "please don't input values outside this range".

Early type systems (like C's) are woefully incapable of any serious specification. Modern type systems are significantly more expressive, and are therefore significantly more capable than you suggest. Types in the context of these expressive type systems are logical propositions, and the programs we write are their proofs.

[mycall]

Type theory has applications far beyond readable documentation. It is the basis for modern science.

[hinkley]

If you're trying to simulate a combinatorial explosion of possible states, reigning in the possible values would certainly help with maintaining that illusion.