It turns out that the underlying reason for this observation is also a nice illustration for the concept of *semantic types* that comes up in my [work on formalizing Rust]({% post_url 2015-10-12-formalizing-rust %}) (or rather, its type system).
Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.
-**Update (Jan 11th):** Clarified the role of privacy; argued why `evil` is the problem.
+**Update (2016-01-11):** Clarified the role of privacy; argued why `evil` is the problem.
<!-- MORE -->
[^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).
-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.