Why did you make the return of write discardable? Austral semantics require all linear types have _exactly one_ consumer, so discarding it would be a compile-time error.
I think the interesting part with the linear type mechanics is that the compiler forces proper use of a state machine. A file _must_ be closed, because the handle _must_ be consumed, and a mutable borrow allows changing an object but not the permit to destroy it. They don't have magic functions like =destroy, it's just the typing rule system that requires you to call a destructor-like function at some point.
