Translating it to real Rust means we can actually execute the reference interpreter and test it, and translating it to Coq means we can start proving theorems about it.
But I am getting waaaay ahead of myself, these are rather long-term plans.
-[^bear]: Is that someone the [cool bear](https://fasterthanli.me/articles/) making an appearance on my blog? We'll never know... and also I'd have to ask fasterthanlime for permission and didn't plan this well enough. ;)
+[^bear]: Is that someone the [cool bear](https://fasterthanli.me/articles/) making an appearance on my blog? We'll never know... and also I'd have to ask fasterthanlime to ask them for permission and didn't plan this well enough. ;)
So, if you want to look into my brain to see how I see Rust programs, then please go check out [MiniRust](https://github.com/RalfJung/minirust).
The README explains the scope and goals, the general structure, and the details of pseudo Rust, as well as a comparison with some related efforts.