X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/a7be6d6b7e841ec4ea671fc38fb5902e7b7cfbea..04fb252e44356ce32328819b1a42df753b095190:/personal/_posts/2015-10-12-formalizing-rust.md?ds=sidebyside

diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md
index b867ffb..ad28165 100644
--- a/personal/_posts/2015-10-12-formalizing-rust.md
+++ b/personal/_posts/2015-10-12-formalizing-rust.md
@@ -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).
-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 -->
 
@@ -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.
-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