Oxide: A Formal Semantics for Rust
arxiv.org
arxiv.org
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.
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
What is the extent of support from mozilla? I can't find a list of other corporate sponsors?
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.
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.
let msg: &'msg str = "Hello World";
let msg: &'_ str = "Hello World";
This error example shows the valid uses of lifetimes: https://doc.rust-lang.org/nightly/error-index.html#E0261
'a: {
let a_var: u32 = 42;
let a_ref: &'a u32 = &a_var;
} // ^^^^^ only valid in 'a: {}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.
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.
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);
}
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
It's been done for full Standard ML, and I believe Java as well. But yeah, it's rare.
[0]: https://runtimeverification.com/blog/k-framework-an-overview...
I also have almost 0 interest in OCaml due to the syntactic choices they've made.
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
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.
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
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...