The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/19/2016 07:08 PM, Pierre-Marie Pédrot wrote:
> On 20/02/2016 01:00, Jonathan Leivent wrote:
> > Thanks, Robbert.  Unfortunately, I guess this means "not without a
> > plugin".  Instead, I'll just define hopefully enough numbers via
> > Notations...
> Out of curiosity, what prevents you from writing / using a plugin?
>
> PMP

1. I don't have all of the necessary instructions.

2. I want my project to be usable by Coq novices who know even less 
about plugins than I do.  One goal of my project is to try to make Coq 
(and dependent-type language-based proof assistants in general) more 
appealing as a tool to software developers who otherwise wouldn't 
consider using a proof assistant, because they might believe the costs 
outweigh the benefits.  Hence, keeping the bar as low as possible is ideal.

3. Writing plugins does not appear to me to be as safe or maintainable 
as directly using the existing UI.

4. Stressing the UI (Ltac, commands, etc.) allows me to find more bugs, 
more opportunities for UI enhancement, and so forth - and in this way, 
perhaps contribute ever so slightly to nudging the UI towards a future 
less in continuous need of plugins.  After all, not all Coq users should 
have to become Coq developers.

These are subject to change...

-- Jonathan