So my compromise solution is to write down the semantics in a format that is hopefully known to everyone who could be interested: in Rust code.
Specifically, MiniRust is specified by a *reference interpreter* that describes the step-by-step process of executing a MiniRust program, *including* checking at each step whether the program has Undefined Behavior.
-"Hold on", I hear someone say, "you are defining Rust in Rust code? Isn't that cyclic?"[^bear]
+"Hold on", I hear a [Cool Bear](https://fasterthanli.me/articles/) say, "you are defining Rust in Rust code? Isn't that cyclic?"[^bear]
Well, yes and no. It's not *really* Rust code.
It's what I call "pseudo Rust", uses only a tiny fragment of the language (in particular, no `unsafe`), and then extends the language with some conveniences to make things less verbose.
The idea is that anyone who knows Rust should immediately be able to understand what this code means, but also hopefully eventually if this idea pans out we can have tooling to translate pseudo Rust into "real" languages -- in particular, real Rust and Coq.
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 to ask them for permission and didn't plan this well enough. ;)
+[^bear]: Thanks to fasterthanlime for facilitating the bear's appearance on this blog.
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.
projects / web.git / commitdiff