[pfdietz]

> Uh, isn't that exactly what happens with runtime type checking?

No, it raises an exception, which you can handle. In some cases one can even resume via restarts. This is versus C, where a miscast pointer can cause memory corruption.

[streetfighter64]

Again, a proper C compiler in combination with sensible coding standards should prevent "miscast pointers" at compile time / static analysis. Anyway, being better than C at typing / memory safety, is a very low bar to pass.

I'm curious in what situation catching a typing exception would be useful though. The practice of catching exceptions due to bugs seems silly to me. What's the point of restarting the app if it's buggy?

Likewise, trying to catch exceptions due to for example dividing by zero is a strange practice. Instead check your inputs and throw an "invalid input" exception, because exceptions are really only sensible for invalid user input, or external state being wrong (unreadable input file, network failures, etc.).

[pfdietz]

If "just don't do the bad things" is a valid argument, why do we need type checking at all?

Exceptions from type checking are useful because they tell you exactly where something has screwed up, making fixing the bug easier. It also means problems are reduced from RCEs to just denial of service. And I find (in my testing) that it enables such things as rapid automated reduction of inputs that stimulate such bugs. For example, the SBCL compiler is such that it should never throw an exception even on invalid code, so when it does so one can automatically prune down a lambda expession passed to the COMPILE function to find a minimal compiler bug causing input. This also greatly simplifies debugging.

A general reason I look down on static type checking is that it's inadequate. It finds only a subset, and arguably a not very interesting subset, of bugs in programs. The larger set of possible bugs still has to be tested for, and for a sufficient testing procedure for that larger set you'll stimulate the typing bugs as well.

So, yeah, if you're in an environment were you can't test adequately, static typing can act as a bit of a crutch. But your program will still suck, even if it compiles.

The best argument for static typing IMO is that it acts as a kind of documentation.

[streetfighter64]

That's very silly, because in languages that do static type checking right, like Haskell, Rust, or to a lesser extent TypeScript, if you have a typing bug your program won't even compile. How's that "just don't do bad stuff"?

> It finds only a subset, and arguably a not very interesting subset, of bugs in programs. The larger set of possible bugs still has to be tested for, and for a sufficient testing procedure for that larger set you'll stimulate the typing bugs as well.

I agree that having your program be properly typed is a minumum requirement for it to even be possibly correct. So why would you not check that requirement statically? Skipping it is akin to not checking the syntax at compile time, instead preferring to crash at runtime due to invalid syntax. Or worse, throwing an exception. And then you're supposed to catch the "missing parenthesis exception"?

If you're building a bridge, presumably you'll calculate the forces and everything, before putting it together and verifying it actually holds for those forces. Likewise, if I specify that my function f returns a positive integer, why would I not let the compiler check that assumption statically? Are you really saying you'll write a test like (assert (> (f) 0)) or whatever? Seems like a huge waste of time building the app and starting up the test suite, when you could just as well just have stopped the build when the compiler saw you were returning the wrong type.

> For example, the SBCL compiler is such that it should never throw an exception even on invalid code

What does this even mean? What does it do if you run (/ 1 x) where x = 0?

> So, yeah, if you're in an environment were you can't test adequately, static typing can act as a bit of a crutch. But your program will still suck, even if it compiles.

This is a ridiculous argument, and is much closer to "just don't do the bad things" than what I said. Also note that I never said "don't write tests". You're making a complete strawman by pitting type checking against testing. It's two complimentary methods of verifying correctness, and the type system is a quicker and more accurate way of catching bugs, so moving all logic that you possibly can to the type system and away from tests is a huge win in efficiency and correctness. That doesn't mean skip testing, just like checking the syntax of your program statically doesn't mean skip testing.

Just because I'm wearing a seat belt (type checking) doesn't mean I'll drive recklessly (skip testing). Likewise, just being a careful driver (writing tests) doesn't mean you should stop wearing your seat belt (type checking).