add Reddit link

[web.git] / personal / _posts / 2019-11-18-stacked-borrows-paper.md

diff --git a/personal/_posts/2019-11-18-stacked-borrows-paper.md b/personal/_posts/2019-11-18-stacked-borrows-paper.md
index 467b0854f425651df5101fc3fc74b4242d6c9a1f..49d7dc7a4ba27d652fe98a25510feae7bcc210c3 100644 (file)
--- a/personal/_posts/2019-11-18-stacked-borrows-paper.md
+++ b/personal/_posts/2019-11-18-stacked-borrows-paper.md
@@ -1,6 +1,7 @@
 ---
 title: "Stacked Borrows: An Aliasing Model for Rust (the paper)"
 categories: research rust
 ---
 title: "Stacked Borrows: An Aliasing Model for Rust (the paper)"
 categories: research rust

+reddit: /rust/comments/dy8avz/stacked_borrows_an_aliasing_model_for_rust_the/

 ---
 
 I have [blogged]({% post_url 2019-05-21-stacked-borrows-2.1 %}) a [few]({% post_url 2019-04-30-stacked-borrows-2 %}) times before about [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md), my proposed aliasing model for Rust.
 ---
 
 I have [blogged]({% post_url 2019-05-21-stacked-borrows-2.1 %}) a [few]({% post_url 2019-04-30-stacked-borrows-2 %}) times before about [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md), my proposed aliasing model for Rust.


@@ -13,7 +14,7 @@ If you have already read my blog posts, the paper does not say much you have not
 However, the paper is the most coherent and most complete introduction to Stacked Borrows so far.
 So if you were always confused by some aspect of Stacked Borrows, or if you have not read the previous blog posts, the paper is a great way to learn about Stacked Borrows.
 
 However, the paper is the most coherent and most complete introduction to Stacked Borrows so far.
 So if you were always confused by some aspect of Stacked Borrows, or if you have not read the previous blog posts, the paper is a great way to learn about Stacked Borrows.
 

-If there is nothing new, you may wonder what to us so long, then, and why we needed 4 people for that?
+If there is nothing new, you may wonder what took us so long, then, and why we needed 4 people for that?

 The answer is that my coauthor Hai, with some help from Jeehoon and me, took on the Herculean task of [formalizing Stacked Borrows in Coq](https://gitlab.mpi-sws.org/FP/stacked-borrows) and then formally verifying that some key optimizations are actually sound under that model.
 Those proofs turned out to be more complex to carry out than we expected, but now I am sure that what I claimed about Stacked Borrows in previous posts is actually correct.
 (In fact we were not able to complete the proof in time for the conference submission deadline, but lucky enough the reviewers were convinced enough by the informal description and the evaluation with Miri that they still accepted the paper.)
 The answer is that my coauthor Hai, with some help from Jeehoon and me, took on the Herculean task of [formalizing Stacked Borrows in Coq](https://gitlab.mpi-sws.org/FP/stacked-borrows) and then formally verifying that some key optimizations are actually sound under that model.
 Those proofs turned out to be more complex to carry out than we expected, but now I am sure that what I claimed about Stacked Borrows in previous posts is actually correct.
 (In fact we were not able to complete the proof in time for the conference submission deadline, but lucky enough the reviewers were convinced enough by the informal description and the evaluation with Miri that they still accepted the paper.)