add draft on Tree Borrows

[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 b78dfe2e4d948c66101e0ce267d8563e7ed778cf..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.


@@ -32,8 +34,10 @@ But I am getting waaaay ahead of myself, these are rather long-term plans.
 
 [^bear]: Thanks to fasterthanlime for facilitating the bear's appearance on this blog.
 
 
 [^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.