[roadmap] rework item on performance

[gares]

This is an attempt of separating "trust" from "performance" in the main items.

What I want to say is that we optimize the system for the projects was regard as flagship. We have being doing so over the years relentlessly, it is nothing new ( @ppedrot , @SkySkimmer ), I'm just trying to put it into words and decorrelate it from trust.

Help from native speakers is more than welcome.

[Zimmi48]

These four bullet points are reflected in the structure of the document below and we should keep the link.

Do you think that it doesn't make sense to keep the two items in the same section? Then, what about moving performance in the same section as maintenance?

Otherwise, what about merging back these two lines, but keeping things more separated than they were, e.g.:

Trustworthy and performant: The Rocq Prover prioritizes self-verification, ensuring the highest level of trust in your formal proofs. At the same time, we optimize the system for our flagship projects in both industry and academia.

[Zimmi48]

And maybe remove the "our" in front of "flagship projects" to avoid carrying the meaning that we only care about projects that we own.

[gares]

I'm fine with your proposal.

Trustworthy and performant: The Rocq Prover prioritizes self-verification, ensuring the highest level of trust in your formal proofs. At the same time, we optimize the system for our flagship projects in both industry and academia.

But even there you can see that the two concepts are not related (eg "At the same time"). So I'd prefer to move it to 4, i.e. make it part of usability. Point 3 has efficiency in the title, but looks like another meaning.

So my proposal is now:

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.

4. Enhanced Usability

• Performance: optimize the system for flagship projects in both industry and academia.

[Zimmi48]

There is already an item about performance in section 2 which should be removed or moved.

Besides this small issue, I'm happy to merge this change. I will do so if there are no more comments.

I think the "Enhanced usability" section is becoming too long and it probably means something, but it doesn't have to be addressed in this PR.

[gares]

I remove the line about performance from section 2.

W.r.t. section 2, I was wondering if we should mention the De Bruijn criteria (third party verification of proofs). But that is for another PR.

[gares]

This seems to be the version @silene @TheoWinterhalter any myself like the most. @Zimmi48, @jfehrle are you ok with this last version?

[Zimmi48]

I'm quite satisfied by this proposal.

I want to emphasize that since this is a living document, we are aiming for incremental improvements. If everyone agrees this is an improvement, this PR should be merged.

If there are no more comments, I will merge at the end of the day.

[Zimmi48]

The roadmap would much stronger with more detail. I don't think there's enough here so that users have much of an idea what is planned. We can be clear that the tasks it mentions are things we would like to address in the near future but it is not guaranteed we will get to them.

At some point, perhaps in a different document, we should identify which potential improvements to Rocq will provide the most value to users, their cost and rank them (without regard to whether anyone is already committed to implement them).

For the record, this particular document aims to provide a high-level vision that should be reasonably stable in the next few years (except maybe, to remove the introduction which, like you noticed, is very specific to the renaming event).

This roadmap does not supersede the effort of #69 (which likely will find a different form, because a CEP has not been a good solution for a living document).

[Zimmi48]

If there are no more comments, I will merge at the end of the day.

Actually, in this repo, we can self-merge PRs.

So @gares: please choose your preference among my two suggestions of audience above and then merge your PR.

[jfehrle]

@gares [to me] are you ok with this last version?

@Zimmi48 My take is that is better to start afresh and implement one (reasonable) behavior, document it, and recommend that for new code.

How about allowing me time to respond before merging? Are you in a rush? I was not available between 3 and 9 am PDT this morning when the last comments were posted.

[gares]

Sorry. Please open another pr with your comments and we will amend the text again.

[Zimmi48]

@jfehrle See what I wrote when approving the PR:

I want to emphasize that since this is a living document, we are aiming for incremental improvements. If everyone agrees this is an improvement, this PR should be merged.

I should indeed have given you time to confirm whether you agree that the PR is an improvement.

But there is no point in delaying PRs that are considered improvements just because they could be improved further.

PRs are cheap, we can open new ones. If you have a vision of what the text should say, it's even easier if you are the author of the PR, rather than trying to convey your vision to someone else through review comments.

We are not adding new features to Coq here (where it makes sense to delay a PR until it is fully polished), but fixing a roadmap document that was already approved by the core team and which is already live on the Rocq website. Merging improvements quickly makes sense in this case.

[jfehrle]

I will survive. However, I'm not so keen on submitting PRs for everything unlike the usual review process. Often I want to make an observation or ask a question without having exact new wording. That doesn't really fit with me submitting a PR. Also it doesn't help that I have two fingers in a splint until maybe 1.5 weeks from now, so stuck doing hunt and peck for now. Maybe I will comment later when I can type. But also thinking the interaction takes considerable time, competing with other worthwhile tasks. Suggesting wording improvements often takes significant time.