[anodized] docs: further refine README (#137)

Author: mkovaxx

crates/anodized/README.md

@@ -12,15 +12,15 @@
 
 # Anodized
 
-In short: `anodized` is to specification what `serde` is to serialization.
+`anodized` is to specification what `serde` is to serialization: a common layer that connects your code to an ecosystem of tools.
 
-Anodized is a common specification layer for Rust: it allows writing specs directly in Rust. The specs can **express complex properties** that go far beyond what the type system supports. Anodized **works on stable Rust** and does not alter the language or the toolchain in any way, staying compatible with components such as `rust-analyzer`. Besides expressing specs, Anodized also helps enforce them by **providing integration points** for tools such as fuzzers, property-based testing, formal verifiers, and so on.
+Write preconditions, postconditions, loop invariants, and type refinements directly in standard Rust. Validate them with runtime checks, fuzzers, model checkers, or formal provers - without rewriting your specs when you switch or combine tools.
 
 ## The `spec` Attribute
 
-- **highly expressive**: Write pre/postconditions, loop invariants, and type refinements: all in the standard Rust you already know.
-- **deeply integrated**: Syntax/type-checked by the compiler, and understood by `rust-analyzer` - no need for special components.
-- **widely compatible**: Validate the specs with any combination of runtime checks, fuzzers, model checkers, or formal provers.
+- **highly expressive**: Write specs in the Rust you already know - call functions, use macros, write `if` and `match` expressions.
+- **deeply integrated**: Syntax-checked, type-checked, and understood by `rust-analyzer` out of the box. No special toolchain components needed.
+- **widely compatible**: Validate the same specs with any combination of runtime checks, fuzzers, model checkers, or formal provers.
 
 <img style="max-width:630px;" alt="editor integration demo" src="https://raw.githubusercontent.com/mkovaxx/anodized/main/assets/anodized-editor-integration.gif">
 
@@ -58,11 +58,9 @@ fn calculate_percentage(part: f64, whole: f64) -> f64 {
 
 **3. Validate your code against the specs.**
 
-Use one or more enforcement tool.
+Use one or more enforcement tools.
 
-The easiest is runtime checks, which Anodized provides out of the box.
-
-All you need is tests that make function calls.
+The easiest is runtime checks, which Anodized provides out of the box. All you need is tests that make function calls.
 
 ```rust,no_run
 #[test]
@@ -94,23 +92,32 @@ For more details and other approaches, see [The Anodized Reference](https://gith
 
 ## Why Anodized
 
-The Rust Team is building [native contract support](https://github.com/rust-lang/rust/issues/128044) into the language. We hope that learnings from Anodized will help their work, and we plan to offer a migration tool so that Anodized users can switch to Rust-native contracts as soon as they're ready.
+Rust has a growing ecosystem of excellent verification tools - Aeneas, Creusot, Flux, Hax, Kani, Prusti, Verus, and more. Each one brings unique strengths. Anodized provides a shared specification layer so that these tools, and the developers who use them, do not have to go it alone.
+
+**For developers writing specs:**
+
+- Write your specs once in standard Rust, using the language you already know.
+- Validate them with runtime checks right away, without learning any new tools.
+- When you are ready for deeper assurance, connect the same specs to a fuzzer, model checker, or formal verifier - without rewriting anything.
+- Switch or combine tools freely. Your specs are yours, not locked to any single tool.
+
+**For developers building verification tools:**
 
-Rust has many excellent verification tools: Aeneas, Creusot, Flux, Hax, Kani, Prusti, Verus, just to name a few. Their wider adoption is limited by the following key issues:
+- Consume Anodized specs instead of building and maintaining a custom spec frontend.
+- Focus your effort on the analysis that makes your tool unique.
+- Reach developers who are already writing specs, lowering the barrier to trying your tool.
 
-- Modifications to Rust (the language or the toolchain) make learning and use more difficult.
-- Differences make using a combination of tools difficult and increase switching costs.
-- Keeping modified components in sync with upstream Rust is more work for tool developers.
+### Relationship to Rust Native Contracts
 
-By adopting Anodized as a frontend, developers of verification systems can focus on the analysis itself and avoid duplicating the effort of defining and processing specs. Users can write their specs once, and gain access to a wide range of enforcement tools including runtime checks, fuzzing, verification, and more.
+The Rust Team is building [native contract support](https://github.com/rust-lang/rust/issues/128044) into the language. Anodized is a library-level experiment that lets developers start writing specs on stable Rust today. We hope to actively participate in the native contracts effort and contribute useful data points from practical experience with Anodized. When Rust-native contracts stabilize, we plan to offer a migration tool so that Anodized users can transition smoothly.
 
 ## Why Write Specs as Rust Code
 
 A core design principle of Anodized is that a spec uses **standard Rust syntax**. This is a deliberate choice that provides key benefits over using a custom language.
 
-- **The Language You Already Know**: No need to learn yet another language to write the specs. Write them in the one you already know: standard Rust. Call functions, use macros (like `matches!`), or write `if` and `match` expressions, and so on. As long as it syntax- and type-checks, it's good to go.
+- **The Language You Already Know**: No need to learn yet another language to write the specs. Write them in the one you already know: standard Rust. Call functions, use macros (like `matches!`), or write `if` and `match` expressions, and so on. As long as it syntax- and type-checks, it is good to go.
 
-- **An Integral Part of Your Code**: Specs aren't special comments or strings; they are real Rust expressions, fully integrated with your code. The Rust compiler checks every spec for syntax and type errors, just like any other part of your code. If you misspell a variable, compare incompatible types, or make any other mistake, you'll get a familiar compiler error pointing directly to the spec element that needs fixing.
+- **An Integral Part of Your Code**: Specs are not special comments or strings; they are real Rust expressions, fully integrated with your code. The Rust compiler checks every spec for syntax and type errors, just like any other part of your code. If you misspell a variable, compare incompatible types, or make any other mistake, you will get a familiar compiler error pointing directly to the spec element that needs fixing.
 
 ## Why "Spec" Instead of "Contract"
 
@@ -128,7 +135,7 @@ The term "spec" is already familiar from test specs, API specs, and formal speci
 
 ## Prior Art and Motivation
 
-The idea of adding contracts to Rust isn't new, and Anodized builds upon the great work and ideas from several other projects and discussions in the community. It is a fresh take with a strong focus on ergonomics and a forward-looking vision for an integrated ecosystem.
+The idea of adding contracts to Rust is not new, and Anodized builds upon the great work and ideas from several other projects and discussions in the community. It is a fresh take with a strong focus on ergonomics and a forward-looking vision for an integrated ecosystem.
 
 **The `contracts` Crate**