Coq will be renamed into 'The Rocq Prover'
Coq, a formal proof management system for mathematical proofs and programming language certification, will be renamed "The Rocq Prover" by late 2024, with community support and a dedicated Stack Exchange site.
Read original article
Coq is a formal proof management system that allows users to write mathematical definitions, algorithms, and theorems, facilitating the development of machine-checked proofs. It is utilized in various applications, including the certification of programming languages and the formalization of mathematical theorems. Users can access Coq through its Reference Manual and Standard Library, with tutorials and books recommended for beginners. Coq can be run directly in a browser using jsCoq, or installed on a local system. The Coq community is active, contributing to formal developments and tools, and engaging through forums and chat platforms. Coq is open-source, primarily developed by Inria, and encourages contributions from users in various forms, including financial support through the Coq Consortium. Recently, the Coq team announced plans to rename the software to "The Rocq Prover," with a new visual identity and website expected by the end of 2024, along with the first release of Rocq. Additionally, a Stack Exchange Q&A site for Proof Assistants has been established for users to ask and answer questions related to Coq.
- Coq is a formal proof management system used for mathematical proofs and programming language certification.
- The software will be renamed to "The Rocq Prover" with a new identity expected by late 2024.
- Users can run Coq in a browser or install it locally, with extensive community support available.
- Coq is open-source and encourages contributions from both academic and industrial users.
- A dedicated Stack Exchange site for Proof Assistants has been launched for community engagement.
Related
Show HN: Qq: like jq, but can transcode between many formats
The GitHub repository hosts `qq`, a tool using `jq` query syntax and `gojq` for configuration format transcoding. It offers interactive query building, multiple format support, and encoding performance focus. Installation options include source or releases. Contributions welcome.
OCaml for the Skeptical (2006)
OCaml tutorial covers installation, syntax, data types, functions, control structures, error handling, and more. It explains type inference, pattern matching, and compiling applications. Updated on 17 June 2006.
Co-Dfns v5.7.0
The Co-dfns Compiler project enhances Dyalog dfns with task parallelism, synchronization, and determinism for optimized code and improved reliability. Contact arcfide@sacrideo.us for inquiries. Contributions and support are welcomed.
LeanDojo: Theorem Proving in Lean Using Language Models
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches. It includes benchmarks and enables interactive proof state observation, improving automation and discovering new proofs.
LeanDojo: Theorem Proving in Lean Using LLMs
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches, and includes benchmarks for training machine learning models in theorem proving.
15 commentsI'm not part of the Coq community so I've got no strong opinions on this. But I do know I've often heard people saying GIMP could do with a better name.
> No option receives more likes than dislikes.
So the new name was just "the least bad" option. Naming things is hard and getting a community to agree on a name is surely that much harder still, but I still find it a bit sad that the new name is not well-liked.
That being said context matters too, I still refer to loading a round into a gun's chamber as cocking a gun.
I've never had an issue referencing the project's name in a professional environment, where most of my colleagues are unfamiliar with it.
We all appreciate various kinds of humor, in the right contexts.
But this software seems like something used in professional and academic contexts.
Including professional and academic contexts with a history of sometimes being unwelcoming to women. Who might not want to be reminded of old boys' club locker room phallic humor insensitivity throughout each day as they work.
So, the new name is going to seem like doubling-down, by those who didn't understand all the problems with the previous name, or didn't consider them problems.
I think this is one of those things we sometimes do out of lighthearted intention, with no harm intended, and only later realize and regret.
Now's a chance avert some harm and regret.
They have a typo on the side, it's `The Rocq Hard Prover`
Related
Show HN: Qq: like jq, but can transcode between many formats
The GitHub repository hosts `qq`, a tool using `jq` query syntax and `gojq` for configuration format transcoding. It offers interactive query building, multiple format support, and encoding performance focus. Installation options include source or releases. Contributions welcome.
OCaml for the Skeptical (2006)
OCaml tutorial covers installation, syntax, data types, functions, control structures, error handling, and more. It explains type inference, pattern matching, and compiling applications. Updated on 17 June 2006.
Co-Dfns v5.7.0
The Co-dfns Compiler project enhances Dyalog dfns with task parallelism, synchronization, and determinism for optimized code and improved reliability. Contact arcfide@sacrideo.us for inquiries. Contributions and support are welcomed.
LeanDojo: Theorem Proving in Lean Using Language Models
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches. It includes benchmarks and enables interactive proof state observation, improving automation and discovering new proofs.
LeanDojo: Theorem Proving in Lean Using LLMs
LeanDojo enhances theorem proving in Lean with retrieval-augmented language models, introducing Lean Copilot for tactic suggestions and proof searches, and includes benchmarks for training machine learning models in theorem proving.