search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Guidelines for advocacy for Coq and Coq-community #90

Open palmskog opened 4 years ago

palmskog commented 4 years ago

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

Realism and Honesty

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 commented 4 years ago

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 notifications@github.com 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 https://github.com/coq-community/manifesto/issues/90?email_source=notifications&email_token=AABTNTS333UJBHXLF3C73JTRACFCZA5CNFSM4KMYL2V2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IJKRAFA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTXAGZABJKWAYO24NJTRACFCZANCNFSM4KMYL2VQ .

palmskog commented 4 years ago

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.