Move

New post on Proofs and Intuitions: Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory, in which I describe how I mechanised Move’s borrow checker in Lean with AI assistance, producing 39,000 lines of metatheory in about one month.