Stream: Coq users

Topic: Proofweb


view this post on Zulip Théo Zimmermann (Oct 19 2022 at 10:53):

I had no idea that ProofWeb was still used today. Too bad it's stuck at Coq 8.2 :fear:

view this post on Zulip Alessandro Bruni (Oct 20 2022 at 07:40):

Théo Zimmermann said:

I had no idea that ProofWeb was still used today. Too bad it's stuck at Coq 8.2 :fear:

Yes, it's terribly out of date and in dire need of some care. I wouldn't know where to start though, since I believe they are patching Coq to extract the proof trees. It would be nice to make it work against vanilla Coq, possibly even jsCoq...
The positive side is that people like it, and it can give a first introduction to formal reasoning and proof checkers without the need to explain all the intricacies of Coq, yet it's easy to later sell Software Foundations to those who want to dive into the details. And it's very well documented. I've yet to find something that matches it, even though many ad-hoc tools exist for this purpose.


Last updated: Mar 28 2024 at 20:01 UTC