[pfdietz]

SBCL has fine type checking. Some is done at compile time -- you get warnings if something clearly can't be type correct -- but otherwise when compiled with safety 3 (which people tend to make the default) types are checked dynamically at run time. You don't get the program crashing from mistyping as one would in C.

[mapcars]

> You don't get the program crashing from mistyping as one would in C.

Sorry but I don't compare to C anymore, I want the same safety as in Rust or Typescript: exhaustive checks, control-flow type narrowing, mapped types and so on. Some detection at compile time is not enough, since there is a way to eliminate all type errors I want to eliminate them all, not some.

[guenthert]

Why stop there? Why not demand proof of correctness? After all, that's now within reach using LLMs producing the formal specification from a simple prompt, right?

SBCL does a fine job in detecting type mismatches within the frame of ANSI Common Lisp, not Haskell. While I would agree that a strict type system eases long term maintenance of large systems, for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way. And if such proof-of-concept looks promising, then there is no shame in rewriting it in a language more suitable for scale and maintenance.

[mapcars]

Proof of correctness would be fantastic, but I have yet to see it in action. LLMs maybe could do it for simple program, but I'm pretty sure it will fail in large codebases (due to context limits), and types help a lot in that case.

> for "explorative computing", proof-of-concepts, RAD or similar that tends to get in the way

I would even argue that its better to have typed system even for POCs, because things change fast and it very often leads to type errors that need to be discovered. At least when I did that I often would do manual tests after changes just to check if things work, with typing in place this time can also be minimised.

[streetfighter64]

> You don't get the program crashing from mistyping as one would in C.

Uh, isn't that exactly what happens with runtime type checking? Otherwise what can you do if you detect a type error at runtime other than crash?

In C the compiler tries to detect all type errors at compile time, and if you do manage to fool the compiler into compiling badly typed code, it won't necessarily crash, it'll be undefined behavior (which includes crashing but can also do worse).

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