As a working academic in programming languages, I’ve mostly resisted the urge to dive into proof assistants for my work. (As an academic, I mostly resist the urge to do anything that seems to be popular among my peers.)
Remarkably, the points he makes (almost a decade ago) are no less familiar today. I’m more familiar with ACL2 than Coq, but it seems each tool has its own issues when it comes to learning curve.
Reading his summary makes me wonder if making major investments in IDE/UI technology (perhaps proof state visualization?) would help.
Visualization as a debugging aid helps, and in this case I guess it complements seamlessly with the way stepwise development in Coq presumably works (I’m no expert). For example, there is prooftree for Proof General.
In between the extremely specific “proofassistants” tag (estimate: one post per week) and the useful but extremely general “compsci” tag (estimate: 10 posts per week), I was thinking “formalmethods” (estimate: 3 posts per week) would be a useful middle ground.
Tactic language often gets lauded as being far superior to raw proof tree construction (Coq-style versus Agda style), but I just don’t see it. Literally: tactics obscure the exact thing you are working with by attempting to relay, only interactively, the state of partial proof trees on goal-state. Of course Agda proofs are more laborious, and I can’t as easily list out my free variables at every scope, but putting that into your interactive “assistant” bit seems more natural.
So what gives? Well, Agda has only a limited auto “tactic”, and no Chlipala-style sledgehammer. Those are really nice to have at times when you want to just elide an obvious proof as obvious.
What’s really missing is that even the auto mode on Agda doesn’t quite give you what you want. I think I want a “macro system” where my appeals to auto are made explicit (without sacrificing speed) and also without tossing the proof tree out entirely.
Really, though, I think this is just a large UX design space and I’m excited to see provers get more “mainstream” so many eyes can really make light work of gathering the needs of the practical “prover’s” workflow.
As a working academic in programming languages, I’ve mostly resisted the urge to dive into proof assistants for my work. (As an academic, I mostly resist the urge to do anything that seems to be popular among my peers.)
Remarkably, the points he makes (almost a decade ago) are no less familiar today. I’m more familiar with ACL2 than Coq, but it seems each tool has its own issues when it comes to learning curve.
Reading his summary makes me wonder if making major investments in IDE/UI technology (perhaps proof state visualization?) would help.
Visualization as a debugging aid helps, and in this case I guess it complements seamlessly with the way stepwise development in Coq presumably works (I’m no expert). For example, there is prooftree for Proof General.
There’s also the work in Fstar which has some interesting tooling around it. Also has an MSR Cambridge connection.
This is actually about Coq. I was not sure what tags to apply, wish there was one for automated proof assistants.
Yeah, I’d really like one for formal methods in general. @jcs, possible?
People have generally put such topics in “compsci.”
In between the extremely specific “proofassistants” tag (estimate: one post per week) and the useful but extremely general “compsci” tag (estimate: 10 posts per week), I was thinking “formalmethods” (estimate: 3 posts per week) would be a useful middle ground.
Also recently applicable to this other story.
Tactic language often gets lauded as being far superior to raw proof tree construction (Coq-style versus Agda style), but I just don’t see it. Literally: tactics obscure the exact thing you are working with by attempting to relay, only interactively, the state of partial proof trees on goal-state. Of course Agda proofs are more laborious, and I can’t as easily list out my free variables at every scope, but putting that into your interactive “assistant” bit seems more natural.
So what gives? Well, Agda has only a limited
auto“tactic”, and no Chlipala-stylesledgehammer. Those are really nice to have at times when you want to just elide an obvious proof as obvious.What’s really missing is that even the auto mode on Agda doesn’t quite give you what you want. I think I want a “macro system” where my appeals to
autoare made explicit (without sacrificing speed) and also without tossing the proof tree out entirely.Really, though, I think this is just a large UX design space and I’m excited to see provers get more “mainstream” so many eyes can really make light work of gathering the needs of the practical “prover’s” workflow.