Oxide: The Essence of Rust (2020)
arxiv.org
Oxide: The Essence of Rust (2020)
1–10 of 14 posts
Re: Oxide: The Essence of Rust (2020)
#2Amusing name collision with https://oxide.computer/ (who also use Rust).
Re: Oxide: The Essence of Rust (2020)
#3I don't like the trend of corporate names taking real names and repurposing them.
The first results of a Google search for "Amazon" are the company. Not the river.
The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from.
And a Google search for "Rust" returns links to the programming language and the video game, before the chemical reaction.
Re: Oxide: The Essence of Rust (2020)
#4I don't like the trend of corporate names taking real names and repurposing them. The first results of a Google search for "Amazon" are the company. Not the river. The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from. And a Google search for "Rust" returns links to the programming language and the video game, before the chemi…
I did a couple searches of my own too:
The first results of a Google search for "C" are the programming language. Not the letter.
The first results of a Google search for "Python" are the programming language. Not the snake.
Re: Oxide: The Essence of Rust (2020)
#5I'm studying programming language semantics and papers like these are quite valuable in understanding type systems of real languages, see also Featherweight Java[0] and Featherweight Go[1]. At first it looks like a lot to take in, but when you start with far simpler type systems like typed arithmetic expressions and simply-typed lambda calculus, you see the same definitions and metatheorems (properties about the type system) appear over and over again (including in this paper). In particular, the pieces you see repeated are:
- the terms and types of the language
- the values (a subset of terms)
- the evaluation relation, telling you how you go from one term to the next
- the typing relation, telling you how you build well-typed terms and what their types are
- Progress states that if you have a well-typed term, it either is a value or it can take one step of evaluation
- Preservation states you that if you have a well-typed term of type T and it takes a step of evaluation, the resulting term still has type T
And we have the slogan, safety = progress + preservation.
I should also note that past a certain level of complexity of type system, you definitely would want to use a theorem prover such as Coq to formally verify and automate easy cases. The proofs themselves are actually quite boring (which is a good thing!).
[0] https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf
Re: Oxide: The Essence of Rust (2020)
#6I don't like the trend of corporate names taking real names and repurposing them. The first results of a Google search for "Amazon" are the company. Not the river. The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from. And a Google search for "Rust" returns links to the programming language and the video game, before the chemi…
I did a couple searches of my own too: The first results of a Google search for "C" are the programming language. Not the letter. The first results of a Google search for "Python" are the programming language. Not the snake.
Some of this might be your search bubble. If I had to wade through pages of snakes every time I Googled "python something", then I would go insane.
Re: Oxide: The Essence of Rust (2020)
#7I don't like the trend of corporate names taking real names and repurposing them. The first results of a Google search for "Amazon" are the company. Not the river. The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from. And a Google search for "Rust" returns links to the programming language and the video game, before the chemi…
This is why my first instinct when looking something up is to check Wikipedia, not a search engine: the original article will take precedence rather than the more popular thing.
Re: Oxide: The Essence of Rust (2020)
#8I don't like the trend of corporate names taking real names and repurposing them. The first results of a Google search for "Amazon" are the company. Not the river. The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from. And a Google search for "Rust" returns links to the programming language and the video game, before the chemi…
It's not a trend. It's the way companies have always been named. Historically, many were named after people or places.
If you want to search for things that exist, just add a Wikipedia quick search to your browser
Re: Oxide: The Essence of Rust (2020)
#9This should really have a [2019] tag
Re: Oxide: The Essence of Rust (2020)
#10I don't like the trend of corporate names taking real names and repurposing them. The first results of a Google search for "Amazon" are the company. Not the river. The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from. And a Google search for "Rust" returns links to the programming language and the video game, before the chemi…
I know a search engine that ranks pages the way you like. It's called AltaVista.