This is a lovely invitation. I had already begun an effort with my colleagues @shabalin and @saeta, though so I'll need to consult with them about what we think the best path forward is.
1 Like
This might be the case. 
This particular topic has always been a little frustrating for me, as it seems very difficult to coin unambiguous terms on the concepts involved.
Hopefully, the notations I used in the draft are more univocal.
We can forget about this part of our discussion if we restrict ourselves to the definition of an operational semantics that is sufficient to describe all desired properties.
Static invariants refer to those guaranteed by a static semantics, regardless of what the operational semantics actually allows. For instance, there's nothing in Swift's runtime execution model (I believe) that actually prevents an initializer from returning without initializing all properties. Yet such an invariant (namely, all properties are initialized when an initializer exits) holds, thanks to a set of rules that are enforced statically.
In the context of the law of exclusivity, the invariant would be that "two aliases on the same mutable storage are never available at the same time" (this is merely a paraphrase of the law itself). Here, the assumption is that the operational semantics does allow this invariant to be violated, but the type system doesn't.
It depends on the entity from whom the effect is unobservable. In this context, aliasing is unobservable to the user, who is unable to write an expression that witnesses the aliasing. Yet, it is still observable and interesting to observe from the derivation of the program's evaluation.
And you might be correct. This is why I originally suggested that both avenues should be explored. FWIW, you convinced me and I formalized a system that completely abstracts over memory. 
My claim is that the lower-level formalism is significantly simpler to define. I substantiate this claim by the fact that function calls require 4 inference rules in the semantics I drafted, as opposed to the single one I would need if I relied on an explicit memory. That being said, I do not claim that there can't be a simpler way to handle the distinction between owned and inout parameters.
Therefore, imho, which of these semantics is the best-suited to reason about any kind of property, including the ones related to value semantics, is still up for debate and might very well be subjective. Note that I use the term "reasoning" as being able to establish an understanding of the properties in the context of all Swift programs, and build on this understanding to deduce other properties specific to a single program. I do not use the term as being able to formally prove anything. Understanding a property is orthogonal to the fact that it should hold for all objects. Defining a property does not imply that it should hold for all objects: the area of a right triangle is half of the product of its two smallest sides, yet not all triangles are right-angled, and the property doesn't hold for those.
Unfortunately, in the absence of an additional high-level formalism, one would have to trust that the properties related to value semantics are indeed satisfied by the low-level model, without any formal proof. This is in fact quite common. Most people trusted that Rust guaranteed freedom from data race before any formal proof was presented. Nonetheless, this is one clear advantage of your approach, as the properties are "built-in", and ultimately the reason why I picked it for my first draft.
Of course!