[aconz2]

> Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data.

I've never bought this line of thinking when the "Clojure folks" also say "code is data", because then a syntactic type signature you write down is also just data. If you want to consume the type signature (or spec signature or whatever) as syntax (as a sibling comment suggests), use a macro or any other program which consumes programs.

The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time.

Lastly, I strongly disagree these approaches are meant as a replacement for static typing or formal verification because (as far as I can tell) a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program. This is also in contrast to Racket contracts, which will give you the correct blame information between parties using and not using contracts.

[ComNik]

You make a very good point, the comparison was flawed there.

> The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time.

This is a better way to put it. The second important factor for me is expressiveness. With spec or any other contracts-like system one gets the full power of the language to express constraints. Of course type systems are not artificially restricted in this regard, they simply make a different trade-off.

I hope my comment did not come off as a riff on static vs dynamic typing, and I don't think any contract system is meant to replace type systems. Until expressing all important program specifications formally becomes viable for everyone (maybe through this work https://www.math.ias.edu/vladimir/current_work?), a less-formal, dynamic approach seems very attractive.

[aconz2]

I hear you on expressiveness of using the language. Of course (and as you mention) the strength of restricting the expressiveness is that it becomes decidable in some amount of acceptable time for most programs.

I agree with your last sentiment but I don't think it has to be any less "formal" than something like Coq. I just think we shouldn't be so concerned with proving all properties of a program before running. And then we can turn the knob to adjust how much to prove during vs. before running.

[pron]

> a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program

The spec is just metadata. How it's used is part of the tooling. I see nothing precluding using specs in tools that employ and analyze that information in different ways.

[aconz2]

Yep you are totally correct. I only point this out because the tool presented here does not do the same thing as other contract systems, but could (as you say) be used as a building block to get there.