Discard is not reset

A physical-memory reset has a different output type. For a declared memory $M$, define

On a joint state,

By contrast, discard returns no memory register at all.

One may model “discard, then allocate a blank” as an observable implementation of (eq:reset). That syntax still does not say how a reusable physical memory, its blank-state preparation, its controllers, or its environment are restored between runs.