credit where credit is due

[web.git] / ralf / _posts / 2015-10-12-formalizing-rust.md

diff --git a/ralf/_posts/2015-10-12-formalizing-rust.md b/ralf/_posts/2015-10-12-formalizing-rust.md
index b867ffb80a9f4e0bd2b69871d22cc5d8f4e67e21..43a1a710099c870734febcaa33256a3016aec64f 100644 (file)
--- a/ralf/_posts/2015-10-12-formalizing-rust.md
+++ b/ralf/_posts/2015-10-12-formalizing-rust.md
@@ -6,7 +6,7 @@ reddit: /rust/comments/3ofkz6/formalizing_rust/
 
 My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.
 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.
 
 My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.
 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.

-Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](http://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.
+Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](https://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.

 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 
 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 


@@ -15,7 +15,9 @@ It's going to be fun! Honestly, that's enough of a reason for me.
 But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust.
 There are lots of things that can be done about such bugs -- my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust.
 This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf).
 But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust.
 There are lots of things that can be done about such bugs -- my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust.
 This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf).

-However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do.
+However, we (at my [research group](https://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do as part of the [RustBelt](https://plv.mpi-sws.org/rustbelt/) research project.
+
+**Update:** Added link to RustBelt website.

 
 <!-- MORE -->
 
 
 <!-- MORE -->
 


@@ -74,7 +76,7 @@ For example, to check that a function is semantically well-typed, you check what
 It doesn't matter *how* the function performs these operations.
 This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules.
 Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use.
 It doesn't matter *how* the function performs these operations.
 This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules.
 Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use.

-Lucky enough, my advisor [Derek Dreyer](http://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!
+Lucky enough, my advisor [Derek Dreyer](https://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!

 
 ## What We Are Doing
 
 
 ## What We Are Doing