the Cool Bear can be on this blog :)

diff --git a/ralf/_posts/2022-08-08-minirust.md b/ralf/_posts/2022-08-08-minirust.md
index 00d4e312d723ad786635a15f6499eedbbcebb880..b78dfe2e4d948c66101e0ce267d8563e7ed778cf 100644 (file)
--- a/ralf/_posts/2022-08-08-minirust.md
+++ b/ralf/_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.
 
 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.
 
 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.
 
 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.