Guidelines for advocacy for Coq and Coq-community

[palmskog]

Many Coq-community members regularly do advocacy for Coq itself, for Coq-community, type theory, machine-checked proofs, Coq libraries, Coq-verified software, and so on. It helps to have guidelines about how to best perform advocacy. This is just meant to start a discussion, but I can see at least the following (example) issues:

Terminology

• Coq is a "proof assistant", or "interactive theorem prover" (not just a "theorem prover" or "program verification tool")
• Coq is based on "propositions-as-types", or "Curry-Howard correspondence", but perhaps not "Curry Howard isomorphism"(?)

Realism and Honesty

• Coq has had several critical bugs, but theorems certified by Coq still have (much) higher trustworthiness than manual proofs, and self-certification efforts are underway
• There are many proof assistants with different foundations and capabilities, so a general ordering from "best to worst" should be avoided, but comparisons on concrete, objective, and user-relevant metrics are important for development progress.

The bottom line is that I think we should aim to include high-quality community-written advocacy guidelines in some form in the manifesto repository.

[spitters]

This initiative may be worth mentioning, and being expanded on: https://popl20.sigplan.org/details/CoqPL-2020-papers/2/The-use-of-Coq-for-Common-Criteria-Evaluations

…

On Tue, Jan 28, 2020 at 8:59 PM Karl Palmskog ***@***.***> wrote: Many Coq-community members regularly do advocacy for Coq itself, for Coq-community, type theory, machine-checked proofs, Coq libraries, Coq-verified software, and so on. It helps to have guidelines about how to best perform advocacy. This is just meant to start a discussion, but I can see at least the following (example) issues: Terminology - Coq is a "proof assistant", or "interactive theorem prover" (not just a "theorem prover" or "program verification tool") - Coq is based on "propositions-as-types", or "Curry-Howard correspondence", but perhaps not "Curry Howard isomorphism"(?) Realism and Honesty - Coq has had several critical bugs <https://github.com/coq/coq/blob/master/dev/doc/critical-bugs>, but theorems certified by Coq still have (much) higher trustworthiness than manual proofs, and self-certification efforts <https://github.com/MetaCoq/MetaCoq> are underway - There are many proof assistants with different foundations and capabilities, so a general ordering from "best to worst" should be avoided, but comparisons on concrete, objective, and user-relevant metrics are important for development progress. The bottom line is that I think we should aim to include high-quality community-written advocacy guidelines in some form in the manifesto repository. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#90?email_source=notifications&email_token=AABTNTS333UJBHXLF3C73JTRACFCZA5CNFSM4KMYL2V2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IJKRAFA>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTXAGZABJKWAYO24NJTRACFCZANCNFSM4KMYL2VQ> .

[palmskog]

One more note on terminology. The community has for some reason embraced mechanization or mechanised or mechanical [proofs] as common keywords and descriptors.

I think it's much better to empasize machine-checked [proofs] instead, since it's bound to cause less confusion for outsiders.