It’s so cool to see an open source project adopt formal methods. I tried to start a working group in Openstack a couple of years ago but the reception was barely lukewarm.
This is a group of people working on different approaches, but trying to find some commonality. You’d have to compare against each of them to really know.
Insinuating that research is not doing "anything useful", while at the same time calling Rust "pragmatic/useful" is particularly ironic. Rust's design has been heavily influenced by research in programming language theory and adjacent fields: https://github.com/rust-lang/rust-wiki-backup/blob/master/No...
Depends on what you mean by “formal”, and on what timescale, but this group will be a consumer of the “unsafe guidelines WG”, and we would eventually like to formalize such a thing. Some of the participants in this WG would be the ones interested in doing this work.
With mere “guidelines”, there is no practical, unambiguous way to establish without a shadow of doubt that a function implemented using unsafe Rust upholds the safety guarantees of safe Rust.
So I want a proper formal semantics, maybe not for all of Rust, but at least for a fragment interesting enough to express lifetime and mutability concerns. In particular, I want a formal account of interior mutability.
Looking forward to reading more about it!