Add posts from dotty-website

6 files changed, 471 insertions, 12 deletions

diff --git a/docs/blog/2015-10-23-dotty-compiler-bootstraps.md b/docs/blog/2015-10-23-dotty-compiler-bootstraps.md
index cdd472b7f..519848f23 100644
--- a/docs/blog/2015-10-23-dotty-compiler-bootstraps.md
+++ b/docs/blog/2015-10-23-dotty-compiler-bootstraps.md
@@ -1,11 +1,10 @@
 ---
-layout: blog
-post-type: blog
-by: Martin Odersky and Dmitry Petrashko
-title: We Got LiftOff! The Dotty Compiler for Scala Bootstraps.
+author: Martin Odersky and Dmitry Petrashko
+title: "We got liftoff!"
+subTitle: The Dotty compiler for Scala bootstraps.
 ---
 
-## We Got Liftoff!
+## We got liftoff!
 
 The [Dotty project](https://github.com/lampepfl/dotty)
 is a platform to develop new technology for Scala
@@ -14,7 +13,7 @@ Its compiler is a new design intended to reflect the
 lessons we learned from work with the Scala compiler. A clean redesign
 today will let us iterate faster with new ideas in the future.
 
-Today we reached an important milestone: The Dotty compiler can
+Today we reached an important milestone: the Dotty compiler can
 compile itself, and the compiled compiler can act as a drop-in for the
 original one. This is what one calls a *bootstrap*.
 
@@ -35,7 +34,7 @@ go unnoticed, precisely because every part of a compiler feeds into
 other parts and all together are necessary to produce a correct
 translation.
 
-## Are We Done Yet?
+## Are we done yet?
 
 Far from it! The compiler is still very rough. A lot more work is
 needed to
@@ -43,21 +42,28 @@ needed to
  - make it more robust, in particular when analyzing incorrect programs,
  - improve error messages and warnings,
  - improve the efficiency of some of the generated code,
+ - improve compilation speed,
  - embed it in external tools such as sbt, REPL, IDEs,
  - remove restrictions on what Scala code can be compiled,
  - help in migrating Scala code that will have to be changed.
 
-## What Are the Next Steps?
+## What are the next steps?
 
 Over the coming weeks and months, we plan to work on the following topics:
 
  - Make snapshot releases.
- - Get the Scala standard library to compile.
  - Work on SBT integration of the compiler.
  - Work on IDE support.
  - Investigate the best way to obtaining a REPL.
  - Work on the build infrastructure.
 
-If you want to get your hands dirty with any of this, now is a good moment to get involved!
-To get started: <https://github.com/lampepfl/dotty>.
+If you want to get your hands dirty with any of this, now is a good
+moment to get involved! Join the team of contributors, including
+Dmitry Petrashko ([@DarkDimius](https://github.com/DarkDimius)),
+Guillaume Martres ([@smarter](https://github.com/smarter)),
+Ondrey Lhotak ([@olhotak](https://github.com/olhotak)),
+Samuel Gruetter ([@samuelgruetter](https://github.com/samuelgruetter)),
+Vera Salvis ([@vsalvis](https://github.com/vsalvis)),
+and Jason Zaugg ([@retronym](https://github.com/retronym)).
 
+To get started: <https://github.com/lampepfl/dotty>.
diff --git a/docs/blog/2016-01-02-new-year-resolutions.md b/docs/blog/2016-01-02-new-year-resolutions.md
new file mode 100644
index 000000000..7402a2347
--- /dev/null
+++ b/docs/blog/2016-01-02-new-year-resolutions.md
@@ -0,0 +1,64 @@
+---
+title: New Year Resolutions
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+For most of us, the change of the year is an occasion for thinking
+about what we missed doing last year and where we want to improve. I decided
+there are a couple of things where I would like to do better in 2016
+than in 2015. The first is that I would like to do more blogging and
+writing in general. I have been pretty silent for most of the last
+year. This was mostly caused by the fact that I had been heads down to
+work on DOT, Scala's foundations, and _dotty_, the new Scala compiler
+platform we are working on. It's been a lot of work, but we are finally
+getting good results. DOT now has a mechanized proof of type soundness
+and the dotty compiler [can now compile
+itself](http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html)
+as well as large parts of Scala's standard library.
+
+The dotty compiler has a completely new and quite unusual
+architecture, which makes it resemble a functional database or a
+functional reactive program. My [talk at the JVM language
+summit](https://www.youtube.com/watch?v=WxyyJyB_Ssc) gives an
+overview. In the coming months I want to write together with my
+collaborators a series of blog posts
+ that explain details of the code base. The
+aim of these posts will be to present the new architectural patterns
+to a larger audience and also to help existing and potential
+contributors get familiar with the code base.
+
+My second resolution is to take a larger effort to promote simplicity
+in Scala. I believe the recent [blog post by Jim
+Plush](http://jimplush.com/talk/2015/12/19/moving-a-team-from-scala-to-golang/) should be a wakeup call for our
+community. Scala is a very powerful and un-opinionated language.  This
+means we have a large spectrum of choice how to write a Scala
+application or library. It's very important for all of us to use this
+power wisely, and to promote simplicity of usage wherever possible.
+Unfortunately, most of us fall all too easily into the complexity
+trap, as Alex Payne's tweet sums it up very nicely.
+
+<blockquote class="twitter-tweet" lang="en"><p lang="en" dir="ltr">“Complexity is like a bug light for smart people. We can&#39;t resist it, even though we know it&#39;s bad for us.” <a href="https://t.co/V9Izi573CF">https://t.co/V9Izi573CF</a></p>&mdash; Alex Payne (@al3x) <a href="https://twitter.com/al3x/status/683036775942496256">January 1, 2016</a></blockquote>
+<script async src="//platform.twitter.com/widgets.js" charset="utf-8"></script>
+
+I have been as guilty of complication as everybody else. Is
+`CanBuildFrom` the most appropriate solution to deal with the
+constraints of embedding special types such as arrays and strings in a
+collection library? It achieves its purpose of providing a uniform
+user-level API on disparate datatypes. But I now think with more
+effort we might be able come up with a solution that works as well and
+is simpler. Another example, where I have doubts if not regrets are
+the `/:` and `:\` operators in scala.collections.  They are cute
+synonyms for folds, and I am still fond of the analogy with falling
+dominoes they evoke. But in retrospect I think maybe they did give a
+bad example for others to go overboard with symbolic operators.
+
+So my main agenda for the coming year is to work on making Scala
+simpler: The language, its foundations, its libraries. I hope you
+will join me in that venture.
+
+With that thought, I wish you a happy new year 2016.
+
+
+
+
diff --git a/docs/blog/2016-02-03-essence-of-scala.md b/docs/blog/2016-02-03-essence-of-scala.md
new file mode 100644
index 000000000..e5e68d0fd
--- /dev/null
+++ b/docs/blog/2016-02-03-essence-of-scala.md
@@ -0,0 +1,144 @@
+---
+title: The Essence of Scala
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+What do you get if you boil Scala on a slow flame and wait until all
+incidental features evaporate and only the most concentrated essence
+remains? After doing this for 8 years we believe we have the answer:
+it's DOT, the calculus of dependent object types, that underlies Scala.
+
+A [paper on DOT](http://infoscience.epfl.ch/record/215280) will be
+presented in April at [Wadlerfest](http://events.inf.ed.ac.uk/wf2016),
+an event celebrating Phil Wadler's 60th birthday. There's also a prior
+technical report ([From F to DOT](http://arxiv.org/abs/1510.05216))
+by Tiark Rompf and Nada Amin describing a slightly different version
+of the calculus. Each paper describes a proof of type soundness that
+has been machine-checked for correctness.
+
+## The DOT calculus
+
+A calculus is a kind of mini-language that is small enough to be
+studied formally. Translated to Scala notation, the language covered
+by DOT is described by the following abstract grammar:
+
+    Value       v  =  (x: T) => t            Function
+                      new { x: T => ds }     Object
+
+    Definition  d  =  def a = t              Method definition
+                      type A = T             Type
+
+    Term        t  =  v                      Value
+                      x                      Variable
+                      t1(t2)                 Application
+                      t.a                    Selection
+                      { val x = t1; t2 }     Local definition
+
+    Type        T  =  Any                    Top type
+                      Nothing                Bottom type
+                      x.A                    Selection
+                      (x: T1) => T2          Function
+                      { def a: T }           Method declaration
+                      { type T >: T1 <: T2 } Type declaration
+                      T1 & T2                Intersection
+                      { x => T }             Recursion
+
+The grammar uses several kinds of names:
+
+    x      for (immutable) variables
+    a      for (parameterless) methods
+    A      for types
+
+The full calculus adds to this syntax formal _typing rules_ that
+assign types `T` to terms `t` and formal _evaluation rules_ that
+describe how a program is evaluated. The following _type soundness_
+property was shown with a mechanized, (i.e. machine-checked) proof:
+
+> If a term `t` has type `T`, and the evaluation of `t` terminates, then
+  the result of the evaluation will be a value `v` of type `T`.
+
+## Difficulties
+
+Formulating the precise soundness theorem and proving it was unexpectedly hard,
+because it uncovered some technical challenges that had not been
+studied in depth before. In DOT - as well as in many programming languages -
+you can have conflicting definitions. For instance you might have an abstract
+type declaration in a base class with two conflicting aliases in subclasses:
+
+     trait Base { type A }
+     trait Sub1 extends Base { type A = String }
+     trait Sub2 extends Base { type A = Int }
+     trait Bad extends Sub1 with Sub2
+
+Now, if you combine `Sub1` and `Sub2` in trait `Bad` you get a conflict,
+since the type `A` is supposed to be equal to both `String` and `Int`. If you do
+not detect the conflict and assume the equalities at face value you
+get `String = A = Int`, hence by transitivity `String = Int`! Once you
+are that far, you can of course engineer all sorts of situations where
+a program will typecheck but cause a wrong execution at runtime. In
+other words, type soundness is violated.
+
+Now, the problem is that one cannot always detect these
+inconsistencies, at least not by a local analysis that does not need
+to look at the whole program. What's worse, once you have an
+inconsistent set of definitions you can use these definitions to
+"prove" their own consistency - much like a mathematical theory that
+assumes `true = false` can "prove" every proposition including its own
+correctness.
+
+The crucial reason why type soundness still holds is this: If one
+compares `T` with an alias, one does so always relative to some _path_
+`x` that refers to the object containing `T`.  So it's really `x.T =
+Int`. Now, we can show that during evaluation every such path refers
+to some object that was created with a `new`, and that, furthermore,
+every such object has consistent type definitions. The tricky bit is
+to carefully distinguish between the full typing rules, which allow
+inconsistencies, and the typing rules arising from runtime values,
+which do not.
+
+## Why is This Important?
+
+There are at least four reasons why insights obtained in the DOT
+project are important.
+
+ 1. They give us a well-founded explanation of _nominal typing_.
+    Nominal typing means that a type is distinguished from others
+    simply by having a different name.
+    For instance, given two trait definitions
+
+          trait A extends AnyRef { def f: Int }
+          trait B extends AnyRef { def f: Int }
+
+    we consider `A` and `B` to be different types, even though both
+    traits have the same parents and both define the same members.
+    The opposite of
+    nominal typing is structural typing, which treats types
+    that have the same structure as being the same. Most programming
+    languages are at least in part nominal whereas most formal type systems,
+    including DOT, are structural. But the abstract types in DOT
+    provide a way to express nominal types such as classes and traits.
+    The Wadlerfest paper contains examples that show how
+    one can express classes for standard types such as `Boolean` and `List` in DOT.
+
+ 2. They give us a stable basis on which we can study richer languages
+    that resemble Scala more closely. For instance, we can encode
+    type parameters as type members of objects in DOT. This encoding
+    can give us a better understanding of the interactions of
+    subtyping and generics. It can explain why variance rules
+    are the way they are and what the precise typing rules for
+    wildcard parameters `[_ <: T]`, `[_ >: T]` should be.
+
+ 3. DOT also provides a blueprint for Scala compilation. The new Scala
+    compiler _dotty_ has internal data structures that closely resemble DOT.
+    In particular, type parameters are immediately mapped to type members,
+    in the way we propose to encode them also in the calculus.
+
+ 4. Finally, the proof principles explored in the DOT work give us guidelines
+    to assess and treat other possible soundness issues. We now know much
+    better what conditions must be fulfilled to ensure type soundness.
+    This lets us put other constructs of the Scala language to the test,
+    either to increase our confidence that they are indeed sound, or
+    to show that they are unsound. In my next blog I will
+    present some of the issues we have discovered through that exercise.
+
diff --git a/docs/blog/2016-02-17-scaling-dot-soundness.md b/docs/blog/2016-02-17-scaling-dot-soundness.md
new file mode 100644
index 000000000..e01b66d09
--- /dev/null
+++ b/docs/blog/2016-02-17-scaling-dot-soundness.md
@@ -0,0 +1,157 @@
+---
+title: Scaling DOT to Scala - Soundness
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+In my [last
+blog post](http://www.scala-lang.org/blog/2016/02/03/essence-of-scala.html)
+I introduced DOT, a minimal calculus that underlies much of Scala.
+DOT is much more than an academic exercise, because it gives us
+guidelines on how to design a sound type system for full Scala.
+
+## Recap: The Problem of Bad Bounds
+
+As was argued in the previous blog post, the danger a path-dependent type
+system like Scala's faces is inconsistent bounds or aliases. For
+instance, you might have a type alias
+
+      type T = String
+
+in scope in some part of the program, but in another part the same
+type member `T` is known as
+
+      type T = Int
+
+If you connect the two parts, you end up allowing assigning a `String`
+to an `Int` and vice versa, which is unsound - it will crash at
+runtime with a `ClassCastException`. The problem is that there
+is no obvious, practical, compile time analysis for DOT or
+Scala that ensures that all types have good bounds. Types can contain
+abstract type members with bounds that can be refined elsewhere and
+several independent refinements might lead together to a bad bound
+problem.  Barring a whole program analysis there is no specific
+point in the program where we can figure this out straightforwardly.
+
+In DOT, the problem is resolved by insisting that every path prefix `p`
+of a type `p.T` is at runtime a concrete value. That way, we only have
+to check for good bounds when objects are _created_ with `new`, and
+that check is easy: When objects are created, we know their class and
+we can insist that all nested types in that class are aliases or
+have consistent bounds. So far so good.
+
+## Loopholes Caused by Scaling Up
+
+But if we want to scale up the DOT result for full Scala, several
+loopholes open up. These come all down to the fact that the prefix of
+a type selection might _not_ be a value that's constructed with a
+`new` at run time.  The loopholes can be classified into three
+categories:
+
+ 1. The prefix value might be lazy, and never instantiated to anything, as in:
+
+        lazy val p: S = p
+        ... p.T ...
+
+    Note that trying to access the lazy value `p` would result in an infinite loop. But using `p` in a type does not force its evaluation, so we might never evaluate `p`. Since `p` is not initialized with a `new`, bad bounds for `T` would go undetected.
+
+ 2. The prefix value might be initialized to `null`, as in
+
+        val p: S = null
+        ... p.T ...
+
+    The problem here is similar to the first one. `p` is not initialized
+    with a `new` so we know nothing about the bounds of `T`.
+
+ 3. The prefix might be a type `T` in a type projection `T # A`, where `T`
+    is not associated with a runtime value.
+
+We can in fact construct soundness issues in all of these cases. Look
+at the discussion for issues [#50](https://github.com/lampepfl/dotty/issues/50)
+and [#1050](https://github.com/lampepfl/dotty/issues/1050) in the
+[dotty](https://github.com/lampepfl/dotty/issues/1050) repository
+on GitHub. All issues work fundamentally in the same way: Construct a type `S`
+which has a type member `T` with bad bounds, say
+
+    Any <: T <: Nothing
+
+Then, use the left subtyping to turn an expression of type `Any` into
+an expression of type `T` and use the right subtyping to turn that
+expression into an expression of type `Nothing`:
+
+    def f(x: Any): p.T = x
+    def g(x: p.T): Nothing = x
+
+Taken together, `g(f(x))` will convert every expression into an
+expression of type `Nothing`. Since `Nothing` is a subtype of every
+other type, this means you can convert an arbitrary expression to have
+any type you choose. Such a feat is an impossible promise, of
+course. The promise is usually broken at run-time by failing with a
+`ClassCastException`.
+
+## Plugging the Loopholes
+
+To get back to soundness we need to plug the loopholes. Some of the
+necessary measures are taken in pull request [#1051](https://github.com/lampepfl/dotty/issues/1051).
+That pull request
+
+ - tightens the rules for overrides of lazy values: lazy values
+   cannot override or implement non-lazy values,
+ - tightens the rules which lazy values can appear in paths: they
+   must be final and must have concrete types with known consistent bounds,
+ - allows type projections `T # A` only if `T` is a concrete type
+   with known consistent bounds.
+
+It looks like this is sufficient to plug soundness problems (1) and
+(3). To plug (2), we need to make the type system track nullability in
+more detail than we do it now. Nullability tracking is a nice feature
+in its own right, but now we have an added incentive for implementing
+it: it would help to ensure type soundness.
+
+There's one sub-case of nullability checking which is much harder to do
+than the others. An object reference `x.f` might be `null` at run time
+because the field `f` is not yet initialized. This can lead to a
+soundness problem, but in a more roundabout way than the other issues
+we have identified. In fact, Scala guarantees that in a program that
+runs to completion without aborting, every field will eventually be
+initialized, so every non-null field will have good bounds. Therefore,
+the only way an initialized field `f` could cause a soundness problem
+is if the program in question would never get to initialize `f`,
+either because it goes into an infinite loop or because it aborts with
+an exception or `System.exit` call before reaching the initialization
+point of `f`. It's a valid question whether type soundness guarantees
+should extend to this class of "strange" programs. We might want to
+draw the line here and resort to runtime checks or exclude "strange"
+programs from any soundness guarantees we can give. The research community
+has coined the term [soundiness](http://soundiness.org/) for
+this kind of approach and has [advocated](http://cacm.acm.org/magazines/2015/2/182650-in-defense-of-soundiness/fulltext) for it.
+
+The necessary restrictions on type projection `T # A` are problematic
+because they invalidate some idioms in type-level programming. For
+instance, the cute trick of making Scala's type system Turing complete
+by having it [simulate SK
+combinators](https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/)
+would no longer work since that one relies on unrestricted type
+projections. The same holds for some of the encodings of type-level
+arithmetic.
+
+To ease the transition, we will continue for a while to allow unrestricted type
+projections under a flag, even though they are potentially
+unsound. In the current dotty compiler, that flag is a language import
+`-language:Scala2`, but it could be something different for other
+compilers, e.g. `-unsafe`.  Maybe we can find rules that are less
+restrictive than the ones we have now, and are still sound.  But one
+aspect should be non-negotiable: Any fundamental deviations from the
+principles laid down by DOT needs to be proven mechanically correct
+just like DOT was. We have achieved a lot with the DOT proofs, so we
+should make sure not to back-slide. And if the experience of the past
+10 years has taught us one thing, it is that the meta theory of type
+systems has many more surprises in store than one might think. That's
+why mechanical proofs are essential.
+
+
+
+
+
+
+
diff --git a/docs/blog/2016-05-05-multiversal-equality.md b/docs/blog/2016-05-05-multiversal-equality.md
new file mode 100644
index 000000000..e6c8a2014
--- /dev/null
+++ b/docs/blog/2016-05-05-multiversal-equality.md
@@ -0,0 +1,88 @@
+---
+title: Multiversal Equality for Scala
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+I have been working recently on making equality tests using `==` and `!=` safer in Scala. This has led to a [Language Enhancement Proposal](https://github.com/lampepfl/dotty/issues/1247) which I summarize in this blog.
+
+## Why Change Equality?
+
+Scala prides itself of its strong static type system. Its type discipline is particularly useful when it comes to refactoring. Indeed, it's possible to write programs in such a way that refactoring problems show up with very high probability as type errors. This is essential for being able to refactor with the confidence that nothing will break. And the ability to do such refactorings is in turn very important for keeping code bases from rotting.
+
+Of course, getting such a robust code base requires the cooperation of the developers. They should avoid type `Any`, casts, [stringly typed](http://c2.com/cgi/wiki?StringlyTyped) logic, and more generally any operation over loose types that do not capture the important properties of a value. Unfortunately, there is one area in Scala where such loose types are very hard to avoid: That's equality. Comparisons with `==` and `!=` are _universal_. They compare any two values, no matter what their types are. This causes real problems for writing code and more problems for refactoring it.
+
+For instance, one might want to introduce a proxy for some data structure so that instead of accessing the data structure directly one goes through the proxy. The proxy and the underlying data would have different types. Normally this should be an easy refactoring. If one passes by accident a proxy for the underlying type or _vice versa_ the type checker will flag the error. However, if one accidentally compares a proxy with the underlying type using `==` or a pattern match, the program is still valid, but will just always say `false`.  This is a real worry in practice. I recently abandoned a desirable extensive refactoring because I feared that it would be too hard to track down such errors.
+
+## Where Are We Today?
+
+The problems of universal equality in Scala are of course well known. Some libraries have tried to fix it by adding another equality operator with more restricted typing. Most often this safer equality is written `===`. While `===` is certainly useful, I am not a fan of adding another equality operator to the language and core libraries. It would be much better if we could fix `==` instead. This would be both simpler and would catch all potential equality problems including those related to pattern matching.
+
+How can `==` be fixed? It looks much harder to do this than adding an alternate equality operator. First, we have to keep backwards compatibility. The ability to compare everything to everything is by now baked into lots of code and libraries.  Second, with just one equality operator we need to make this operator work in all cases where it makes sense. An alternative `===` operator can choose to refuse some comparisons that should be valid because there's always `==` to fall back to. With a unique `==` operator we do not have this luxury.
+
+The current status in Scala is that the compiler will give warnings for _some_ comparisons that are always `false`. But the coverage is weak. For instance this will give a warning:
+
+```
+scala> 1 == "abc"
+<console>:12: warning: comparing values of types Int and String using `==' will always yield false
+```
+
+But this will not:
+
+```
+scala> "abc" == 1
+res2: Boolean = false
+```
+
+There are also cases where a warning is given for a valid equality test that actually makes sense because the result could be `true`. In summary, the current checking catches some obvious bugs, which is nice. But it is far too weak and fickle to be an effective refactoring aid.
+
+
+## What's Proposed?
+
+I believe to do better, we need to enlist the cooperation of developers. Ultimately it's the developer who provides implementations of equality methods and who is therefore best placed to characterize which equalities make sense. Sometimes this characterization can be involved. For instance, an `Int` can be compared to other primitive numeric values or to instances of type `java.lang.Number` but any other comparison will always yield `false`. Or, it makes sense to compare two `Option` values if and only if it makes sense to compare the optional element values.
+
+The best known way to characterize such relationships is with type classes. Implicit values of a trait `Eq[T, U]` can capture the property that values of type `T` can be compared to values of type `U`. Here's the definition of `Eq`
+
+```
+package scala
+
+trait Eq[-T, -U]
+```
+
+That is, `Eq` is a pure marker trait with two type parameters and without any members.  Developers can define equality classes by giving implicit `Eq` instances. Here is a simple one:
+
+```
+implicit def eqString: Eq[String, String] = Eq
+```
+
+This states that strings can be only compared to strings, not to values of other types.  Here's a more complicated `Eq` instance:
+
+```
+implicit def eqOption[T, U](implicit _eq: Eq[T, U]): Eq[Option[T], Option[U]] = Eq
+```
+
+This states that `Option` values can be compared if their elements can be compared.
+
+It's foreseen that such `Eq` instances can be generated automatically. If we add an annotation `@equalityClass` to `Option` like this
+
+```
+@equalityClass class Option[+T] { ... }
+```
+
+then the `eqOption` definition above would be generated automatically in `Option`'s companion object.
+
+Given a set of `Eq` instances, the idea is that the Scala compiler will check every time it encounters a _potentially problematic_ comparison between values of types `T` and `U` that there is an implicit instance of `Eq[T, U]`. A comparison is _potentially problematic_ if it is between incompatible types. As long as `T <: U` or `U <: T` the equality could make sense because both sides can potentially be the same value.
+
+So this means we still keep universal equality as it is in Scala now - we don't have a choice here anyway, because of backwards compatibility. But we render it safe by checking that for each comparison the corresponding `Eq` instance exists.
+
+What about types for which no `Eq` instance exists? To maintain backwards compatibility, we allow comparisons of such types as well, by means of a fall-back `eqAny` instance. But we do not allow comparisons between types that have an `Eq` instance and types that have none.  Details are explained in the [proposal](https://github.com/lampepfl/dotty/issues/1247).
+
+## Properties
+
+Here are some nice properties of the proposal
+
+1. It is _opt-in_. To get safe checking, developers have to annotate with `@equalityClass` classes that should allow comparisons only between their instances, or they have to define implicit `Eq` instances by hand.  2. It is backwards compatible. Without developer-provided `Eq` instances, equality works as before.
+3. It carries no run-time cost compared to universal equality. Indeed the run-time behavior of equality is not affected at all.
+4. It has no problems with parametricity, variance, or bottom types.  5. Depending on the actual `Eq` instances given, it can be very precise. That is, no comparisons that might yield `true` need to be rejected, and most comparisons that will always yield `false` are in fact rejected.
+
+The scheme effectively leads to a partition of the former universe of types into sets of types. Values with types in the same partition can be compared among themselves but values with types in different partitions cannot.  An `@equalityClass` annotation on a type creates a new partition. All types that do not have any `Eq` instances (except `eqAny`, that is) form together another partition.  So instead of a single _universe_ of values that can be compared to each other we get a _multiverse_ of partitions. Hence the name of the proposal: **Multiversal Equality**.
diff --git a/docs/dotc-scalac.md b/docs/dotc-scalac.md
index d1d435371..8ddabbac5 100644
--- a/docs/dotc-scalac.md
+++ b/docs/dotc-scalac.md
@@ -59,7 +59,7 @@ if (sym is Flags.PackageClass)  // dotc (*)
   `Long`
 * Each flag is either valid for types, terms, or both
 
-````
+```
 000..0001000..01
         ^     ^^
         flag  | \