System Capybara: Capture Tracking for Ownership and Borrowing
summary
System Capybara extends capture checking to track ownership and borrowing by adding access-mode-qualified captures (read vs owned), enforcing separation and freshness through capture sets and a consume-as-fresh mechanism that models run-once resources. A prototype compiler Cavia implements the formal calculus and an experimental Scala 3 separation checker exists; demos show a mutable string buffer and file-handle APIs compile and reject aliasing or post-close use, and the team claims potential Rust encodings.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:42What is System Capybara
- 1:03Capture tracking core idea
- 3:13Separation and freshness
- 5:04Access modes for capabilities
- 9:04Reasoning about data separation
- 10:50Freshness and resource patterns
- 11:11File handling errors
- 13:41Formal system and future work
- 15:29Array buffer demo
- 17:01Q&A
related talks
01h 03mWhere Are We With Scala's Capabilities?
38mCapture Checking - A New Approach to Effect Safety in Scala
01h 03mInside the Scala Capture Checker
01h 23mCapture Tracking in Scala
49mThe first steps towards practical capture checking
41mHands On Capture Checking with Martin Odersky
31mReal-Life Scala Capture Checking
34mHow can we trust our agents?