The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 8/21/21 8:20 PM, Talia Ringer wrote:
> I remember watching you live prove during DeepSpec 2017. It's quite 
> possible that the example was manufactured since it was educational, 
> but one thing that stood out was that in trying to extend 
> program-specific custom tactics to handle changes, you first made 
> changes within individual proofs, then figured out how to bubble those 
> changes out into your tactic going forward.
Yup, that's how I'm used to seeing this style of proof scripting work well.
> LLMs I think could be very helpful for figuring out those changes 
> within individual proofs, but as of now, it is likely that a human 
> would still need to observe that such repetition is occurring, then 
> figure out how to generalize it inside of the custom tactic 
> implementation.
That would certainly be magical if a machine-learning-based tool could 
figure out the "fundamentally new" step missing from a proof! My cartoon 
model says it's only the steps that already more-or-less exist elsewhere 
that would be suggested.  I don't think of generalization of the 
specific step into a tactic script as particularly labor-intensive; it's 
finding the specific step that bottlenecks the process.
> Though, I'm not certain of that; I think it would be a really 
> interesting exercise for you to find someone with Copilot access, pick 
> a project you're working on, and just hack with Copilot on for a long 
> time, and see what it's good at and what it struggles with for your 
> own style (with an extremely open mind, remembering that it ought to 
> get better over time).
>
> I'd be interested in a more systematic exploration of this for 
> different proving styles if you're interested; I think it’s important 
> to know as we head toward a future where these language models for 
> programming and proving become much more widespread.

I'm skeptical about the long-term value of this sort of tool, for 
programming in general, with proof scripting in Coq as just one case.  
That doesn't mean these tools won't catch on like wildfire, even if they 
are actually part of local optima that are pretty easy to improve with 
the kind of thinking that we appreciate as logicians.

Specifically, I've seen these tools make up reusable and generalizable 
units of code by analyzing many examples.  I hypothesize that results 
would be much better with humans providing the reusable units, as 
well-documented library functions, classes, tactics, whatever.  
Especially when it is realized via verbose copy and paste of code, 
automatic generalization strikes me as a crutch to make up for 
weaknesses in design of languages and/or libraries.  It seems pretty bad 
for code readability.

Machine-learning-base search to build combinator trees, using explicitly 
declared libraries, could be a best of both worlds, though, quite 
possibly applicable in proof assistants.