I’m always interested in declarative style programming. I’m often left thinking about the implications this has for testing. How do I test that I’ve described something right? Maybe a couple unit test-esque sanity-checks? Maybe describe it twice - like double-entry bookkeeping?
Describing it twice is a actually a great method, even though it seems redundant. For example, you could have an algorithm which is tricky to implement but quite efficient, then assert that it’s equal to a function which is extremely simple to implement, but inefficient.
The real magic comes in when you’re able to specify your function in such a way that only a single implementation is possible. That way the type-checker (i.e. proof-checker) verifies it for you, which is what this article is actually doing (the test part in the title is a little lie).
In this case, Z3 was used to find a particular number that satisfied a bunch of constraints. I would be curious to see it used to write more general functions as well.
The title “Test-Only Development” reminds me of the field of inductive programming, where algorithms author computer programs for you, given things like input/output pairs.
It’s an interesting topic. One example of such a thing is Magic Haskeller which takes input/output pairs and constructs Haskell functions around them.
Another weird and interesting one is ADATE, written in OCaml, which runs a genetic algorithm over abstract syntax trees to construct functions that satisfy the provided input/output pairs.