[ridiculous_fish]

> 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?

[leshow]

C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.