Some notes on Rust, mutable aliasing and formal verification

Rust, Aliasing, and Formal Verification

• Many see Rust’s borrow rules (shared‑xor‑mutable) as making formal reasoning substantially easier than in languages with pervasive mutable aliasing.
• Others caution that this shrinks the search space but doesn’t change verification’s fundamental intractability; hard properties still blow up with composition.
• Interest in a “verification‑aware Rust” or Rust‑like language that bakes in specifications, better automation, and lower annotation overhead.

Deadlocks, Concurrency, and Unsafe

• Desire for static deadlock analysis in Rust (locks, Rc/RefCell, async) to enable safer back‑pointers and fewer reference counts.
• Some doubt traditional locks are a good target for analysis, preferring role‑separated primitives (channels, producer/consumer APIs) that are more analyzable.
• Verifying correct use of unsafe is seen as valuable but blocked by the lack of a fully formalized Rust memory model.

Proof Assistants, Tooling, and UX

• Strong interest in Coq/Agda/Lean/Isabelle, but many find onboarding and proof development “mage level” and time‑consuming.
• Calls for “QuickCheck/Nitpick‑like” counterexample generation integrated into proofs to detect incorrect specs early.
• Communities (e.g., Zulip) are praised for helping beginners; nonetheless, proof scripts break when internal representations change, and tactics are often opaque.

Sound vs Unsound Methods; Practical Limits

• One camp stresses that sound, compositional proofs for rich properties rarely scale; correctness often does not decompose, so full verification of real systems remains economically out of reach.
• Another argues even partial sound guarantees (memory safety, data‑race freedom, unsafe wrappers) are meaningful, especially for security‑critical code.
• Unsound methods (testing, fuzzing, large‑scale simulation, model checking with heuristics) are highlighted as delivering better cost‑benefit in practice.

Memory Safety and Security Debate

• Disagreement over whether fully sound memory safety is “underwhelming” or foundational.
• One side: once unsoundness is reduced ~95% by safer languages or checks, the marginal value of proving the last 5% may not justify the cost.
• Other side: history of severe memory‑safety CVEs shows humans systematically misjudge risk; for software with an attack surface, eliminating memory unsafety (by any means) is argued to be non‑negotiable.

Education, Adoption, and Everyday Practice

• Many programmers lack proof experience; a single discrete math course is seen as insufficient for working comfortably with formal tools.
• Even basic techniques (static typing, unit tests, fuzzing) are underused; some see cultural and economic incentives (speed over robustness) as the bigger barrier than tool capability.

GC, Reference Counting, and Hybrids

• Discussion of refcounting plus cycle collectors (Python, Nim’s ORC, DOM, Rust crates) and compile‑time refcount optimization (e.g., Koka).
• Rust’s Arc, Mutex, RefCell, and cycle‑GC experiments are noted; typical large Rust codebases reportedly use them sparingly, but patterns vary (e.g., embedded Mutex<RefCell<_>>).