It appears to be the case indeed, my apologies.
I argue that it depends on the purpose of the resulting formalization.
Say I define some sort of operational semantics, i.e., the purely functional system you mentioned. Then yes, of course, I can model "mutation" in very simple terms. For instance, many lambda-calculi express assignment as simply as this:
let x := v in e ~> e[x/v]
This is expressive enough, I assume, to describe the kind of formal definition you suggested. Nonetheless, notice that such a syntactic trick does not support "reference semantics". This, I believe, necessarily requires to model memory somehow. But this is still just math (to be fair, so are Alias Types). There also has been some interesting approaches to do this "syntactically"; see [1] and subsequent work from Elena Zucca.
Now the question is: what do I want from this?
If the goal is to formally illustrate the properties you described in your proposal, then I completely agree. We do not need the kind of models I suggested. In fact, if we look at your bullet points, the simple assignment semantics above can almost illustrate everything:
- Each variable of type
Xhas an independent notional value . - A language-level copy (e.g.,
let b = a) of a variable of typeXhas an
equivalent value. - Given a local variable
aof typeX, safe code cannot observe the value ofa
except via an expression that usesa. - Given a variable
aof typeX, safe code cannot alter the value ofa
except by (...) - Concurrent access to the values of distinct variables of type
Xcannot
cause a data race.
The two last points require a little more attention, because they are predicated upon a notion of reference. This comes back to what I meant about the requirement to model memory as some sort of "store", so that two names can refer to the same thing. I like @Lantua's definition of so-called points of access (see Avoiding unbreakable reference cycle with value types and closures? - #20 by Lantua) to describe this concept. We can model such a store in the "conventional" way, by the means of an ad-hoc data structure, or in the style of [1]. In the former case, I guess it would look something like the following:
S; var x := v in e ~> S, x=v; e[x/ref(x)]
S, x=v1; ref(x) := v2 in e ~> S, x=v2; e
We obtain a very simple framework (I don't even need types!) to formally illustrate your bullet points. We may also prove them on terminating programs. 1-2 seem trivial. 3-4 require some care about the ways one can interact with the store. 5 seems trivial, although I might be missing something more subtle from the definition.
Now, because this is described entirely in terms of operational semantics, we cannot emulate the compiler's behavior with respect to the guarantees it claims. Consider the following example:
func f(a: inout Int, b: inout Int) {}
var x = 0
f(a: &x, b: &x)
The compiler catches that this program is incorrect, correctly pointing out that Inout arguments are not allowed to alias each other. If we model this only through the operational semantics, perhaps using conditions on reduction rules (this is the "care about the ways one can interact with the store" part that I mentioned), then there's no way to say that the program is incorrect without executing it. This is a problem because there's obviously no guarantee that a particular evaluation does not diverge (even Featherweight Swift has recursion through self). To model this, I think it would be appropriate to use an elaborate type system, so that we may prove your properties (and others) statically.
I hope this makes sense, and that I didn't mischaracterise your point. Also, it appears as if I am absolutely unable to write shorter posts, so I thank any reader who will have made it all the way through.
By the way, I'm open to move this discussion to a phone call, even if it means summarizing the exchange in text here afterwards.
[1] Andrea Capriccioli, Marco Servetto, Elena Zucca: An Imperative Pure Calculus. Electron. Notes Theor. Comput. Sci. 322: 87-102 (2016)