From d3bf5b92fa1fb9e313b66cd4a36fe2ece53cd525 Mon Sep 17 00:00:00 2001
From: Justin Hsu <email@justinh.su>
Date: Wed, 21 Nov 2018 15:39:18 -0600
Subject: [PATCH] Tweak slides.

---
 .../docs/resources/slides/lecture-langsec.md  | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/website/docs/resources/slides/lecture-langsec.md b/website/docs/resources/slides/lecture-langsec.md
index c661ce8..71db742 100644
--- a/website/docs/resources/slides/lecture-langsec.md
+++ b/website/docs/resources/slides/lecture-langsec.md
@@ -46,7 +46,7 @@ date: November 21, 2018
     - Model "essence" of real languages
 
 ## 2. Formalize what programs "do"
-- Usually: run it on a machine and find out!
+- Run it on a machine and find out?
     - Not very useful for proofs...
 - Formalize behavior mathematically, on paper
     - Discard "unimportant" details
@@ -115,7 +115,7 @@ date: November 21, 2018
 
 # Operational Semantics
 
-## Programs execute by "stepping"
+## Execute by "stepping"
 - Start with program
     - Imperative: plus variable setting
 - In each step, perform update:
@@ -137,8 +137,8 @@ date: November 21, 2018
 - A type $\tau$ describes a class of programs
     - Usually: well-behaved in some way
 - Can automatically check if program has type $\tau$
-    - Type of program depends on types of its pieces
-    - Scales to large programs
+    - Type of program depends on types of components
+    - Analysis scales to large programs
 
 ## Example
 
@@ -146,18 +146,18 @@ date: November 21, 2018
 - Lightweight
     - Checking types is simple, automatic
     - Don't need to run program
-- Intuitive meaning
+- Natural and intuitive
     - Can't add a String to a Boolean
     - Programmers often think in terms of types
 - Identify correct programs
 
 ## Weaknesses
-- Programmer may need to add some type hints
-    - Extra annotations in program
+- Programmer may need to add annotations
+    - Extra hints for compiler
     - Common for more complex types
 - Compiler sometimes rejects correct programs
     - Figuring out why can be very frustrating
-    - May need to write program in more awkward form
+    - May need to write program in less natural form
 
 ## Types can be complex
 - Simpler types
@@ -170,9 +170,9 @@ date: November 21, 2018
     - ...
 
 ## Prove: soundness
-- "Soundness theorem"
-    - Relate type system to operational behavior
 - If program has a type, it should be well-behaved
+    - Relate type system to operational behavior
+    - "Soundness theorem"
 - Many possible notions of "well-behaved"
     - Don't add Strings to Bools
     - Don't mix public and private data