Update strong mode doc

RUNTIME_SAFETY.md

Index: RUNTIME_SAFETY.md
diff --git a/RUNTIME_SAFETY.md b/RUNTIME_SAFETY.md
new file mode 100644
index 0000000000000000000000000000000000000000..f03da7a83253a716f1882ef54f364aaeca2e52d6
--- /dev/null
+++ b/RUNTIME_SAFETY.md
@@ -0,0 +1,71 @@
+# Strong Mode in the Dart Dev Compiler
+
+## Overview
+
+In the Dart Dev Compiler (DDC), static strong mode checks are augmented stricter runtime behavior.  Together, they enforce the soundness of Dart type annotations.

[Leaf, 2016/01/15 00:01:10]

'augmented with'?

[vsm, 2016/01/15 20:13:39]

Done.

+
+In general, and in contrast to Dart's checked mode, most safety is enforced statically, at analysis time.  DDC exploits this to generate relatively few runtime checks while still providing stronger guarantees than checked mode.
+
+In particular, DDC adds the following:
+
+ - Stricter (but fewer) runtime type checks
+ - Reified type narrowing
+
+## Runtime checks
+
+In practice, strong mode enforces most type annotations at compile time, and, thus, requires less work at runtime to enforce safety.  Consider the following Dart code:
+
+```dart
+String foo(Map<int, String> map, int x) {
+  return map[x.abs()];
+}
+```
+
+Strong mode will enforce that the function `foo` is only invoked in a manner consistent with its signature.  DDC - which assumes strong mode static checking - inserts no further runtime checks.  In contrast, standard Dart checked mode would check the type of the parameters - `map` and `x` - along with the type of the return value at runtime on every invocation of `foo`.  Even Dart production mode, depending on the implementation and its ability to optimize, may require similar checking to dynamically dispatch the map lookup and the method call in the body of `foo`.
+
+Nevertheless, there are cases where DDC still requires runtime checks.  (Note: DDC may eventually provide a mode to elide these checks, but this would violate soundness and is beyond the scope of this document.)
+
+### Implicit casts
+
+Dart has flexible assignability rules.  Programmers are not required to explicitly cast from supertypes to subtypes.  For example, the following is valid Dart:
+
+```dart
+Object o = ...;
+String s = o;  // Implicit downcast
+String s2 = s.substring(1);
+```
+
+The assignment to `s` is an implicit downcast from `Object` to `String` and triggers a runtime check in DDC to ensure it is correct.
+
+Note that checked mode would also perform this runtime test.  Unlike checked mode, DDC would not require a check on the assignment to `s2` - this type is established statically.
+
+### Inferred variables
+
+Dart's inference may narrow the static type of certain variables.  If the variable is mutable, DDC will enforce the narrower type at runtime when necessary.
+
+In the following example, strong mode will infer of the type of the local variable `y` as an `int`:  
+
+```dart
+int bar(Object x) {
+  var y = 0;
+  if (x != null) {
+    y = x;
+  }
+  return y.abs();
+}
+```
+
+This allows it to, for example, static verify the call to `y.abs()` and determine that it returns an `int`.  However, the parameter `x` is typed as `Object` and the assignment from `x` to `y` now requires a type check to ensure that `y` is only assigned an `int`.
+
+Note, strong mode and DDC are conservative by enforcing a tighter type than required by standard Dart checked mode.  For example, checked mode would accept a non-`int` `x` with an `abs` method that happened to return an `int`.  In strong mode, a programmer would have to explicitly opt into this behavior by annotating `y` as an `Object` or `dynamic`.
+
+### Covariant generics
+
+
+### Dynamic operations
+
+## Runtime type Narrowing
+
+### Allocation inference
+
+### Generic methods