edit response (900 words rn)

popl19/response2.md

 We thank the reviewers for their very helpful feedback and will revise
-the paper accordingly.
+the paper accordingly. In particular, we will expand on the motivation
+for using CBPV.
 
 1. Reviewer C says "Moreover, the paper doesn't produce any particular
    equalities that one might want to reason with while programming."
 
-We would push back on this criticism: we show soundness of an entire
+We disagree: we show soundness of an entire
 class of equalities that are useful for program reasoning by programmers
 and compilers alike: things like lifting an if statement (or more
 generally any pattern match) out of a lambda are very common in
-refactoring and optimization, and induction is fundamental for any
-program verification.
+refactoring and optimization.
 
 In terms of "actionable" theorems, we show that upcasts form complex
 values and downcsats form complex stacks, which also justifies 
@@ -29,13 +29,13 @@ contextually equivalent. We do include beta-eta in the definition of
 term dynamism in figure 4, where they are labeled as axioms of term
 dynamism, but this is not enough to prove completeness for an
 effectful language like cbpv: for instance, both sequential and
-non-deterministic languages should model all of axioms.  To ask if our
-syntax is complete for contextual equivalence we need to fix a
-particular model. The syntax is not intended to be complete for any
-particular model, in order that it apply to as many models as
-possible. This is what allows us to interpret the model with
-incompatible definitions of the dynamic type and extend it with new
-axioms based on that model like those given in figure 5.
+non-deterministic languages should model all of the axioms.
+
+The syntax is not intended to be complete for any particular language,
+in order that it apply to as many as possible. This is what allows us
+to interpret the model with incompatible definitions of the dynamic
+type and extend it with new axioms based on that model like those
+given in figure 5.
 
 3. Reviewer C asks "Do these theorems hold when you distinguish
    between different errors via, e.g., blame labels?"
@@ -50,9 +50,8 @@ that blame(l) would be a least element of our ordering for every label
 l so any two blame errors would be equivalent. 
 
 On the other hand the uniqueness theorems seem that they should hold
-when all of the casts involved have the *same* label; we plan to
-explore this in future work, building on 
-the unpublished tech report:
+when all of the casts involved have the *same* label; we may explore
+this in future work, building on the unpublished tech report:
 https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02
 
 4. Reviewer D asks to clarify lines 116-117.
@@ -60,7 +59,7 @@ https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02
 Yes, we mean that the typed equivalences should hold in the statically
 typed portions of the code; the dynamic type casts ensure that the
 equivalences hold in statically typed portions of the code even if they
-interact with (more) dynamically typed code.  We expect that it will be
+interact with (more) dynamically typed code. We expect that it will be
 rare for gradually typed programs to be completely typed (e.g. this is
 very rare in Typed Racket).
 
@@ -68,10 +67,10 @@ very rare in Typed Racket).
    way up to ? if we can still reduce everything to upcasts and
    downcasts.
 
-The use of ? in the factorization of a cast A => B can be replaced with
-any type D that is more dynamic than both A and B, so ?, if it is
-present, always works. We would be curious to know of any systems where
-a cast A => B was allowed but they have no common dynamism-supertype.
+The use of ? in the factorization of a cast A => B can be replaced
+with any type D that is more dynamic than both A and B. We don't konw
+of any systems where a cast A => B is allowed but they have no common
+dynamism-supertype.
 
 6. Reviewer C says that we "restrict to non-effectful programs" and
    finds it surprising because "blame is an effect".
@@ -89,7 +88,7 @@ effects.
 Yes, in the "eager" cast semantics, the eta law for functions should be
 an ordering `V <= \x -> V x` but it's debateable whether this means that
 the right should be allowed to be optimized to the left. This would make
-the semantics of the program dependent on the precise behvior of the
+the semantics of the program dependent on the precise behavior of the
 optimizer, so it would be very hard to change the optimizer without
 either making code error that didn't before or vice-versa (because
 whether or not an optimization is triggered can be very sensitive to
@@ -101,10 +100,8 @@ We apologize for the oversight and will add appropriate discussion; for
 Henglein, a significant difference is that the equational theory there
 is based on a rewriting system with cast rules for each pair of types,
 whereas in our approach those rules are a theorem following from the
-universal characterization of casts.  For others TODO?
+specification of casts.
 
-9. Reviewer B: we apologize that the presentation was not accessible and
-   will work to give a better high-level introduction in the revisions.
-   The reason existing work does not suffice is that gradual typing
-   introduces a dynamic type ? and type casts, and the question is how
-   to enrich the equational theories of CBV and CBN with these features.  
+We will also add a discussion of Degen and Thiemann's work, which is
+related: their completeness property inherently violates CBN eta
+principles, so is incompatible with "lazy" checking.
\ No newline at end of file