# Featherweight Swift (Formal Core Language) **URL:** \ **Category:** Community Showcase\ **Created:** [November 16, 2020, 7:25am UTC](https://forums.swift.org/t/featherweight-swift-formal-core-language/42047 "2020-11-16T07:25:17Z")\ **Posts on this page:** 1\ **Showing post:** 12
**Author:** ![Alvae](https://sea2.discourse-cdn.com/swift/user_avatar/forums.swift.org/alvae/32/37012_2.png) [@Alvae](https://forums.swift.org/u/Alvae)\ **Post date:** [November 19, 2020, 10:33pm UTC](https://forums.swift.org/t/featherweight-swift-formal-core-language/42047/12 "2020-11-19T22:33:22Z")
> [@dabrahams](#): > > I'm not sure we're connecting. It appears to be the case indeed, my apologies. > [@dabrahams](#): > > My point is that all of this low-level modeling of memory and pointers doesn't seem like it should be necessary in order to describe value semantics, and seems like it will result in a much more complicated model than necessary. 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: ```swift 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? > [@dabrahams](#): > > I do think it's important to _eventually_ be able to describe how types with value semantics can be built out of traditionally-unsafe parts like pointers and memory, but that doesn't seem necessary for the purposes of laying a foundation for value semantics. 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 `X` has an independent notional _value_ . - A language-level copy (e.g., `let b = a` ) of a variable of type `X` has an equivalent value. - Given a local variable `a` of type `X` , safe code cannot observe the value of `a` except via an expression that uses `a` . - Given a variable `a` of type `X` , safe code cannot alter the value of `a` except by (...) - Concurrent access to the values of distinct variables of type `X` cannot 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](https://forums.swift.org/t/avoiding-unbreakable-reference-cycle-with-value-types-and-closures/18757/20)) 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: ```swift 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: ```swift 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) --- _[View the full topic](https://forums.swift.org/t/featherweight-swift-formal-core-language/42047)._