Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[roadmap] rework item on performance #95

Merged
merged 2 commits into from
Oct 11, 2024
Merged

[roadmap] rework item on performance #95

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5c05a5d
[roadmap] rework performance item
gares Oct 9, 2024
0bebb8d
Update text/rocq-roadmap.md
gares Oct 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions text/rocq-roadmap.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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!*

Expand All @@ -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

Expand All @@ -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 (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).
Expand Down