4 ms·
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
by 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 agoThere 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 agoAlso 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 agoTypestate is basically all subsumed by the uniqueness system. The two systems are equivalent, so in a sense Rust still has typestate.
- eruquen 10y agoRustbelt targets unsafe and safe code. In addition, it will also deal with concurrency (incl. weak memory). Disclaimer: I am affiliated with the project.