[c-cube]

Except, of course, that specs are only tested correct, not proven correct like types would be. Types (in a reasonable static type system, not, say, C) are never wrong. In addition, specs do not compose, do they ? If you call a function g in a function f, there is no automatic check that their specs align.

[travisjungroth]

> Types (in a reasonable static type system, not, say, C) are never wrong.

Oh man. This is the fundamental disagreement. Sure, you can have a type system that is never wrong in its own little world. But, that's not the problem. A lot of us are making a living mapping real world problems into software solutions. If that mapping is messed up (and it always is to some degree) then the formal correctness of the type system doesn't matter at all. It's like you got the wrong answer really, really right.

[lolinder]

> A lot of us are making a living mapping real world problems into software solutions. If that mapping is messed up (and it always is to some degree) then the formal correctness of the type system doesn't matter at all.

If I'm understanding you correctly, you're saying statically typed language can't protect against design flaws, only implementation flaws. But implementation flaws are common, and statically typed languages do help to avoid those.

[c-cube]

I'm not saying types always model your problem properly! That's not even well specified. I'm saying that "x has type foo" is never wrong if the program typechecks properly. That's totally different, and it means that you can rely on type annotations as being correct, up-to-date documentation. You can also trust that functions are never applied to the wrong number of arguments, or the wrong types; my point is that this guarantees more, in a less expressive way, than specs.

[travisjungroth]

You can statically analyze specs and check them at runtime if you want.

[c-cube]

Can you? Is there any tool that actually does that reliably?

[travisjungroth]

https://clojure.org/guides/spec#_using_spec_for_validation

[c-cube]

The words "static" or "analysis" do not appear there. I imagine you meant that you can runtime check the specs, which, well, is no replacement for a type system.

[cle]

> Except, of course, that specs are only tested correct, not proven correct like types would be.

Yes this is the fundamental tradeoff. Specs et al are undoubtedly more flexible and expressive than static type systems, at the expense of some configurable error tolerance. I don't think one approach is generally better than the other, it's a question of tradeoffs between constraint complexity and confidence bounds.

[undershirt]

Yeah, and I think this is obvious, but it certainly depends on the origin of the data being checked. We can prove the structure of “allowed” data ahead of time if we want guarantees on what’s possible inside our program. We also want a facility to check data encountered by the running program (i.e. from the user or another program.) which of course we can’t know ahead of time.

It is a design decision to be able to build a clojure system interactively while it is running, so a runtime type checker is a way for the developer to give up the safety of type constraints for this purpose—by using the same facility we already need in the real world, a way to check the structure of data we can’t anticipate.

[dgb23]

Yes, I think that is one of the big weaknesses of it. You can write specs that make no sense and it will just let you. So far there is also no way to automatically check whether you are strengthening a guarantee or weaken your assumptions relative to a previous spec. In a perfect world we would have this in my opinion.