For those who wonder, MSO is the logic which is under research to be used for Tau. It's called Monadic Second Order Logic. MSO-U is Monadic Second Order Logic extended with an unbounded quantifier, U binds a set, the property is true for sets that are finite yet arbitrarily large. Tau is MSO over Graphs, but I do not yet know how the developer will deal with issues of decidability. In the near future a blog post will come out which will discuss in detail what Tau will be using but I'm waiting for Ohad to release his blog post.

For the most part this video is just to help people get familiar with MSO, logic, and dealing with infinity.