I’ve written about an idea for a graphical interface to dependent types before. I just played with Coq a little bit, and it’s really fun. I spend 45 minutes proving that every number can be written as either 2n or 2n+1. A feeling of accomplishment washes over me as I finish proving the most substantial result in mathematics history!
Still, the fun of using this system only makes me want to explore this idea more! I like the presentation in the right panel, but I hate the interaction with it. I have to memorize the syntax for a bunch of tactics, typing sequential commands for something that are essentially non-sequential transformations. It’s hard to go back and forth between programming and proving, it’s hard to divert your attention elsewhere for a while. An interface where I could just right click on a hypothesis and see all the ways I could productively transform it would be great in itself.
Damnit! I want a good flexible gui library! I want reactive to be working!