An Interpreter of the Algebra of Programming in MiniKanren
This means bringing the act of programming or analysis of programs to a place where it feels similar to manipulating polynomials or doing an integral. Make things point-free, in other words use combinators or make it categorical. This simplifies the equational reasoning.
An important side effect of this is that programs become perhaps offputtingly concise. This is important if you intend to manipulate a program with pencil and paper, because you will need to copy a significant portion of it for every new line of your deduction. There is something also to sheer syntactic mass being an obstruction to thought. It is good or at least interesting to consider what happens when you can fit an entire complex program on a line or screen. It changes the game. I remember Aaron Hsu saying this about APL, a bug that has not yet bit me. Combinators may take inspiration from traditional list combinators like fold, combinator calculus like SKI, or category theory. Depends on your backwards and predilections.
A second aspect that is interesting is to extend functional programming to relational specification. One has a sense that the concept of a mathematical function is a relatively nice fitting abstraction to the computers we’ve got. Functions are a special case of relations that are completely defined over the domain and deterministic. General relations feel in some sense farther from an implementation, but the extra oomph you get for tight concise specification of a problem is worth it, which can then be refined into a functional implementation.
