So after some off-line discussions, while I continue to feel like the natural-deduction based judgmental methodology really maybe isn't the best way to do the work of experimentally developing logics (you really want the sequent calculus version for that - but that's another post), it's an excellent storytelling device. The idea is that it should help you explain a logic that is initially non-intuitive to an audience that you're trying not to scare off.
I'm not even certain how fully I believe that, since I tend to like using sequent calculus presentations for more-or-less everything that isn't a programming language. However, this tech report, by forcing me to work through a lot of things very carefully, has clarified my views on a lot of things - in particular, I think I have a "modern formulation" of the judgmental methodology that neatly generalizes to things like substructural logics without going out of its way, while simultaneously doing a good job of putting on paper all the tricks I learned from Dan about formalizing logics in Agda.
My wildest hope is that this story can motivate to Random J. PLPerson not only what Bernardo and I are doing specifically, but also give the intuition behind a number of things I've learned from Noam Zeilberger and Dan Licata about the philosophy behind both higher-order focusing and behind doing logic in Agda, and without actually requiring any background with focusing or knowledge of Agda to get there. I'd be happy to hear from you whether you think I've succeeded: any criticism would be greatly appreciated. (Draft Technical Report: Constructive Provability Logic)
Reactions to "Purely Functional Retrogames"
1 hour ago