Hacker News new | past | comments | ask | show | jobs | submit login
Oxide: A Formal Semantics for Rust (arxiv.org)
223 points by rachitnigam 17 days ago | hide | past | web | favorite | 30 comments

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

> 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

That’s correct; we operate on consensus, and about a hundred people are involved in Rust governance. Only about six are employees of Mozilla.

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

Mozilla pays for those people to work on Rust full time; they hire individuals for short-term contracts for specific work; they pay the CI and hosting bills. They also provide legal support.

Some other companies do sponsor work at times as well. A recent hot topic of discussion is “does a Rust foundation make sense”, there are good arguments for and against. We’ll see.

Oh, and note that that number is people who are decision makers in the project; about 120~150 distinct people contribute to each six-week release. We’ve had 2786 distinct people contribute. And that’s only to rust-lang/rust; not Cargo, not any of the libraries the team maintains, not any of the other kinds of work that doesn’t produce a commit.

> We’ve had 2786 distinct people contribute. And that’s only to rust-lang/rust; not Cargo, not any of the libraries the team maintains, not any of the other kinds of work that doesn’t produce a commit.

To put this into more context: a lot of the code shipped with the Rust toolchain does not live in rust-lang/rust.

Some parts of the standard library (HashMap, HashSet, C FFI, intrinsics, etc.) are used as dependencies. All of the tools (the linter, language server, rustfmt, rustup, cargo, etc.) are dependencies. Many compiler components like miri (constant evaluator), chalk (type queries), polonius (borrow checking), etc. are also dependencies. The Cranelift code generation backend can be dynamically used and does not live in rust-lang/rust, etc. Then there is the RFC repository, and probably other things.

Counting contributors for such a distributed infrastructure isn't easy, but the number of contributors to rust-lang/rust isn't super meaningful.

One might be able to do better by finding commits to rust-lang/rust that update "Rust" submodules (e.g. not LLVM), and adding the contributors to those repos from the last update. One might also want to find commits that update versions of rust-lang/rust dependencies, and for those that live in the rust project (or that have dependencies there), count the contributors from the last version, etc.

The Rust project has seen significant modularization over the last couple of years, and the more modular it gets, the less meaningful "contributors to rust-lang/rust" becomes, and the less accurate the "Thanks!" pages of each release become.

Yep. Still want to re-do it. Sigh.

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.

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

I believe you can actually name the lifetime of a block, via the same mechanism that makes labeled breaks and continues possible.

I think that was just a proposal that never got accepted? Never see it in real code either way.

Do you have an example of what you mean?

Like this:

  'a: {
      let a_var: u32 = 42;
      let a_ref: &'a u32 = &a_var;
  } //    ^^^^^ only valid in 'a: {}

That doesn't compile with "use of undeclared lifetime name `'a`"

You can name loop labels like this, but you cannot use them to introduce actual lifetimes, that’s right.

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.

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.

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

> AFAICT "full" language verification is basically never done

It's been done for full Standard ML, and I believe Java as well. But yeah, it's rare.

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

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

Rust-lang came first

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

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.

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?)

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

     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.

>but OCaml is much noisier than Haskell in my opinion.

I would rather say explicit, and that was a breath of fresh air to me after Haskell. As for your example, how many instances do you need to write all the type classes you need?

In OCaml I could just write all the functions I need in a file, and this file-module would implement all the signatures, thanks to the structural typing, now condiser:

    type 'a t
    val bind : 'a t -> ('a -> 'b t) -> 'b t
    val apply : ('a -> 'b) t -> 'a t -> 'b t
    val map : ('a -> 'b) -> 'a t -> 'b t
    val show : 'a t -> ('a -> string) -> string
    val return : 'a -> 'a t
instead of

    instance Functor a => Functor (Type a) where
       fmap        :: (a -> b) -> f a -> f b

    instance Applicative a => Applicative (Type a) where
       <*>         :: f (a -> b) -> f a -> f b

    instance Show (Type a) where
       show        :: a -> string

    instance Monad...

which is more verbose?

This is pretty nitpicky, but I really dislike the postfix syntax for type constructor application.

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

Gonna try Rust. Seems pretty!

Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact