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...
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.
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.
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.
9 comments
[ 2.3 ms ] story [ 25.6 ms ] threadRESOLVE is a research project that is effectively a means to generate papers and grant money, not to do anything useful.
In open source, some people wear many hats :)
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.
The interior mutability primitives in the standard library already have a proof, incidentally. Look at the Rust Belt work.
Looking forward to reading more about it!