Is there actually a formal language semantics definition anywhere? I thought all we had was stuff like https://doc.rust-lang.org/reference/index.html which is explicitly listed as "not a formal spec".
We are generally at a point where if it's documented, it's guaranteed. This feature is really easy to describe, and so we have a high degree of confidence that when we say "this behavior is defined", we won't run into an edge case where we'd have to break it.
So, in this case, it's a documented part of Option.
I realize this answer isn't fantastic, but it's where we're at now. It's why we're working on the reference this year!
