From 0f9efaa7c9ae3f2a7546aea66ee7affcf1ae7202 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 8 Aug 2022 09:58:52 -0400 Subject: [PATCH] the Cool Bear can be on this blog :) --- personal/_posts/2022-08-08-minirust.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/personal/_posts/2022-08-08-minirust.md b/personal/_posts/2022-08-08-minirust.md index 00d4e31..b78dfe2 100644 --- a/personal/_posts/2022-08-08-minirust.md +++ b/personal/_posts/2022-08-08-minirust.md @@ -23,14 +23,14 @@ English language, on the other hand, is not very precise. 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. -- 2.30.2