Cleanup is lexical and ordered: defer registers work on one scope, and the constrained File using form composes with the same unwind stack.
Policy
defer call or defer { block } belongs to the innermost lexical scope. Registered actions run last-in, first-out on normal exit and when return, Result propagation, break, or continue crosses that scope. A successful File using acquisition registers one implicit close before the body registers later defers, so body cleanup runs first and close runs last.
Specified behavior
A break value is fully evaluated before crossed scopes unwind. while let success scopes drain before the next scrutinee attempt. The using initializer runs once before its binding exists; failure propagates before cleanup registration. Its File binding is immutable and child-scoped, body tail is discarded, and control crossing the scope closes before continuing. A closure may retain the File value, but the implicit close still occurs at scope exit.
Constraints and loud decline
defer is not catch/finally syntax and does not replace an existing returned Err with a cleanup error. using is File-only, one resource, one bare name, and statement-valued. Explicit close does not cancel the registered attempt. Ordinary runtime fault aborts do not carry a language guarantee that lexical defers or using cleanup drain.
Deferred boundary
User-defined disposable protocols, multi-resource acquisition, resource transfer, asynchronous cleanup, cancellation, module-lifetime finalization, host-exception guarantees, and portable behavior after repeated or post-close File operations are outside this language policy.
Worked example
function writeLog(message: string) -> Result<(), string> {
let file = open("app.log")?
defer { file.close() }
file.write(message)?
return Ok(())
}