Reference Lifetimes

[DavePearce]

In the current plans for Whiley, there is no specific need for lifetimes. That's because references always refer to heap allocated data, and never to stack allocated data (hence, always refer to data with static lifetime). However, to be a proper systems language, it seems like we'd want the ability to have references to the stack as well. For example:

int[] xs = [1,2,3]
&int p = &xs

The problem with this is that now we have to consider lifetimes. Static reference counting is not sufficient to prevent dangling pointers when stack allocated data goes out of scope. Therefore, following the trajectory of Whiley (i.e. compared with Rust) it seems sensible to punt the challenge of borrow checking to the verifier. That means we need a way to identify the lifetime of a variable within specification elements. Say |p| gives the lifetime of the data referred to by p. Then, we might want to say things like this:

function f(&int p, &int q) -> (&int r)
requires |p| > |q|
ensures |r| == |q|:
   ...

This says that: (1) the data referred to by p outlives (strictly) that referred to by q, whilst the return r has the same lifetime as q. This would seem to offer something strictly more powerful than borrow checking in Rust.