This talk is great and Giuseppe delivers it well. I'm really impressed with the expressiveness of the type system they have designed. Describing types as sets with predicate logic reads very clearly.
I was particularly impressed with the Exahustivity and redundancy in pattern matching, using the type to inform you when you have failed to fulfill the type contract across multiple expressions is _very_ clever and yet very easy to understand. This feels very much like the type of feedback I would expect from elixir when writing.