add Coq typeclass index problem draft

[web.git] / personal / _posts / 2017-05-23-internship-starting.md

diff --git a/personal/_posts/2017-05-23-internship-starting.md b/personal/_posts/2017-05-23-internship-starting.md
index b20c7c30560795a4be667d5ee9475693f4410fe9..eb523b50fe493537496f2d20c4f831d10ee61e5a 100644 (file)
--- a/personal/_posts/2017-05-23-internship-starting.md
+++ b/personal/_posts/2017-05-23-internship-starting.md
@@ -14,7 +14,7 @@ I meant to write this yesterday, but the morning was filled with bureaucratics a
 (But don't tell Aaron, my manager, or Niko, my mentor -- I was of course supposed to be working. ;)
 
 So, what concretely will I be doing in the next three months?
 (But don't tell Aaron, my manager, or Niko, my mentor -- I was of course supposed to be working. ;)
 
 So, what concretely will I be doing in the next three months?

-Based on [my prior posts]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %}) and me being in the [unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) (which I totally forgot to announce here... I'm not good at this blogging thing, am I?), it should not be surprising that my main project is going to be related to unsafe code.
+Based on [my prior posts]({% post_url 2016-01-09-the-scope-of-unsafe %}) and me being in the [unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) (which I totally forgot to announce here... I'm not good at this blogging thing, am I?), it should not be surprising that my main project is going to be related to unsafe code.

 More specifically, we want to figure out ways to specify what unsafe code is and what it is not allowed to do (i.e., when its behavior is well-defined, and when it is undefined).
 Ultimately, the way I think this should be specified (and lucky enough, my new bosses agree on this) is by defining, for every possible Rust (or rather, MIR) program one could write, what that program is going to do when it is executed.
 
 More specifically, we want to figure out ways to specify what unsafe code is and what it is not allowed to do (i.e., when its behavior is well-defined, and when it is undefined).
 Ultimately, the way I think this should be specified (and lucky enough, my new bosses agree on this) is by defining, for every possible Rust (or rather, MIR) program one could write, what that program is going to do when it is executed.