Dafny vs Ownership

[kjx]

@MikaelMayer and @kjx are both interested in Dafny vs Rust vs Ownership / Ownership types.
(along with a bunch of other people, including at least one paper at OOPSLA 2023).

The lemma I was proving was part of a Dafny model of somewhat Rust-style ownership.
(trying to be a lighter weigh alternative to things like Derek Dreyer's Coq model of Rust).
In particular, that lemma was proving that when you delete an "owner" such as a Rust
stack frame or non-borrowing variable - you can transitively delete everything "owned" by that owned.

I'm doing this in Dafny, rather than in the core of the translator, or just the "Rust Backend".
my main aim is to support various research projects I'm doing by modelling Rust or other semantics -
but I have slowly been realising that if one could bind such a semantic meta-model to "domain" objects in Dafny
then

Thus my interest in your type system model - although I haven't got on to working with that yet - just with heap invariants with an model of actual evaluation.

MPTP.pdf
learn.pdf
Rusty_Links_in_Local_Chains.pdf

[kjx]

and 18 months later I'm still going on this - I'd forgotten I'd even left this here.

can't decide if I'm daft, or just bloody-minded.

Dafny program verifier finished with 3806 verified, 0 errors, 1 time out

real	7m54.298s
user	9m53.750s
sys	0m24.956s