I was talking about language syntax, and in particular the way proof terms for linear logic (which linear type systems come from) already provide a syntax for t

I was talking about language syntax, and in particular the way proof terms for linear logic (which linear type systems come from) already provide a syntax for this. But in fact we also have multiple options on the more programmer-familiar side of this- `try/finally` blocks, `defer`, etc. The problem isn't limited to linear types so it's already been pretty thoroughly explored.