Updates for front-page documentation (rust-lang#1138)

* Changes for `README.md`

* Changes for getting-started

* Rename "Workarounds" to "Working with CBMC"

* Minor fixes in "Working with rustc"

* Suggestions from code review

* Place "working w rustc" after "working w CBMC"

* Add suggestion and correct link

* Remove "it" and capitalize Rust

Author: adpaco-aws

README.md

@@ -2,19 +2,20 @@
 
 The Kani Rust Verifier is a bit-precise model checker for Rust.
 
+Kani is particularly useful for verifying unsafe code in Rust, where many of the language's usual guarantees are no longer checked by the compiler.
 Kani verifies:
- * Memory Safety -- even in unsafe Rust code
- * User-specified assertions
- * Absence of panics
- * Absence of some classes of undefined behavior
+ * Memory safety (e.g., null pointer dereferences)
+ * User-specified assertions (i.e., `assert!(...)`)
+ * The absence of panics (e.g., `unwrap()` on `None` values)
+ * The absence of some types of unexpected behavior (e.g., arithmetic overflows)
 
 ## Installation
 
 Kani must currently be built from source. See [the installation guide](https://model-checking.github.io/kani/install-guide.html) for more details.
 
-## How does Kani work?
+## How to use Kani
 
-You write a _proof harness_ that looks a lot like a test harness, except that you can check all possible values using `kani::any()`:
+Similar to testing, you write a harness, but with Kani you can check all possible values using `kani::any()`:
 
 ```rust
 use my_crate::{function_under_test, is_valid, meets_specification};
@@ -35,7 +36,8 @@ fn check_my_property() {
 }
 ```
 
-Kani will then prove that all valid inputs produce acceptable outputs, without panicking or executing undefined behavior.
+Kani will then try to prove that all valid inputs produce acceptable outputs, without panicking or executing unexpected behavior.
+Otherwise Kani will generate a trace that points to the failure.
 We recommend following [the tutorial](https://model-checking.github.io/kani/kani-tutorial.html) to learn more about how to use Kani.
 
 ## Security

docs/src/SUMMARY.md

@@ -18,9 +18,9 @@
   - [Where to start on real code](./tutorial-real-code.md)
 
 - [Developer documentation](dev-documentation.md)
-  - [Workarounds](./workarounds.md)
-  - [Command cheat sheets](./cheat-sheets.md)
+  - [Working with CBMC](./cbmc-hacks.md)
   - [Working with `rustc`](./rustc-hacks.md)
+  - [Command cheat sheets](./cheat-sheets.md)
   - [Testing](./testing.md)
     - [Regression testing](./regression-testing.md)
     - [Book runner](./bookrunner.md)

docs/src/workarounds.md renamed to docs/src/cbmc-hacks.md

@@ -1,7 +1,6 @@
-# Workarounds
+# Working with CBMC
 
-This section describes a few workarounds that may help overcome tooling
-issues in the Kani project.
+This section describes how to access more advanced CBMC options from Kani.
 
 ## CBMC arguments
 

docs/src/getting-started.md

@@ -1,20 +1,18 @@
 # Getting started
 
-Kani is a Rust verification tool based on _model checking_. With Kani, you can
-ensure that wide classes of problems are absent from your Rust code by writing
-_proof harnesses_, which are broadly similar to tests (especially property
-tests).
+Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs.
+Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler.
+Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows).
+Kani can also prove custom properties provided in the form of user-specified assertions.
 
-Kani is particularly useful for verifying unsafe code in Rust, where
-many of the language's usual guarantees can no longer be checked by the
-compiler. But it's also useful for finding panics and check user-defined
-assertions in safe Rust.
+Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses.
 
 ## Project Status
 
 Kani is currently under active development and has not made an official release yet.
-There is support for a fair amount of the Rust language features, but not all of them.
-If you encounter issues when using Kani we encourage you to [report them to us](https://github.com/model-checking/kani/issues/new/choose).
+There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
+Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features.
 
-Kani usually synchronizes with the main branch of Rust every two weeks, and so
-is generally up-to-date with the latest Rust language features.
+Kani usually synchronizes with the nightly release of Rust every two weeks, and so is generally up-to-date with the latest Rust language features.
+
+If you encounter issues when using Kani, we encourage you to [report them to us](https://github.com/model-checking/kani/issues/new/choose).

docs/src/rustc-hacks.md

@@ -1,9 +1,10 @@
 # Working with `rustc`
-Kani is developed on the top of the rust compiler, which is not distributed on crates.io and it depends on
+
+Kani is developed on the top of the Rust compiler, which is not distributed on [crates.io](https://crates.io/) and depends on
 bootstrapping mechanisms to properly build its components.
 Thus, our dependency on `rustc` crates are not declared in our `Cargo.toml`.
 
-Bellow are a few hacks that will make it easier to develop on the top of `rustc`.
+Below are a few hacks that will make it easier to develop on the top of `rustc`.
 
 ## Code analysis for `rustc` definitions