Also:
> Our optional type system was designed from the perspective that a single language can consistently contain the semantics of both a dynamically-typed and a statically-typed language.
The obvious meaning of the word "consistently" here would preclude Turing-complete languages from this (recognition of the same language + undecidability), unless you adopt a fairly idiosyncratic definition of "type safe". I haven't read the whole thing, but it seems like there's a lot of dancing around this without actually coming out and saying it. For me, at least, headlining what you're not claiming would make this substantially more readable.
Edit: Okay, read some more and the "Parametric Types and Stanza's Captured Type System" and "Implications for Safety" sections "dance closer", but it feels like the implications need to be pulled out and moved way up. The covariance assumption in particular...let's just say that I was expecting something substantially different by the time I got to that point.
Finally, if you want some nit-picky editing advice: The terms "Thus" and (to a lesser extent) "Hence" are used...frequently. Possibly just me, but I found it fairly jarring.