Skip to content

Commit

Permalink
Tune down recommendation and point to bolero (rust-lang#2212)
Browse files Browse the repository at this point in the history
I don't think we should discourage people from looking into Kani so I'm changing the words here. I also changed the reference to point to bolero instead of proptest.
  • Loading branch information
celinval authored Feb 15, 2023
1 parent 9439a54 commit 84068cf
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions docs/src/application.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,8 @@ You may be interested in applying Kani if you're in this situation:
2. You've already invested heavily in testing to ensure correctness.
3. You want to invest further, to gain a much higher degree of assurance.

> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking.
> These yield good results, are very cheap to apply, and are often easier to adopt and debug.
> Kani is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with.
> If you haven't already, we also recommend techniques like property testing and fuzzing (e.g. with [`bolero`](https://github.com/camshaft/bolero/)).
> These yield good results, are very cheap to apply, and are often easy to adopt and debug.
In this section, we explain [how Kani compares with other tools](./tool-comparison.md)
and suggest [where to start applying Kani in real code](./tutorial-real-code.md).

0 comments on commit 84068cf

Please sign in to comment.