10 ms·

Oxide: A Formal Semantics for Rust

223 points by rachitnigam 8y ago

bluejekyll 8y ago
One of the examples in the paper has some code that you can't actually write in Rust, it's close to this: let msg: &'msg str = "Hello World"; You can write something similar and allow the compiler to infer the lifetime: let msg: &'_ str = "Hello World"; I often find myself declaring the type when I get into confusing type issues in Rust, but you can't do that as easily with lifetimes. With non-lexical lifetimes this has been less of an issue, but still there are times when I would like to be able to declare the lifetime like the first example. This error example shows the valid uses of lifetimes: https://doc.rust-lang.org/nightly/error-index.html#E0261 https://doc.rust-lang.org/nightly/error-index.html#E0261
- webkike 8y ago
  I believe you can actually name the lifetime of a block, via the same mechanism that makes labeled breaks and continues possible.
  - bluejekyll 8y ago
    Do you have an example of what you mean?
    - coolreader18 8y ago
      Like this: 'a: { let a_var: u32 = 42; let a_ref: &'a u32 = &a_var; } // ^^^^^ only valid in 'a: {}
      - gpm 8y ago
        That doesn't compile with "use of undeclared lifetime name `'a`"
        steveklabnik 8y ago
        You can name loop labels like this, but you cannot use them to introduce actual lifetimes, that’s right.
  - Retra 8y ago
    I think that was just a proposal that never got accepted? Never see it in real code either way.
twothumbsup 8y ago
Love seeing some good PL research from Northeastern in the news! I was part of the capstone class they ran back in 2015 where we used/learned the alpha version of Rust that had just been released. Great experience.
wolco 8y ago
Love the name. Could not describe what it is/does any better.
ipodopt 8y ago
Please correct me if I am wrong. They produced a simpler modified version of Rust called Oxide that focused on ownership and borrowing. They did did so they could translate it to a formal system and validate it in an easy to understand way.
- Groxx 8y ago
  That's normal for programming language formal verification, from what I've seen. The question is always "how simplified is it", and if it's simplified to the point of uselessness. There's usually something to be learned (and often bugs to be fixed) from even the most-simplified version, but AFAICT "full" language verification is basically never done (except on toy[1] languages). edit: [1]: "toy" implying "not intended for broad use", not any kind of "pointless" or "just for fun", to be clear. maybe there's a better term I should be using. so basically all "this language is designed to be formally verified and it does something interesting" languages fall into this category, because it's really not expected to be generally usable - it exists to demonstrate something, and at best become a feature of another language eventually.
  - floofy222 8y ago
    Usually these inform tools that can be used to detect rule violations. For example, the rust constant evaluator can execute almost all Rust at run-time except for FFI. This allows you to write `cargo miri test` in your project, and run your unit tests in the constant evaluator. The constant evaluator executes the program based on rules given by models like this, and if you perform an action that violates one of the rules, they report an error. For example, this program mutates a variable while a shared borrow (which excludes mutation) is alive via a raw pointer fn main() { let mut a = 13; let b = &a; let c = b as *const _ as *mut _; unsafe { *c = 42; } println!("b = {}", b); } On the playground it prints "b = 42" (https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=6a1915616357b53e8d45d4a81c7b1bd1 https://play.rust-lang.org/?version=stable&mode=debug&editio...). The playground has a `Tools` button, that allows you to run the program under `miri` (the constant evaluator). When doing so, it prints: error[E0080]: constant evaluation error: borrow being accessed (Alias(None)) does not exist on the borrow stack --> src/main.rs:5:14 | 5 | unsafe { *c = 42; } | ^^^^^^^ borrow being accessed (Alias(None)) does not exist on the borrow stack error: aborting due to previous error The error messages of the constant evaluator aren't great yet, but that basically tells you that it couldn't find a suitable mutable borrow to mutate the variable, so the access is undefined behavior.
cttet 8y ago
I really hope there would be a ML-like syntax for Rust. The current one is not so friendly to read.
- hardwaresofton 8y ago
  Agree -- these days whenever I try to pick between Haskell and Rust for a new project I go Haskell because of the much nicer syntax (though it took some getting used to). I also have almost 0 interest in OCaml due to the syntactic choices they've made.
  - TheAsprngHacker 8y ago
    I use OCaml and I am also writing my own ML dialect, so I would like to ask, what exact aspects of the OCaml syntax don't you like, and what parts of the Haskell syntax do you like in particular? (For example, do you prefer indentation-based syntax?)
    - hardwaresofton 8y ago
      I honestly don't know how to explain it really well, but OCaml is much noisier than Haskell in my opinion. Many times when I see code snippets in OCaml they're not as nice as they look in Haskell, though they're really similar. The small difference seems to snowball when the code gets increasingly complicated. Compare functor's definitions in either syntax: module type FUNCTOR = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end;; class Functor where fmap :: (a -> b) -> f a -> f b The latter looks cleaner to me. There are other ways you could write it (for example if you turned on explicit forall it would get messier. At this point I start skipping talks at conferences when they're in Scala because the amount of noise in the syntax is near unbearable to me (and there's likely to be a haskell talk on a similar topic) -- OCaml is much better in that respect, but I still find Haskell's syntax to be easiest on the eyes. OCaml might be more pedantically descriptive though, it seems to be more explicit about everything.
      - 8y ago
hardwaresofton 8y ago
> Rust is a major advancement in industrial programming languages due in large part to its success in bridging the gap between low-level systems programming and high-level application programming So glad to see this sentiment echoed somewhere outside my own head/conversations. Rust is a game changer, it brings something novel (ownership/borrowing, research-grade type system) to systems programming, and it brings great features for high level programming (type inference, strict control, high level abstraction support, "zero-cost" abstractions), and is basically a paragon of good open-source development in the open. On top of all of that it's done by Mozilla, with so much less resources than other companies, and a demonstrated interest in making software that's good for everyone.
- svrtknst 8y ago
  > On top of all of that it's done by Mozilla IIRC it's open-source with a fairly wide set of contributors, with Mozilla being a major one, rather than Mozilla being the "owners" of Rust. Not arguing your point, and there's a chance I'm awfully wrong, but as I recall it, Mozilla are more the champions of the language rather than the owner of it. Regardless, it's a really neat language
  - steveklabnik 8y ago
    That’s correct; we operate on consensus, and about a hundred people are involved in Rust governance. Only about six are employees of Mozilla.
    - hardwaresofton 8y ago
      TIL - to what extent does Mozilla still sponsor rust? Looking at the governance docs[0], there's no mention of Mozilla anywhere at all. This taken with the fact there are less than 10 people in a hundred from mozilla makes it pretty clear that rust has come a long way from being a mozilla research project (which I guess should have been obvious to me as well). What is the extent of support from mozilla? I can't find a list of other corporate sponsors? [0]: https://www.rust-lang.org/governance https://www.rust-lang.org/governance
max_ 8y ago
For those of you interested in formal verification & semantics recommend you have a look at the K framework[0] that can be used for easily creating Formal Semantics. [0]: https://runtimeverification.com/blog/k-framework-an-overview/ https://runtimeverification.com/blog/k-framework-an-overview...
stebann 8y ago
Gonna try Rust. Seems pretty!
loki49152 8y ago
This is going to cause confusion with Rust - the game - and Oxide, its 3rd party mod plugin framework.
- twothumbsup 8y ago
  Rust-lang came first

223 points by rachitnigam 8y ago

One of the examples in the paper has some code that you can't actually write in Rust, it's close to this: let msg: &'msg str = "Hello World"; You can write something similar and allow the compiler to infer the lifetime: let msg: &'_ str = "Hello World"; I often find myself declaring the type when I get into confusing type issues in Rust, but you can't do that as easily with lifetimes. With non-lexical lifetimes this has been less of an issue, but still there are times when I would like to be able to declare the lifetime like the first example. This error example shows the valid uses of lifetimes: https://doc.rust-lang.org/nightly/error-index.html#E0261 https://doc.rust-lang.org/nightly/error-index.html#E0261

webkike 8y ago
I believe you can actually name the lifetime of a block, via the same mechanism that makes labeled breaks and continues possible.
- bluejekyll 8y ago
  Do you have an example of what you mean?
  - coolreader18 8y ago
    Like this: 'a: { let a_var: u32 = 42; let a_ref: &'a u32 = &a_var; } // ^^^^^ only valid in 'a: {}
    - gpm 8y ago
      That doesn't compile with "use of undeclared lifetime name `'a`"
      - steveklabnik 8y ago
        You can name loop labels like this, but you cannot use them to introduce actual lifetimes, that’s right.
- Retra 8y ago
  I think that was just a proposal that never got accepted? Never see it in real code either way.

twothumbsup 8y ago

Love seeing some good PL research from Northeastern in the news! I was part of the capstone class they ran back in 2015 where we used/learned the alpha version of Rust that had just been released. Great experience.

wolco 8y ago

Love the name. Could not describe what it is/does any better.

ipodopt 8y ago

Please correct me if I am wrong. They produced a simpler modified version of Rust called Oxide that focused on ownership and borrowing. They did did so they could translate it to a formal system and validate it in an easy to understand way.

Groxx 8y ago
That's normal for programming language formal verification, from what I've seen. The question is always "how simplified is it", and if it's simplified to the point of uselessness. There's usually something to be learned (and often bugs to be fixed) from even the most-simplified version, but AFAICT "full" language verification is basically never done (except on toy[1] languages). edit: [1]: "toy" implying "not intended for broad use", not any kind of "pointless" or "just for fun", to be clear. maybe there's a better term I should be using. so basically all "this language is designed to be formally verified and it does something interesting" languages fall into this category, because it's really not expected to be generally usable - it exists to demonstrate something, and at best become a feature of another language eventually.
- floofy222 8y ago
  Usually these inform tools that can be used to detect rule violations. For example, the rust constant evaluator can execute almost all Rust at run-time except for FFI. This allows you to write `cargo miri test` in your project, and run your unit tests in the constant evaluator. The constant evaluator executes the program based on rules given by models like this, and if you perform an action that violates one of the rules, they report an error. For example, this program mutates a variable while a shared borrow (which excludes mutation) is alive via a raw pointer fn main() { let mut a = 13; let b = &a; let c = b as *const _ as *mut _; unsafe { *c = 42; } println!("b = {}", b); } On the playground it prints "b = 42" (https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=6a1915616357b53e8d45d4a81c7b1bd1 https://play.rust-lang.org/?version=stable&mode=debug&editio...). The playground has a `Tools` button, that allows you to run the program under `miri` (the constant evaluator). When doing so, it prints: error[E0080]: constant evaluation error: borrow being accessed (Alias(None)) does not exist on the borrow stack --> src/main.rs:5:14 | 5 | unsafe { *c = 42; } | ^^^^^^^ borrow being accessed (Alias(None)) does not exist on the borrow stack error: aborting due to previous error The error messages of the constant evaluator aren't great yet, but that basically tells you that it couldn't find a suitable mutable borrow to mutate the variable, so the access is undefined behavior.

cttet 8y ago

I really hope there would be a ML-like syntax for Rust. The current one is not so friendly to read.

hardwaresofton 8y ago
Agree -- these days whenever I try to pick between Haskell and Rust for a new project I go Haskell because of the much nicer syntax (though it took some getting used to). I also have almost 0 interest in OCaml due to the syntactic choices they've made.
- TheAsprngHacker 8y ago
  I use OCaml and I am also writing my own ML dialect, so I would like to ask, what exact aspects of the OCaml syntax don't you like, and what parts of the Haskell syntax do you like in particular? (For example, do you prefer indentation-based syntax?)
  - hardwaresofton 8y ago
    I honestly don't know how to explain it really well, but OCaml is much noisier than Haskell in my opinion. Many times when I see code snippets in OCaml they're not as nice as they look in Haskell, though they're really similar. The small difference seems to snowball when the code gets increasingly complicated. Compare functor's definitions in either syntax: module type FUNCTOR = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end;; class Functor where fmap :: (a -> b) -> f a -> f b The latter looks cleaner to me. There are other ways you could write it (for example if you turned on explicit forall it would get messier. At this point I start skipping talks at conferences when they're in Scala because the amount of noise in the syntax is near unbearable to me (and there's likely to be a haskell talk on a similar topic) -- OCaml is much better in that respect, but I still find Haskell's syntax to be easiest on the eyes. OCaml might be more pedantically descriptive though, it seems to be more explicit about everything.
    - 8y ago

hardwaresofton 8y ago

> Rust is a major advancement in industrial programming languages due in large part to its success in bridging the gap between low-level systems programming and high-level application programming So glad to see this sentiment echoed somewhere outside my own head/conversations. Rust is a game changer, it brings something novel (ownership/borrowing, research-grade type system) to systems programming, and it brings great features for high level programming (type inference, strict control, high level abstraction support, "zero-cost" abstractions), and is basically a paragon of good open-source development in the open. On top of all of that it's done by Mozilla, with so much less resources than other companies, and a demonstrated interest in making software that's good for everyone.

svrtknst 8y ago
> On top of all of that it's done by Mozilla IIRC it's open-source with a fairly wide set of contributors, with Mozilla being a major one, rather than Mozilla being the "owners" of Rust. Not arguing your point, and there's a chance I'm awfully wrong, but as I recall it, Mozilla are more the champions of the language rather than the owner of it. Regardless, it's a really neat language
- steveklabnik 8y ago
  That’s correct; we operate on consensus, and about a hundred people are involved in Rust governance. Only about six are employees of Mozilla.
  - hardwaresofton 8y ago
    TIL - to what extent does Mozilla still sponsor rust? Looking at the governance docs[0], there's no mention of Mozilla anywhere at all. This taken with the fact there are less than 10 people in a hundred from mozilla makes it pretty clear that rust has come a long way from being a mozilla research project (which I guess should have been obvious to me as well). What is the extent of support from mozilla? I can't find a list of other corporate sponsors? [0]: https://www.rust-lang.org/governance https://www.rust-lang.org/governance

max_ 8y ago

For those of you interested in formal verification & semantics recommend you have a look at the K framework[0] that can be used for easily creating Formal Semantics. [0]: https://runtimeverification.com/blog/k-framework-an-overview/ https://runtimeverification.com/blog/k-framework-an-overview...

stebann 8y ago

Gonna try Rust. Seems pretty!

loki49152 8y ago

This is going to cause confusion with Rust - the game - and Oxide, its 3rd party mod plugin framework.

twothumbsup 8y ago
Rust-lang came first