For the last two weeks at work, my little PLT Redex model of Rust has been taking shape. It's been a lot of fun. I started with lambda calculus, like y' do, but it became clear that that doesn't really make sense as a language to grow Rust out of; for one thing, functions are not expressions in Rust.1 Still, one of the nice, reusable pieces to have come out of that attempt is that I implemented the λgc language from "Abstract Models of Memory Management" by Morrisett, Felleisen and Harper. This was a good way to figure out what I was doing with Redex. It was instructive to go from reading the paper to having running code for λgc. The paper didn't gloss over a lot, but it did gloss over a little! The hardest part was, as usual, Naming Things.
I was able to borrow some ideas from λgc for the Rust model, which I'm calling baby-rust. Whereas λgc models a program as an initially empty heap followed by an expression, baby-rust models a program as a list of "items" (definitions of functions and types), followed by an initially empty heap, followed by an expression. I'm still not modeling the stack explicitly, so this only takes me half as far as I need to go for a realistic model, but items, at least, are a real concept in Rust, so it's a start.
Just for fun, I threw in a baby-rust typechecker, named typeck just like the real Rust typechecker is, even though my brain still insists on pronouncing that as "type eccch". Like Rust, baby-rust has tuples and tuple indexing operations. For instance, in baby-rust you can pull
bar out of the tuple
(tup foo bar baz) using the expression
(index (tup foo bar baz) 1). The best part was when I realized that any old thing that evaluates to a number should be able to appear where the
1 is in that expression, and that therefore, in order to determine the type of the whole expression, I needed to know not only that that thing is a number, but which number it is.2 So now the typechecker calls off to the reduction relation! Excellent!
I'm ready to start thinking seriously about self-types now, so I'm going to try to put the model on the shelf and come back to it later, but I'm a little worried that I won't be able to stay away. Building languages out of ((languages out of) ...) Scheme just feels so good.
- Before you flip out and stab: Rust is still mostly an expression language, and it does have something called
bindexpressions, which are like closures. I'm not modeling those yet, though. Okay, carry on flipping out and stabbing.
- In principle, I could also reject the program as ill-typed if it tried to index out of bounds. I'm actually almost already doing that: a call to Racket's
list-refraises a run-time error, but
list-ref's run-time is baby-rust's typechecking time, so I'm "statically" rejecting baby-rust programs that index out of bounds before I "run" them. Dependent types haha woo? Now we just need to implement all high-assurance systems software in Redex and we're set, right?