Are Clojure's specs equivalent to Wadler's propositions?

Question

Wadler wrote an amazing paper: Propositions as Types - where he talks about the Howard-Curry correspondence, that you can check program behaviour in terms of the types of the program. (For a given subset of languages).

Recently Rich Hickey released Clojure spec, for defining data and function specifications.

Here the commentator writes:

from Wadler we have that props ≅ types, specs ≅ props -> types ergo can do static spec/contract/type checking.

My question is: Are Clojure's specs equivalent to Wadler's propositions?

Answer 1

Defining Terms

Propositions as Types is specifically talking about the isomorphism that exists between Natural Deduction and the Simply Typed Lambda Calculus (STLC), two formalisms for logic and programming languages respectively. What this means is that when you are programming in the STLC, you can convert your programs into a proposition of logic.

For example, these are equivalent:

(a -> b) -> a -> b

P implies Q
P
therefore Q

The first is a type signature for a function, the second is a logical proposition. Now when you "Are Clojure's specs equivalent to Wadler's propositions?" what you are asking is "can we convert Clojure specs into statements of logic?" or because of the isomorphism, "can we convert clojure specs into the STLC?"

Lack of Equivalence

Specs allow us to use any and all Clojure predicates. This makes spec incredibly flexible, but it is also the key to seeing that specs are not propositions.

One of the key features that makes the STLC work as a logic is that all terms reduce or in other words, all programs in the STLC terminate. Clojure does not have this property, it is easy to write Clojure programs that will never terminate. In order for any programming language to be a consistent logic, it must have this termination property, because "non-termination" is equivalent to contradiction in logic. Since specs can use any Clojure function, you can write a spec that does not terminate and hence cannot be translated to the STLC. So Clojure specs are not equivalent to Wadler's propositions.

What is different and what is similar?

As the docs of Clojure spec states, spec is not a type system. Specs are not concerned with proof, but types are. Types restrict the programs we can write to those that can be statically proven to 'go right'. Type systems come in various levels of power and expressivity, but sound type systems prove certain properties about your code.

Specs do not prove properties about your code, but instead try to give you confidence that your code works and visibility when it does not. Specs cannot be run statically, they are fundamentally about runtime values and the relationships between them.

But even with these differences, types and Clojure specs serve similar pragmatic purposes, both of them give us more confidence in our code, they allow us to encode semantics into our function definitions, and both can help aid us in test generation to help us prevent bugs from creeping into our code.