[HN Gopher] Oxide: The Essence of Rust (2020)
       ___________________________________________________________________
        
       Oxide: The Essence of Rust (2020)
        
       Author : VitalyAnkh
       Score  : 67 points
       Date   : 2021-05-15 10:56 UTC (12 hours ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | rrdharan wrote:
       | Amusing name collision with https://oxide.computer/ (who also use
       | Rust).
        
       | phab wrote:
       | This should really have a [2019] tag
        
       | HenryKissinger wrote:
       | I 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.
        
         | tobz1000 wrote:
         | 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.
        
           | senkora wrote:
           | Or at least take you to a disambiguation page where both are
           | listed.
        
         | smt88 wrote:
         | 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
        
         | qzw wrote:
         | I know a search engine that ranks pages the way you like. It's
         | called AltaVista.
        
         | senkora wrote:
         | But the Amazon rainforest is similarly named after the Amazon
         | warriors from Greek mythology.
        
         | bschwindHN wrote:
         | I'm a bit disappointed you're not the real Henry Kissinger.
        
         | sidpatil wrote:
         | 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.
        
           | cjohnson318 wrote:
           | 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.
        
       | siraben wrote:
       | I'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
       | 
       | [1] https://arxiv.org/pdf/2005.11710.pdf
        
         | jamespwilliams wrote:
         | The most interesting parts of my comp sci degree were in this
         | area - "models of computation", and later "type systems for
         | programming languages", which started with lambda calculus, and
         | culminated in studying Haskell's type system (and its relation
         | to lambda calculus).
         | 
         | It was surprising to me to discover how logical and
         | mathematical Haskell's type system is.
         | 
         | It's the kind of topic that I'd probably not ever have thought
         | about if I didn't do a degree, but has had an impact on how I
         | view other areas of computer science.
        
       ___________________________________________________________________
       (page generated 2021-05-15 23:02 UTC)