Rust Formal Verification Working Group | Hacker News Reader

Rust Formal Verification Working Group

internals.rust-lang.org

151 pointsdmmalam9 comments

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.

Looking forward to reading more about it!

How does this compare to projects like RESOLVE https://www.cs.clemson.edu/resolve/?

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.

This is Rust-specific and pragmatic/useful.

RESOLVE is a research project that is effectively a means to generate papers and grant money, not to do anything useful.

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...

Will there ever be a formal semantics for unsafe Rust?

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.

In open source, some people wear many hats :)

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.

I hear you! As I said, these things take time.

The interior mutability primitives in the standard library already have a proof, incidentally. Look at the Rust Belt work.

Reply on news.ycombinator.com