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.