[anneal] README: Explain philosophy wrt typing

anneal/Cargo.toml

@@ -4,7 +4,7 @@ members = [".", "tools/doc_gen"]
 [package]
 name = "cargo-anneal"
 edition = "2024"
-version = "0.1.0-alpha.22"
+version = "0.1.0-alpha.23"
 description = "Formally verify that your safety comments are correct."
 categories = [
   "development-tools::cargo-plugins",

anneal/README.md

@@ -7,17 +7,92 @@
 > **Note:** Anneal is currently in pre-alpha. You're welcome to use it, but many things
 > are broken or unsound, and we will change APIs frequently.
 
-Anneal enables "literate verification" of safe and `unsafe` code. It allows you to write [Lean](https://lean-lang.org/) specifications and proofs of correctness and soundness directly within your Rust source files using standard documentation comments.
+For safe code, Rust promises that "if it compiles, then it is memory-safe." Anneal promises the same for unsafe code.
 
-By checking the validity of proofs using Lean, Anneal removes most `unsafe` code from your [trusted computing base](https://en.wikipedia.org/wiki/Trusted_computing_base) (TCB).*
+Rust promises that all safe Rust code is free of memory safety bugs. It does this by encoding the requirements for memory safety in the type system, ensuring that if a program type checks, then it is free of memory safety bugs. The lifetime system prevents use-after-free bugs, the ownership system prevents double-free bugs, and so on. **There do not exist type-checked safe Rust programs with memory safety bugs.**[^1] The same is not true of unsafe Rust code. **There do exist type-checked unsafe Rust programs with memory safety bugs.**
 
-| TCB without Anneal | TCB with Anneal |
-| ------------------- | ---------------- |
-| Rust toolchain      | Rust + Anneal toolchains   |
-| `unsafe` code       | Unsupported `unsafe` code* |
+[^1]: Barring compiler and platform bugs, which do exist.
+
+One way to understand this distinction is that a safe Rust function must be free of memory safety bugs *no matter what value is passed in*. Consider [`usize::strict_div`](https://doc.rust-lang.org/std/primitive.usize.html#method.strict_div):
+
+```rust
+impl usize {
+    /// # Panics
+    /// 
+    /// This function will panic if `rhs` is zero.
+    pub fn strict_div(self, rhs: usize) -> usize;
+}
+```
+
+A safe implementation of `strict_div` would be forced to handle *all possible values* of `self` and `rhs`. `strict_div` must handle the case where `rhs == 0` (division by zero). It could choose to return an arbitrary `usize` or, as it does in practice, panic. But it cannot exhibit a memory safety bug – Rust would prevent such a program from compiling.
+
+By contrast, consider the unsafe [`usize::unchecked_div_exact`](https://doc.rust-lang.org/std/primitive.usize.html#method.unchecked_div_exact):
+
+```rust
+impl usize {
+    /// # Safety
+    /// 
+    /// This results in undefined behavior when `rhs == 0` or `self % rhs != 0`.
+    pub unsafe fn unchecked_div_exact(self, rhs: usize) -> usize;
+}
+```
+
+Rust doesn't have any way to epxress "a pair of `usize`s such `rhs != 0` and `self % rhs == 0`". Thus, the type signature of `unchecked_div_exact` is *too permissive*. While it prevents some illegal values statically (e.g., the type system will not permit you to pass `-1`), some illegal values will compile just fine, and will result in memory safety bugs at runtime:
+
+```rust
+let res: usize = unsafe { 1usize.unchecked_div_exact(0) };
+```
+
+In this view, unsafe Rust differs from safe Rust in that **some type-safe values are still illegal**, while in safe Rust, **all type-safe values are legal** (where "illegal" means "will result in a memory safety bug").
+
+As we saw before, Rust ensures that **no type-checked safe Rust programs contain memory safety bugs.** Anneal provides the same promise, but for unsafe Rust code. Just as Rust encodes memory safety requirements in its types, Anneal encodes memory safety requirements in its annotations. Unlike Rust types, Anneal annotations are powerful enough to prevent *any* illegal values from compiling, even in unsafe code. In this sense, Anneal annotations are an *extension* to Rust's type system.
+
+For example, here's how Anneal would encode the safety precondition of `unchecked_div_exact`, preventing buggy programs from compiling:
+
+```rust
+impl usize {
+    /// # Safety
+    /// 
+    /// ```anneal
+    /// requires(nonzero): rhs != 0
+    /// requires(divides): self % rhs == 0
+    /// ```
+    pub unsafe fn unchecked_div_exact(self, rhs: usize) -> usize;
+}
+
+let res: usize = unsafe { 1usize.unchecked_div_exact(0) }; // ERROR: (TODO: What's the error message?)
+```
+
+Anneal removes most `unsafe` code from your [trusted computing base](https://en.wikipedia.org/wiki/Trusted_computing_base) (TCB).*
+
+| | Rust | Anneal |
+|-| ---- | ------ |
+| | `cargo check` | `cargo anneal verify` |
+| Types | Rust types | Rust types + Anneal annotations |
+| Guarantee | Safe code is free of memory safety bugs | Safe and unsafe code is free of memory safety bugs |
+| Caveat | Unsafe code is unchecked | Unsupported `unsafe` code is unchecked* |
+| TCB | Rust toolchain, `unsafe` code | Rust + Anneal toolchains, unsupported `unsafe` code* |
 
 \* *Anneal cannot verify the soundness of certain constructs such as FFI or inline assembly. These constructs remain in the TCB.*
 
+### Development Philosophy
+
+Anneal is a [formal verification](https://en.wikipedia.org/wiki/Formal_verification) tool. However, it diverges from many formal verification tools in its philosophy for how it should be used by end users.
+
+While exceptions exist, the most common form of formal verification has historically been *post-hoc verification*, in which verification is applied to a software artifact which already exists and which was not specifically written with verification in mind. This approach comes with a number of assumptions and limitations which we aim to sidestep:
+1. Assumes that verification requires distinct expertise which developers lack
+2. Verification is applied to a codebase whose structure may not be amenable to verification
+3. Results in long iteration cycles, in which feedback from verification is obtained long after a line of code is written
+4. Without extra infrastructure (e.g. in CI), software codebase and verification artifacts (specifications and proofs) can drift, requiring periodic efforts to update the verification to "catch up" with recent code changes
+
+We believe that all of these can be addressed by thinking of specifications as merely an extension to the type system rather than a parallel artifact. In particular:
+1. Developers already have justifications – albeit undocumented – for their belief that their code is correct. Type annotations simply ask them to make these justifications explicit
+2. As with any form of static typing, Anneal annotations will shape the codebase and nudge developers towards certain patterns for code organization which are more amenable to verification. This nudging will happen in the developer's inner loop and so will be much more effective than feedback from post-hoc verification
+3. We expect `cargo anneal verify` to be just as frequent as `cargo check`, and so iteration cycles are extremely short
+4. CI can simply run `cargo anneal verify` to ensure that specifications and proofs never drift or bit rot
+
+### Human and Agentic Development
+
 Anneal is designed for use by both human engineers and AI coding agents. By providing machine-checked guarantees for safe and `unsafe` code, Anneal eliminates the cognitive burden of manual review and enables the safe acceleration of systems software development. We have [demonstrated](https://drive.google.com/file/d/1areyf438L0izETTHj7PRMnoSHSX4kM29/view?usp=sharing) that Antigravity can author `unsafe` Rust code and prove its soundness using Anneal.
 
 Without Anneal:
@@ -109,7 +184,7 @@ impl std::ops::Div<PositiveUsize> for usize {
 Install Anneal and its required toolchains (Charon and Aeneas):
 
 ```bash
-cargo install cargo-anneal@0.1.0-alpha.22
+cargo install cargo-anneal@0.1.0-alpha.23
 cargo anneal setup
 ```