Functional purification for `Cell` and other types with interior mutability

[tyrbentsen]

Could you elaborate on whether functional purification can still hold when using types with interior mutability, like 'Cell'?

In the following example, c2 is mutated through c1. Is there any rule that can be used to transform this into a purely functional equivalent (without having to track all the aliases to c1, which might be difficult for non-trivial cases)?

let c1: &Cell<i32> = &Cell::new(0);
let c2: &Cell<i32> = c1;
c1.set(2);
println!("{:?}", c2.get()); // Prints 2

What about RefCell, Mutex, ... ?

[Kha]

Yes, types with interior mutability are outside the thesis' language subset a priori. Some of them like Rc could still be modeled in a referentially transparent way as long methods like try_unwrap that expose the mutable state are not exposed. For all other types, you would have to introduce a global heap and presumably reason about it using separation logic. My hope is that this would still be simpler than other models that use separation logic for every single type, but this was out of scope for the thesis.