4 ms·

Rust Formal Verification Working Group

151 points by dmmalam 9y ago

choroid 9y ago
How does this compare to projects like RESOLVE https://www.cs.clemson.edu/resolve/ https://www.cs.clemson.edu/resolve/?
- TheDong 9y ago
  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.
  - majewsky 9y ago
    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/Note-research.md https://github.com/rust-lang/rust-wiki-backup/blob/master/No...
- steveklabnik 9y ago
  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.
catnaroek 9y ago
Will there ever be a formal semantics for unsafe Rust?
- steveklabnik 9y ago
  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 :)
  - catnaroek 9y ago
    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.
    - steveklabnik 9y ago
      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.
agentultra 9y ago
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!

151 points by dmmalam 9y ago

choroid 9y ago

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

TheDong 9y ago
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.
- majewsky 9y ago
  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/Note-research.md https://github.com/rust-lang/rust-wiki-backup/blob/master/No...
steveklabnik 9y ago
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.

catnaroek 9y ago

Will there ever be a formal semantics for unsafe Rust?

steveklabnik 9y ago
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 :)
- catnaroek 9y ago
  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.
  - steveklabnik 9y ago
    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.

agentultra 9y ago

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!