Update README.md to create a list of examples of using Verus #1352
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
programs over there.
utaal
requested changes
Nov 29, 2024
| @@ -20,8 +20,6 @@ Verus is under *active development*. Features may be broken and/or missing, and | |||
| the documentation is still incomplete. If you want to try Verus, please be | |||
| prepared to ask for help in the [💬 Zulip](https://verus-lang.zulipchat.com/). | |||
|
|
|||
| The Verus community has published a number of research papers, and there are a variety of industry and academic projects using Verus. You can find a list on our <a href="https://verus-lang.github.io/verus/publications-and-projects/">publications and projects</a> page. If you're using Verus please consider adding your project to that page (see the instructions there). | |||
There was a problem hiding this comment.
Even if it leads to a little bit of repetition, I'd like to preserve this paragraph. It's a more direct link to Verus-related publications and projects, which aren't necessarily just example code that people are looking for as a way to "see Verus used in action".
| In addition to the documentation above, it can be helpful to see Verus used in action. Here are some starting points. | ||
| * <a href="https://verus-lang.github.io/verus/publications-and-projects/">Publications and projects</a> using Verus -- If you're using Verus please consider adding your project to that page (see the instructions there). | ||
| * [Standalone examples](https://github.com/secure-foundations/human-eval-verus/) showing Verus in use for small, concrete tasks. | ||
| * [Miscellaneous small examples](source/rust_verify/example) illustrating various Verus features |
There was a problem hiding this comment.
These aren't just "small examples". For examples, the state_machines directories has sizable examples of VerusSync. Can we make it sound a bit more appealing than "miscellaneous"? I think browsing these would be worthwhile for a newcomer, especially syntax.rs (which we may want to point out explicitly), although giving it a bit more structure would be helpful.
| * <a href="https://verus-lang.github.io/verus/publications-and-projects/">Publications and projects</a> using Verus -- If you're using Verus please consider adding your project to that page (see the instructions there). | ||
| * [Standalone examples](https://github.com/secure-foundations/human-eval-verus/) showing Verus in use for small, concrete tasks. | ||
| * [Miscellaneous small examples](source/rust_verify/example) illustrating various Verus features | ||
| * [Unit tests](source/rust_verify_test/tests) for Verus features |
There was a problem hiding this comment.
Suggested change
| * [Unit tests](source/rust_verify_test/tests) for Verus features | |
| * [Unit tests](source/rust_verify_test/tests) for Verus, containing examples of Verus syntax and features. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A number of people have been interested in examples of using Verus, but they haven't found the projects link that we already have, and only a few manage to find the folders of examples and tests, so I think it would help to have them presented more explicitly.