From 5c05a5da5438d815f4a38d88561a2ffe61b0edad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Oct 2024 09:15:31 +0200 Subject: [PATCH 1/2] [roadmap] rework performance item --- text/rocq-roadmap.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/rocq-roadmap.md b/text/rocq-roadmap.md index 9a0303c4..1f19a50a 100644 --- a/text/rocq-roadmap.md +++ b/text/rocq-roadmap.md @@ -10,9 +10,9 @@ While Rocq leverages the rich heritage of Coq, it embraces a more agile developm This roadmap outlines our vision for Rocq's future, focusing on four key pillars: + **Open and Accessible**: The Rocq Prover provides user-friendly installation, comprehensive educational resources, and a thriving community to ensure everyone can benefit from its power. -+ **Trustworthy**: The Rocq Prover prioritizes self-verification and performance optimization, ensuring the highest level of trust and efficiency in your formal proofs. ++ **Trustworthy**: The Rocq Prover prioritizes self-verification, ensuring the highest level of trust in your formal proofs. + **Maintainable**: We are committed to a clean and streamlined codebase, simplifying future development and reducing the burden on users. -+ **Usable**: We do our best to improve day-to-day usability for mathematicians, educators, and engineers alike. This includes exploring AI-powered features and streamlined domain-specific tools. ++ **Usable**: We do our best to improve day-to-day usability for mathematicians, educators, and engineers alike. This includes improving performance, exploring AI-powered features and streamlined domain-specific tools. *Join us in shaping the future of formal verification!* @@ -38,7 +38,6 @@ This roadmap outlines our vision for Rocq's future, focusing on four key pillars ### 2. Trustworthy Proofs * **Certified Type Theory and Extraction:** The Rocq prover is based on the formal verification of its type theory implementation and extraction system, minimizing the trusted code base and increasing user confidence in results (C, D, E). -* **Performance Optimization:** We keep identifying areas for performance improvement while maintaining stability (all audiences). ### 3. Implementation Efficiency and Maintainability @@ -49,6 +48,7 @@ This roadmap outlines our vision for Rocq's future, focusing on four key pillars ### 4. Enhanced Usability +* **Performance**: address performance limitations that impact projects that are widely used in industry and academia. * **AI-powered Features:** Leverage AI for improved suggestion mechanisms, proof search, information retrieval, error reporting, and visualization (A, B, C, E). * **Theory Transfer Support:** Develop tools for transferring proofs and concepts between different representations, *e.g.*, proof-oriented vs. computation-oriented structures (D, E). * **Library Integration:** Simplify collaboration and integration of existing and future libraries from diverse contributors (C, E). From 0bebb8d6f08c9e6eeb2552cc139334ba0712b05a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Oct 2024 20:37:55 +0200 Subject: [PATCH 2/2] Update text/rocq-roadmap.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- text/rocq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/rocq-roadmap.md b/text/rocq-roadmap.md index 1f19a50a..8109ec65 100644 --- a/text/rocq-roadmap.md +++ b/text/rocq-roadmap.md @@ -48,7 +48,7 @@ This roadmap outlines our vision for Rocq's future, focusing on four key pillars ### 4. Enhanced Usability -* **Performance**: address performance limitations that impact projects that are widely used in industry and academia. +* **Performance**: address performance limitations that impact projects that are widely used in industry and academia (C, D). * **AI-powered Features:** Leverage AI for improved suggestion mechanisms, proof search, information retrieval, error reporting, and visualization (A, B, C, E). * **Theory Transfer Support:** Develop tools for transferring proofs and concepts between different representations, *e.g.*, proof-oriented vs. computation-oriented structures (D, E). * **Library Integration:** Simplify collaboration and integration of existing and future libraries from diverse contributors (C, E).