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

Jump to bottom

Update README.md to create a list of examples of using Verus #1352

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Update README.md to create a list of examples of using Verus #1352

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7c055c0
Update README.md to create a list of examples of using Verus
parno Nov 19, 2024
c894b2e
Add a link to the HumanEval repo, since there are 80+ example Verus
parno Nov 26, 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
9 changes: 7 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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".


## Try Verus

To try Verus in your browser, please visit the [Verus Playground](https://play.verus-lang.org/).
Expand All @@ -39,6 +37,13 @@ Our (work-in-progress) documentation resources include:
* [Verus License](LICENSE)
* [Verus Logos](https://verus-lang.github.io/verus/verus/logo.html)

## Examples of Using Verus
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

* [Unit tests](source/rust_verify_test/tests) for Verus features
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


## Getting in touch, reporting issues, and starting discussions

Please report issues or start discussions here on GitHub, or join us on [💬 Zulip](https://verus-lang.zulipchat.com/) for more realtime discussions and if you need help. Thank you for using and contributing to Verus!
Expand Down