We've started to formalise TypeQL (TypeDB's query language) using dependent type theory, which fit together very nicely. Interestingly, the formalisation shows us how to consistently and safely extend the language with new structures for higher levels of expressivity, which is a huge benefit of type theoretic formalisms of production languages IMO.