The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

To be fair to the state of the art, Ltac has clearly demonstrated its viability as a tactics framework. Indeed, this mailing list has many subscribers whose productivity in Ltac is legendary.

Anecdotally, as an ordinary user coming at Coq from the outside, Ltac was the hardest part to learn. The basic idea is simple enough to understand, but going from that to scalable, maintainable, readable frameworks is a skill unto itself. I don’t know about others on this list, but I find Ltac definitions incredibly hard to read when browsing other people’s code.

Against a backdrop of “some people are stellar with Ltac” and “some find it inhibiting,” long term the big question is: what changes could be made to yield improvements in productivity writ large?

A tactics system that’s built to support proof DSLs doesn’t seem like a crazy idea to me - it seems more like a natural generalization of the state of the art. Ltac is already a monad (morally speaking), why not make that explicit? Monad transformers are super handy things, why not explore their uses here?

Will those ideas pan out? Real world, the answer is probably going to be “yes for some teams, no for others,” same as when we ask whether language X is the “best language” (or more broadly, technology X). Hoping for one environment/approach to rule them all is something I’m sure we all do, but historically computing doesn’t usually go that way. We’ll see!

Sent from my iPhone

On Jan 2, 2020, at 5:45 PM, Beta Ziliani <beta AT mpi-sws.org> wrote:



Talking about tactic languages, I agree with Adam that proof engineering is a young field, and we are still finding what are the good abstractions. But Ltac is *very* limited to explore these, and this limitation is what got me into the Mtac projects: I wanted to have good programming practices in my proofs, and Ltac is clearly not up to the task. Lean's way, if it is not the ideal, at least is pointing in the right direction. Same or different language, that's not really important. What matters is what you can do with it.

My 1ct.

Beta

On Thu, Jan 2, 2020 at 9:16 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi, the UW user study mentioned earlier is here: http://tlringer.github.io/pdf/analytics.pdf

It's a start (I say as the first author), but it will not answer every question you have. The infrastructure and data are public. We really, really hope the lessons we learned and the data and infrastructure will help other people with future user studies. Our main goals were to encourage user studies in the Coq community, and figure out some ways to improve automation.

We didn't do this study for Lean, but hopefully the lessons for how to conduct these user studies generalize enough to help people outside of just the Coq community. Within Coq, unsurprisingly, some of our users wrote a lot of custom tactics, while some wrote few or none. This is not in the paper, but the data should show this, though you will need to write an analysis to crawl the data and figure out how often those users defined new tactics. More interesting might be how often users messed up while defining those tactics, how much time they spent tweaking tactics, and so on. 

A controlled study across proof assistants for tactic development would be very challenging given the small number of users in our community and the difficulty of controlling for other variables. But I hope to see people at least try this kind of thing.

Anyways, if you care about any of this, please come to our CPP talk. A lot of what I want is to start a community discussion on how we can run better user studies.

---

With respect to reducing the number of languages: I'm also not sure it's a win, but I do think that one thing Kevin is getting at that is nice is being able to write new commands without using the plugin system or modifying Coq itself. And believe me, I am probably the most enthusiast plugin developer in the community. But when you build a plugin, even for something simple and really universal like the use cases Kevin mentioned, it is very difficult to get users. 

The particular commands Kevin mentioned maybe aren't necessary in Coq, but I've had people ask me to implement functionality before that I already had implemented and exposed as a Coq command in one of my plugins. Getting developers to use new tools is always hard. Getting developers to use libraries is less hard. It would be nice to be able to write commands directly inside of Coq once in a while, at least for relatively simple things. (The plugin system should still exist alongside that.)

On Thu, Jan 2, 2020, 3:33 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 1/2/20 6:00 PM, Kevin Buzzard wrote:

On Thu, 2 Jan 2020 at 21:55, Adam Chlipala <adamc AT csail.mit.edu> wrote:

I'm not sure I understand this point.  Ltac works well for most kinds of
tactic programming.  At least, I don't see how it could be held not to
meet the binary requirement of "a rich programming environment with
useful abstractions."

I am not a computer scientist and I don't have much experience with Coq,

but with Lean you only need to learn one language not two,

It's not clear to me that reducing the number of languages is a clear win, when we often design new languages to better suit different use cases.

and as well as

writing tactics people have been writing things like linters, new commands

which tell you which namespace you're in, which namespaces are open,

what variables you have and so on, stuff which makes the end users life

a bit easier.

At least in Coq, I feel like all of the above kinds of queries are obviated by the default display in proof mode.  I get the feeling "namespace" means something different and more subtle in Lean, though.  (And I've never seen the need for a "linter" in mechanized proof, especially for experienced users.)

In general, I think it's a mistake to compare proof assistants using
criteria associated with random varieties of open-source projects, since
typically open-source projects are much less involved in major
design-space innovations.  IMO, worrying about quality of library
ecosystems should mostly be avoided.

When mathematicians come looking at these systems, one of the first questions

they seem to ask is "how much mathematics is in there already?".

I think today it makes a lot more sense for pure math vs. program verification to try to codify the existing shared knowledge base, since it's so much better-established.  One issue with program verification is that it brings in different kinds of scalability challenges, such that it no longer makes sense to think in terms of "which famous theorems are proved," but rather "which tools are available for new verifications."  Tactics can be just as important as theorems, and they very rarely correspond neatly with decision procedures.