how clojure.spec.alpha validation correctness is reasoned about?

Question

Hi!
I am exploring an implementation of clojure.spec.alpha and found out a rather "little" (according to my naive expectations) set of tests :)

Clojure spec defines a set of primitives being able to compose one with each other.
Another words Clojure spec defines a language to describe structure + its predicative properties.

Assuming that spec semantics is described informally in Rationale and Guide how do you reason about the correspondence between declared semantics and spec implementation?

I expected a huge set of tests covering basic scenarios and finite number of their compositions -- kinda induction base. And if induction base is true then other compositions are also ok.

how do you reason about verification of the clojure.spec.alpha validation implementation correctness?

UPD: narrowed the question context to validation aspect according to Alex Miller first answer.

Answer 1

Are you asking primarily about validation, conformance, description, or generation?

Comments

let's define a `validation` as a primary context

---

The base layer of validation is predicate based and largely reuses predicates from Clojure. Those predicates themselves are largely simple and correct by definition (as they are the same predicates used by Clojure itself). For example, strings are checked by string? which checks that an object is an instance of java.lang.String. So there are not a ton of those kinds of tests in spec - we leverage an existing working base.

For building up, there are generally not a ton of cases per construct, but https://github.com/clojure/spec.alpha/blob/master/src/test/clojure/clojure/test_clojure/spec.clj is testing compositions of primitives to cover them. Certainly, doing more would be better, but would really like to spend some time eventually on generatively creating specs and values for testing (but this is tricky without spec!).

---

"Certainly, doing more would be better, but would really like to spend some time eventually on generatively creating specs and values for testing (but this is tricky without spec!)"

Does it make sense to generate specs _somehow_ then generate values via generated specs generators and validate values via generated specs?
As a result problem of values generating is resolved by using generated spec generators what brings coupling for sure on the whole generators logic layer so validation responsibility is not tested in isolation.