Dynamic Specifications and Type Systems

Software engineering continues to accrue more and more responsibilities, as software is permeating every industry and every aspect of life. This necessitates the maturing of our craft towards the same standards we expect from the aviation or automotive industries. Luckily we’ve got powerful allies in the quest for safe and correct software. One of them is fields medal winner Vladimir Voevodsky, who works to lift our type systems to the next level - a level where it becomes reasonable to provide formal proofs for every bit of software we produce. Unfortunately, this is far from practical today, especially when modelling the intricate, asynchronous semantics of distributed systems. Additionally, though we do gain correctness and safety, increasingly declarative abstractions detach us from performance and execution considerations. Plus it never hurts to pursue an alternative.

Powerful type systems allow us to write our programs as if they were their own specifications and to then automatically prove certain things about these specifications. Through a heritage of thinking about programs as discrete mathematical objects, the quest for definite mathematical proof is as understandable as it is worthwhile. Sometimes we have to think of programs simply as artefacts of a very human engineering process and embrace the orderly approach to testing, improving and the inevitable faults that come with such a process.

We can already achieve tight, high-bandwidth feedback-loops, by utilizing tools like REPLs or Bruce Hauman’s excellent devcards. Especially the latter presents a very attractive vision of what modern program specifications could look like. What devcards lack in formal rigour, they make up for in other areas. A devcards specification can easily be shared with and understood by our clients and customers. And, at least for now, devcards are vastly superior when specifying primarily visual programs, like GUIs.

To this we add a first-class way of directly expressing a programs logic, constraints and invariants. One obvious tool would be something like miniKanren, which can be used from multiple host-languages. But any tuple store with a declarative query engine, like datomic, can provide most of this functionality. Again we gain the ability to specify our programs logic more directly and in a way that can be more readily shared and discussed with our client. Plus, a logic engine allows us to express much richer constraints than what is possible with the current breed of type systems. The resulting system would probably feel more like Design by Contract. I have started a small project to explore this application of logic programming.