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.
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
staticlifetime). 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: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 byp. Then, we might want to say things like this:This says that: (1) the data referred to by
poutlives (strictly) that referred to byq, whilst the returnrhas the same lifetime asq. This would seem to offer something strictly more powerful than borrow checking in Rust.