The problem with Coq

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!

7 thoughts on “The problem with Coq

  1. Have you tried coqide ? It has some bits of mouse interaction. It’s not that much easier than typing directly, but it helps with the tactics’ syntax.

  2. That’s not the problem with Coq. The problem with Coq is it’s name. Every other bug in Coq pales into insignificance compared to the choice of name ;)

  3. I think that a real problem here is that *proving is hard*. :) E.g.:
    > I have to memorize the syntax for a bunch of tactics
    I don’t have, I use pure lambda terms and ‘refine’ only — much simpler. But I can’t say it’s easier. There are many tricks to make life prettier but no silver bullet.

  4. beroal: you do have a point. I often complain that “dependent types are too hard”, but maybe that’s because maths is hard. But I actually find coq quite a bit easier than other systems I have used, and mostly dislike the style of interface. . I would prefer not to have a sequential text file at all, and treat proofs in a more, um, tangible(?) way.

    Which is why I’m looking into the coq core so I can build my own interface on top, for experimentation.

  5. Hi. I know it’s too late to bring this up. But as time passes, I’m getting more and more convinced that you are right and a proof-assistant needs a different GUI than CoqIDE has. I’d like to read links in your post by they do not work (‘a’ without ‘href’).

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s