Capitalize Things

diff --git a/ralf/_posts/2015-10-12-formalizing-rust.md b/ralf/_posts/2015-10-12-formalizing-rust.md
index 9f5dc7ae39225a5ee81ee0ac1be4c0e60275de83..b867ffb80a9f4e0bd2b69871d22cc5d8f4e67e21 100644 (file)
--- a/ralf/_posts/2015-10-12-formalizing-rust.md
+++ b/ralf/_posts/2015-10-12-formalizing-rust.md
@@ -37,13 +37,13 @@ The first version is also not going to cover automatic destructors, i.e., the `D
 This is, of course, a significant gap, even more so since dropck may well be the most subtle part of the type system, and the current version (as of Rust 1.3) is [known to be unsound](https://github.com/rust-lang/rust/issues/26656).
 But we have to start somewhere, and even without `Drop`, there is a lot to be done.
 
 This is, of course, a significant gap, even more so since dropck may well be the most subtle part of the type system, and the current version (as of Rust 1.3) is [known to be unsound](https://github.com/rust-lang/rust/issues/26656).
 But we have to start somewhere, and even without `Drop`, there is a lot to be done.
 

-## So what's left?
+## So What's Left?

 
 You may wonder now, what are we even doing then?
 The goal is to prove that programs following Rust's rules of ownership, borrowing and lifetimes are *memory and thread safe*, which, roughly speaking, means that all executed pointer accesses are valid, and there are no data races.
 I will often just say "memory safety", but concurrency is definitely part of the story.
 
 
 You may wonder now, what are we even doing then?
 The goal is to prove that programs following Rust's rules of ownership, borrowing and lifetimes are *memory and thread safe*, which, roughly speaking, means that all executed pointer accesses are valid, and there are no data races.
 I will often just say "memory safety", but concurrency is definitely part of the story.
 

-## The syntactic approach and its limitations
+## The Syntactic Approach and Its Limitations

 
 We could now be looking at the checks the Rust compiler is doing, and prove directly that these checks imply memory safety.
 Let us call these checks Rust's type system, then we are looking for the classic result of *type soundness*: Well-typed programs don't go wrong.
 
 We could now be looking at the checks the Rust compiler is doing, and prove directly that these checks imply memory safety.
 Let us call these checks Rust's type system, then we are looking for the classic result of *type soundness*: Well-typed programs don't go wrong.


@@ -54,7 +54,7 @@ In the following, we will consider programs containing `unsafe` as not being wel
 (We could also consider them well-typed in a more liberal type system that above result does not, and cannot, apply to. This is closer to what the Rust compiler does, but it's not helpful in our context.)
 Note that this issue is viral: `Vec`, `RefCell`, `Rc` -- all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck.
 
 (We could also consider them well-typed in a more liberal type system that above result does not, and cannot, apply to. This is closer to what the Rust compiler does, but it's not helpful in our context.)
 Note that this issue is viral: `Vec`, `RefCell`, `Rc` -- all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck.
 

-## Semantics to the rescue
+## Semantics to the Rescue

 
 Intuitively, why do we even think that a program that uses `Vec`, but contains no `unsafe` block *itself*, should be safe?
 It's not just the compiler checks making sure that, e.g., we don't call `push` on a shared borrow.
 
 Intuitively, why do we even think that a program that uses `Vec`, but contains no `unsafe` block *itself*, should be safe?
 It's not just the compiler checks making sure that, e.g., we don't call `push` on a shared borrow.


@@ -76,7 +76,7 @@ This is in contrast to the *syntactic* notion of well-typedness of a function, w
 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!
 
 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!
 

-## What we are doing
+## What We Are Doing

 
 So, that's what we are trying to do: Come up not only with a formal version of Rust's (syntactic) type system, but also with appropriate *semantics* for these types.
 We then have to show that the syntactic types make semantic sense. This recovers, in a very roundabout way, the result I mentioned above:
 
 So, that's what we are trying to do: Come up not only with a formal version of Rust's (syntactic) type system, but also with appropriate *semantics* for these types.
 We then have to show that the syntactic types make semantic sense. This recovers, in a very roundabout way, the result I mentioned above:

diff --git a/ralf/_posts/2017-05-23-internship-starting.md b/ralf/_posts/2017-05-23-internship-starting.md
index 1b7269be7e2902b7322278a1b24a5214e350d9e9..54361c215b552a04cbb0d272bc5842574635e06f 100644 (file)
--- a/ralf/_posts/2017-05-23-internship-starting.md
+++ b/ralf/_posts/2017-05-23-internship-starting.md
@@ -1,5 +1,5 @@
 ---
 ---

-title: Day 1 of my Mozilla Internship
+title: Day 1 of My Mozilla Internship

 categories: internship rust
 ---
 
 categories: internship rust
 ---