4 ms·

Very nice! Is work being done to produce a formal, verifiable specification? edit: I'm particularly interested in formal specifications and their use in open s

Very nice! Is work being done to produce a formal, verifiable specification? edit: I'm particularly interested in formal specifications and their use in open source software.

dikaiosune 10y ago
I know of a few efforts to better specify Rust in addition to ticki's (OP): * https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model * http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/ * https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... The first isn't using formal methods AFAIK, the second is, and the third is as well, but I think they're targeting safe code only.
- mbrubeck 10y ago
  There was also Patina, which formalized a subset of safe Rust's semantics, though it was done on an older (pre-1.0) version of the language: ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf
- weinzierl 10y ago
  Also the Rust compiler had Typestate analysis at one point of its development. [1] [1] http://marijnhaverbeke.nl/talks/rustfest_2016/#4 http://marijnhaverbeke.nl/talks/rustfest_2016/#4
  - pcwalton 10y ago
    Typestate is basically all subsumed by the uniqueness system. The two systems are equivalent, so in a sense Rust still has typestate.
- eruquen 10y ago
  Rustbelt targets unsafe and safe code. In addition, it will also deal with concurrency (incl. weak memory). Disclaimer: I am affiliated with the project.
kwantam 10y ago
There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system. The contribution here is a formalization of borrowing and ownership semantics very close to Rust's, plus a sketch of how one would prove that these semantics give memory safety. The techniques can probably be adapted to an analysis of Rust itself. Benitez, S. "Rusty Types for Solid Safety." ACM PLAS 2016. https://sergio.bz/docs/rusty-types-2016.pdf https://sergio.bz/docs/rusty-types-2016.pdf (Full disclosure: Sergio and I are colleagues.)

Very nice! Is work being done to produce a formal, verifiable specification? edit: I'm particularly interested in formal specifications and their use in open source software.

dikaiosune 10y ago

I know of a few efforts to better specify Rust in addition to ticki's (OP): * https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model * http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/ * https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... The first isn't using formal methods AFAIK, the second is, and the third is as well, but I think they're targeting safe code only.

mbrubeck 10y ago
There was also Patina, which formalized a subset of safe Rust's semantics, though it was done on an older (pre-1.0) version of the language: ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf
weinzierl 10y ago
Also the Rust compiler had Typestate analysis at one point of its development. [1] [1] http://marijnhaverbeke.nl/talks/rustfest_2016/#4 http://marijnhaverbeke.nl/talks/rustfest_2016/#4
- pcwalton 10y ago
  Typestate is basically all subsumed by the uniqueness system. The two systems are equivalent, so in a sense Rust still has typestate.
eruquen 10y ago
Rustbelt targets unsafe and safe code. In addition, it will also deal with concurrency (incl. weak memory). Disclaimer: I am affiliated with the project.

kwantam 10y ago

There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system. The contribution here is a formalization of borrowing and ownership semantics very close to Rust's, plus a sketch of how one would prove that these semantics give memory safety. The techniques can probably be adapted to an analysis of Rust itself. Benitez, S. "Rusty Types for Solid Safety." ACM PLAS 2016. https://sergio.bz/docs/rusty-types-2016.pdf https://sergio.bz/docs/rusty-types-2016.pdf (Full disclosure: Sergio and I are colleagues.)