I thought I’d scribble something about what we’re up to. The team (Pierre-Évariste Dagand, Adam Gundry, Peter Morris, James Chapman) have been hard at work. I have been otherwise engaged. As a result, there has been considerable progress. Don’t worry. I expect I’ll mess things up properly over Christmas.
We’ve decided that the best way to get our new type theory out there for you to play with, sooner rather than later, is not to wrap it up in a new version of the Epigram language, but rather to present it as is, in a low-budget command-driven interactive proof assistant. This is beginning to materialise.
One of the good things about having new people in the team is that they’ve had to learn about how we get this stuff to work, and they’ve been writing down what they’re learning in the Epitome. Literate Programming Considered Essential. We’re not trying to take over the world: we’re just trying to make stuff worth stealing. That’s an unusual optimisation problem.
So, the rumours of our death have been slightly exaggerated. My plan is to continue staying out of the way of the coders and write more articles about How It All Works. We’re plotting a bit of a New Year hacking hooley in Tallinn (Glasgow isn’t cold enough). There might be a thing that does something a bit after that.
I’m hoping that this blog will wire up to the new repo real soon, so that you can peer on in. Afore I go, though, let me remark on the importance of Haskell as an enabling technology. Our engineering philosophy is do it once: we prefer to write one abstract piece of code which captures a concept than many concrete pieces of code which follow a pattern; without higher-kind types and classes, we’d be hosed. Given that our main implementation problem is (or rather, was) No Programmers, it is only because of Haskell that a thing exists at all.
Yay. Glad to hear that progress is being made on this.