move twinsem paper to new folder

[web.git] / personal / _posts / 2022-08-08-minirust.md

diff --git a/personal/_posts/2022-08-08-minirust.md b/personal/_posts/2022-08-08-minirust.md
index f13285b26a5c8fd63a377a1180c97f64e390a8bf..8158cb02515aa55c21ab2636ed78c0914636b140 100644 (file)
--- a/personal/_posts/2022-08-08-minirust.md
+++ b/personal/_posts/2022-08-08-minirust.md
@@ -15,7 +15,9 @@ We have [Miri](https://github.com/rust-lang/miri/), which is a much quicker orac
 
 So I have promised for a long time to find some more holistic way to write down my thoughts on unsafe Rust semantics.
 I thought I could do it in 2021, but I, uh, "slightly" missed that deadline... but better late than never!
 
 So I have promised for a long time to find some more holistic way to write down my thoughts on unsafe Rust semantics.
 I thought I could do it in 2021, but I, uh, "slightly" missed that deadline... but better late than never!

-At long last, I can finally present to you: [**MiniRust**](https://github.com/RalfJung/minirust).
+At long last, I can finally present to you: [**MiniRust**](https://github.com/RalfJung/minirust).[^name]
+
+[^name]: I am beginning to wonder if this name was a bad choice. Naming is not my strong suit. Maybe "CoreRust" would have been better? Alas...

 
 The purpose of MiniRust is to describe the semantics of an interesting fragment of Rust in a way that is both precise and understandable to as many people as possible.
 These goals are somewhat at odds with each other -- the most precise definitions, e.g. carried out in the Coq Proof Assistant, tend to not be very accessible.
 
 The purpose of MiniRust is to describe the semantics of an interesting fragment of Rust in a way that is both precise and understandable to as many people as possible.
 These goals are somewhat at odds with each other -- the most precise definitions, e.g. carried out in the Coq Proof Assistant, tend to not be very accessible.


@@ -23,17 +25,19 @@ 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 for permission and didn't plan this well enough. ;)
+[^bear]: Thanks to fasterthanlime for facilitating the bear's appearance on this blog.
+
+**Update (2023-02-13):** "Pseudo Rust" has now been renamed to "specr lang", the language of the work-in-progress "specr" tool that can translate specr lang into Rust code to make specifications executable. **/Update**

 
 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).
 
 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.
+The README explains the scope and goals, the general structure, and the details of ~~pseudo Rust~~ specr lang, as well as a comparison with some related efforts.

 
 In particular I find that the concept of "places" and "values", which can be rather mysterious, becomes a lot clearer when spelled out like that, but that might just be me.
 I hasten to add that this is *very early work-in-progress*, and it is *my own personal experiment*, not necessarily reflecting the views of anyone else.
 
 In particular I find that the concept of "places" and "values", which can be rather mysterious, becomes a lot clearer when spelled out like that, but that might just be me.
 I hasten to add that this is *very early work-in-progress*, and it is *my own personal experiment*, not necessarily reflecting the views of anyone else.


@@ -48,7 +52,9 @@ On the other hand, there are many things that it *can* explain in full precision
 - what happens when *casting* between pointers and integers
 - padding (that's why tuples can have 2 elements, so there can be padding between them)
 
 - what happens when *casting* between pointers and integers
 - padding (that's why tuples can have 2 elements, so there can be padding between them)
 

-If you re not used to reading interpreter source code, then I guess this can be rather jarring, and there is certainly a *lot* of work that could and should be done to make this more accessible.
-But just being able to talk about these questions with precision *at all* has already lead to some interesting discussions in the UCG WG (some of which made me change my mind, and change MiniRust accordingly), so for now it is serving its purpose, and maybe some of you can find it useful, too.
-And hopefully we can use it as a starting place for seriously tackling the issue of an *official* specification of Rust.
+If you are not used to reading interpreter source code, then I guess this can be rather jarring, and there is certainly a *lot* of work that could and should be done to make this more accessible.
+(Like, examples. I hear people like examples.)
+But just being able to talk about these questions with precision *at all* has already lead to some interesting discussions in the UCG WG, some of which made me change my mind -- thanks in particular to @digama0, @JakobDegen, and @alercah for engaging deeply with my ideas.
+So for now it is serving its purpose, and maybe some of you can find it useful, too.
+Hopefully we can even use this as a starting place for seriously tackling the issue of an *official* specification of Rust.

 More on that soon. :)
 More on that soon. :)