User data saving

Given a program which allows a user to enter non-trivial amounts of data, we do not want to discard unsaved data without the user’s explicit agreement.

This a cross-cutting concern, which is trivial for a human to check in a particular case, but is hard to check exhaustively manually, or to express in any formal way.

The goal is to provide some kind of reliable mechanism to flag any instances of this, existing or newly introduced. Ideally it would not rely on other unenforceable rules (such as “all user input must go into one of these components”) in order to work.