Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
A PLT Redex model of a toy language that is almost, but not quite, entirely unlike Rust
Racket
Branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
.gitignore
README
lambda-gc.rkt
rust-test.rkt
rust.rkt

README

rust-redex: A PLT Redex model of (a very, very small subset of) the
Rust programming language.

Why bother to create a model of Rust?

  * By creating a model, we create notation, and notation can become
    the basis with which people sketch ideas, so that we have a common
    language of reasoning about Rust; "even if we don't use formal
    methods, they can guide our informal methods of reasoning" --
    dherman

  * With regard to proposed language features, people sometimes say,
    "Feature X?  I don't even know what that would mean in Rust."  A
    model could help us figure out what Feature X would mean, without
    having to actually implement it in Rust proper.  By itself, the
    model won't prove that a proposed feature will work as intended,
    but using the model we might be able to demonstrate that it
    *won't* work as intended, avoiding an expensive mistake.

  * People also sometimes say, "I didn't realize that you could do
    so-and-so in Rust until I noticed that it was implemented while I
    was hacking on the compiler today."  One shouldn't have to look at
    the implementation of the compiler to find out what the syntax and
    semantics of Rust is.  Right now, the distinction is somewhat
    academic since pretty much all Rust users are also Rust
    implementors, but (hopefully) it won't be that way forever.  We
    don't expect users to necessarily play with the Redex model, but
    from the Redex model we can generate artifacts that can go in the
    documentation that users read.
Something went wrong with that request. Please try again.