From 08326a3a35be4560d656b0079fcca7845c5fc93d Mon Sep 17 00:00:00 2001
From: Amal Ahmed <amal@ccs.neu.edu>
Date: Fri, 29 Jun 2018 13:18:54 +0200
Subject: [PATCH] more abstract edits

---
 paper/abstract.tex | 3 ++-
 paper/gtt.tex      | 3 +++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/paper/abstract.tex b/paper/abstract.tex
index 19f1fb9..e876b0d 100644
--- a/paper/abstract.tex
+++ b/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
diff --git a/paper/gtt.tex b/paper/gtt.tex
index b44876c..865d658 100644
--- a/paper/gtt.tex
+++ b/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.
 %
-- 
GitLab