> I get that these underpin the technology we as programmers use every single day Is this actually true? Of course Haskell, Idris, etc. leverage type theory, b

> I get that these underpin the technology we as programmers use every single day Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?