I'm feeling both really pissed and validated right now. I thought this was going to just be a normal thoughtless config language that would only be successful as a Google project. Then I looked at the theoretical basis page. I have no formal proof about this, but I've been talking about this type of a type system with my parents and high school CS teacher for a while now! My idea sounds like this: a value is simply an actual binary string. The "type" that classifies any data is described as a formal grammar, where the binary string is a formal language. If the language can parse a given binary value with the formal grammar, that value is an element of the set (type). This naturally leads to a structural type system which can be described using existing set theory and implemented using existing parsers and formal language theory. Of course, this leads to type -> type functions which describe dependent and refinement types naturally. It's great to see this idea being broadcast on the front page here, as I can see it very clearly as a superior type system. I'm really regretting not writing a formal article about it sooner!