Conor McBride: Epigram 2: Autopsy, Obituary, Apology
Source: Mathematics and theoretical computing seminar
Conor McBride (University of Strathclyde)
The talk will be recorded and posted online.
Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted several times in the late 2000s and never even reached cruising altitude. This talk is absolutely not an attempt to persuade you to start using it. Rather, it is an exploration of the ideas which drove it: proof irrelevant observational equality, first class datatype descriptions, nontrivial equational theories for neutral terms. We may yet live to see such things. Although the programming language elaborator never happened, the underlying proof engine was accessible via an imperative interface called "Cochon": we did manage some interesting constructions, at least one of which I can walk through. I'll also explore the reasons, human and technological, why the thing did not survive the long dark.