It seems like every talk or interview coming from Rich ever since Cognitect started hawking clojure.spec contains at least a handful of poorly supported, vague, dogmatic claims about static typing in opposition to…well, “how Clojure does it.”

I’m not too familiar with clojure.spec, but I know a bit about the overall idea of it. Let me see if I can explain the difference between static types vs clojure.spec from a formal methods perspective (which differs a little from the PLT perspective).

Clojure.spec is a contract system. A contract is a formally specifiable property of the code, usually as pre/postconditions on functions, that you expect the code to follow. You’re able to, through the contracts alone, specify the complete behavior of the function via specs. For example, using Deadpixi Contracts in Python:

@require("l must not be empty", lambda args: len(args.l) > 0)
@ensure("result is head of list", lambda a, result: result + tail(a.l) == a.l)
def head(l: List[T]) -> T:
    return l[0]

With this we have that head is only specified for nonempty lists, and also that its result will always be, in fact, the head of the list. This is not something we can do with the type system of Python, or even the type system of Haskell, as the type of head is indistinguishable from the type of last. We’re calling all sorts of other functions and can, in fact, run arbitrary code. In fact, we can completely decouple the specification of contracts from the verification of them. This is both a strength and a weakness. The strength is that we get both expressive power and flexibility. The weakness is that expressive power is usually a bad thing. In the general case contracts are unverifiable due to the halting problem.

In practice, there’s four approaches to verifying contracts:

1. Restrict yourself to a subset where you have simple, automatic static verification. For example, you might not be able to autoverify “this function will be called only with positive even numbers”, but we can autoverify “this function will be called with only integers”. This gives us static typing! I think you could reasonably argue that “type systems are special cases of contract systems”, but that’d get you stabbed to death in 99% of programming forums out there, so uh yeah
2. Limit verification to throwing runtime errors. Every time a contract comes up, check if it’s correct, and throw an error if isn’t. Most contract-oriented languages combine this with static typing to get “conventional” contract systems. You can do a lot of cool stuff with this. Eiffel’s AutoTest can turn your runtime contracts into integration tests, Ada can place contracts on global mutations, most systems let synthesize contracts into dynamic types, etc.
3. Formally prove the contracts correct. This is formal verification. A lot of people are doing this in different ways: Dafny uses pre/postconditions and loop invariants, Liquid Haskell uses refinement types, Idris uses dependent types, etc.
4. Informally prove the contracts correct. This is how we get Cleanroom, which is actually a lot more effective than you’d think. People write the contracts, attach english “proofs” of why they hold, and everybody verifies them through code review.

So, in summary: contracts generalize static types in a form that is good in some ways, bad in others. There are multiple different styles of contracts, just as there’s multiple different type system, but the unifying idea is that they can fully specify the program’s behavior. In verifying them is another matter, and clojure.spec’s approach is “runtime checks” as opposed to most other languages, which reduce the specification power in return representing contracts as static types.

It seems like every talk or interview coming from Rich ever since Cognitect started hawking clojure.spec contains at least a handful of poorly supported, vague, dogmatic claims about static typing in opposition to…well, “how Clojure does it.”

I haven’t been paying all that much attention to the talks more recently, but this is also how I feel about it. There are trade-offs between static types and specs, and specs have some advantages over types, but because of all the straw-man arguments it’s hard to find useful analyses of the trade-offs.

I fail to see what’s vague or dogmatic about his statements. He’s basically saying that types primarily focus on checking internal self consistency, while what you really care about is semantic correctness. Expressing semantic correctness using types ranges from being difficult to impossible depending on the type system. At the same time static typing can introduce a lot of complexity that’s incidental to the problem being solved. You often end up writing code in a way that facilitates static verification as opposed to human readability.