Capturing types annotate types with capture sets that track the capabilities a value mayretain, which form the foundation of Scala 3′s capture checking. Existing formal accounts of capturingtypes establish type soundness syntactically via progress and preservation. However, they do notanswer a more basic question: what does a capturing type mean? We propose a talk on a logicalanswer. We build a logical model of System Capless, where capture sets denote access to heap locations,and establish semantic type soundness of the calculus. The model gives a direct semantic reading ofcapture sets and use-sets, and establishes results such as (1) programs exercise only capabilities intheir statically inferred use-sets, and (2) programs with a read-only use-set do not alter the heap. Thedevelopment is fully mechanized in Lean 4.