The Coq mailing list

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

On 8/18/21 11:24 PM, Talia Ringer wrote:

I'm thinking a bit ahead to the grad seminar I'll teach in the spring (starting in January) which I think I'll have complete freedom over. I really want to do a proof automation course, where one day every week is a deep dive on a single paper, and the other is hacking on the paper artifact. I was thinking this outline:

[...]

8, 9: ATP for ITP

10, 11: neural networks for proofs

I'm really curious on the community's thoughts regarding stable/usable artifacts in these categories.  My collaborators and I actually haven't found any!

There have been research papers on SMT bridges for Coq (heck, I think I built the first one myself as a student), but we find that they all fall over when used for significant program verification.  That is, we hit blocking issues (performance scaling or otherwise) that make the maintainers say "yeah, that would be really hard to fix."

The neural-networks angle has been a popular point of discussion since deep learning became hot, but I don't think I've yet come across someone using such a tool who isn't also one of its primary authors.

    You can carefully curate experiences using rickety tools in a
    course, but it would be nice if students could expect stepping
    outside the lines to go well.