Interesting article. It got me thinking about what invariants could be proven for these data structures with a proof assistant having knowledge of things like

Interesting article. It got me thinking about what invariants could be proven for these data structures with a proof assistant having knowledge of things like lifetime or ownership. One thing that bothers me about Rust is that these properties are hardwired into the syntax in a very specific way. Sometimes I might want these properties to be exactly the way they are in Rust. Sometimes less, sometimes more, sometimes other semantics. This article makes me think that the tools Rust offers aren’t very good for this task. They’re not bad! But it seems like something better could be devised.