Challenge 7: make panicking part optional; remove mention of verifying intrinsics (model-checking#357)

Update the atomic intrinsics challenge to make verifying the intrinsics
out of scope, since that would require verifying compiler
implementations that are out of scope for this effort. Also make the
part about verifying the absence of panics optional to restrict the
requirements to safety only.

I also added a `mdbook-linkcheck` dependency because I discovered I
needed that to build the book locally.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

doc/mdbook-metrics/Cargo.toml

@@ -5,4 +5,5 @@ edition = "2021"
 
 [dependencies]
 mdbook = { version = "^0.4" }
+mdbook-linkcheck = "0.7.7"
 serde_json = "1.0.132"

doc/src/challenges/0007-atomic-types.md

@@ -87,14 +87,18 @@ Write and verify safety contracts for the unsafe functions:
 - `atomic_umax`
 - `atomic_umin`
 
+##### Panicking (Optional)
 Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with `order`s that would cause panics.
 
 For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering.
 In this case, you would write contracts on the safe `store` methods that enforce that they are not called with either of those `order`s.
 
+This section is not required to complete the challenge, since panicking is not undefined behavior.
+However, it would be incorrect for someone to call these functions with the wrong arguments, so we encourage providing these specifications.
+
 #### Part 3: Atomic Intrinsics
 
-Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`):
+Write safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`):
 
 | Operations            |  Functions |
 |-----------------------|-------------|