I've put up a pull request adding this syntax and its semantics to the proposal document. There are a few more details there that should help clarify what Becca's proposal means for typed throws.
Personally, I think this is an important addition---it means that all contexts in which an error is thrown can be explicitly typed, which is a good end state.