From: Ralf Jung Date: Tue, 19 Nov 2019 13:20:56 +0000 (+0100) Subject: typo X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/35f31db1465e69b61738d0ec94fdeafb0cb3403f typo --- diff --git a/ralf/_posts/2019-11-18-stacked-borrows-paper.md b/ralf/_posts/2019-11-18-stacked-borrows-paper.md index 467b085..39ce8ea 100644 --- a/ralf/_posts/2019-11-18-stacked-borrows-paper.md +++ b/ralf/_posts/2019-11-18-stacked-borrows-paper.md @@ -13,7 +13,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. -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.)