I’ve been exploring ways to leverage type-driven development and value constraints for better testing. Turns out this has already been done, and there is a whole category of proof-oriented programming languages.

Prior Context

My explorations started between experimenting with Scott Wlaschin’s approach to designing with types and Clojure’s unique optional type system, clojure.spec.

Scott’s type-driven approach creates guarded domains with little internal defensive programming. Types are used to limit input to constrained values validated at the edge of the domain.

This seemed to cross over with Clojure.spec, which is an optional type system that also allows constrained types. For example, you might make a type InventoryCount that can only be an integer between 0 and 100. These types are enforced dynamically by methods in Design by Contract style Clojure also uses this constraint information to automatically test type-annotated functions with random data.

Clojure’s automatic generative testing had me wondering

  • What does this automatic generative testing measure or prove?
  • How can type-driven approaches similarly leverage constraint data?

I previously explored the first question, and concluded that such tests are an approximation of totality (all inputs properly map to valid outputs).

Turns out the second question has already been explored and has very interesting answers.

Proof-Oriented Languages and Formal Verification

Mark Seemann was kind enough to point me to several existing languages. Turns out that there is a whole category of languages that have considered program verification with constrained types, or more generally with dependent types.

Some are not turing-complete, and are primarily tools for proving assertions in conjunction with other languages, like Coq. Some are only meant for formal math proofs.

Others, like Idris and F* are turing-complete languages.

These languages take advantage of the constraints on types and functions to prove facts about the program. For example, ensuring that a function is pure (no unadvertised effects or state) and total (works for all advertized input). F* says it can verify security properties and bounds on resource usage!

This is a whole new world of design- and compile-time assistance. It changes my view of what can be verified statically. I haven’t experimented much with these languages yet. However, I sense programs are difficult to write so formally, just like the rigor necessary for math proofs is difficult to learn. I’d guess one wouldn’t want to write a whole conventional program in this style. Still, this is an incredible tool for writing critical components with high confidence!