3 ms·

Verifying Move Borrow Checker in Lean:An Experiment in AI-Assisted PL Metatheory

• joshsegall 7mo ago
  "The preservation proof contains 153 lemmas (mostly conjectured by AI), collectively showing that each of these steps preserves the 35-field invariant" Proofs of features are notoriously harder than usage, but I think this illustrates something about how heavyweight the ownership design is and the complexity is forces users to content with.