OK. I knew about <output>. I knew about
HTMLFormElement.elements and the form
attribute of form controls.
But until today I did not know about the defaultValue and defaultChecked property of a form control, which returns
its original value. It's been there since 2015!