If anyone here has an HN account, perhaps you could comment and clarify that I wrote that thing in April 2011, when Rust was a very different language, and even then, I only modeled a tiny subset of the language.
I don't really know what has changed in Rust over time (though a fair amount has changed in Redex (and some in Racket) since this was written, particularly an improved way to write a type checker). Skimming over the current version of the Rust tutorial, it looks like the model doesn't include the full variety of pointer types (just boxes with no notion of ownership), pattern matching/algebraic data types (it does have tuples and projection), or concurrency, and the model's type system is monomorphic. One TODO is for the stack (I'm not sure what there is to do for that). The other is for assignment. This would typically be a reduction step that changes the contents of the heap, but maybe there was still some question about the details of that change (such as whether/when to drop unreachable heap cells). I expect Rust's concurrency would require some more thought about how best to represent program state and some changes to the type system.
If anyone here has an HN account, perhaps you could comment and clarify that I wrote that thing in April 2011, when Rust was a very different language, and even then, I only modeled a tiny subset of the language.