more abstract edits

paper/abstract.tex

@@ -5,7 +5,8 @@ type-based reasoning is preserved when moving from the fully static setting to a
 gradual one. But gradual type soundness does not imply that type-based
 refactorings and optimizations are still sound in the gradual language.  
 Unfortunately, establishing the correctness of program transformations is 
-technically difficult and often neglected in the metatheory of these languages. 
+technically difficult---requires proofs of program equivalence---and
+often neglected in the metatheory of these languages.  
 
 In this paper, we propose an \emph{axiomatic} account of program equivalence in a
 gradual cast calculus, which we formalize in a logic we call \emph{gradual type

paper/gtt.tex

@@ -378,6 +378,9 @@ different from full static typing: we already accept the possibility that
 another part of the program goes into an infinite loop, and all of our
 reasoning must be relative to that possibility.
 
+% AA: Let's make sure that following paragraph is understandable even if the
+% reader doesn't know difference between transient, eager, and lazy semantics. 
+
 However, the dichotomy between gradual and optional typing is not as
 firm as one might like.
 %